Imports
import Mathlib.Tactic import Analysis.Section_7_2 import Analysis.Section_7_3 import Analysis.Section_7_4 import Analysis.Section_8_1

Analysis I, Section 8.2: Summation on infinite sets

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

  • Absolute convergence and summation on countably infinite or general sets.

  • Connections with Mathlib's Summable and tsum.

  • The Riemann rearrangement theorem.

Some non-trivial API is provided beyond what is given in the textbook in order connect these notions with existing summation notions.

After this section, the summation notation developed here will be deprecated in favor of Mathlib's API for Summable and tsum.

namespace Chapter8open Chapter7 Chapter7.Series Finset Function Filter

Definition 8.2.1 (Series on countable sets). Note that with this definition, functions defined on finite sets will not be absolutely convergent; one should use AbsConvergent' instead for such cases.

abbrev AbsConvergent {X:Type} (f: X ) : Prop := g: X, Bijective g (f g: Series).absConverges
theorem AbsConvergent.mk {X: Type} {f:X } {g: X} (h: Bijective g) (hfg: (f g:Series).absConverges) : AbsConvergent f := X:Typef:X g: Xh:Bijective ghfg:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesAbsConvergent f All goals completed! 🐙

The definition has been chosen to give a sensible value when X is finite, even though AbsConvergent is by definition false in this context.

open Classical innoncomputable abbrev Sum {X:Type} (f: X ) : := if h: AbsConvergent f then (f h.choose:Series).sum else if _hX: Finite X then ( x @univ X (Fintype.ofFinite X), f x) else 0
theorem Sum.of_finite {X:Type} [hX:Finite X] (f:X ) : Sum f = x @Finset.univ X (Fintype.ofFinite X), f x := X:TypehX:Finite Xf:X Sum f = x, f x have : ¬ AbsConvergent f := X:TypehX:Finite Xf:X Sum f = x, f x X:TypehX:Finite Xf:X this:AbsConvergent fFalse; X:TypehX:Finite Xf:X g: Xhg:Bijective ga✝:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesFalse X:TypehX:¬Infinite f:X g: Xhg:Bijective ga✝:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesFalse; X:TypehX:¬Infinite f:X g: Xhg:Bijective ga✝:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesInfinite ; All goals completed! 🐙 All goals completed! 🐙theorem AbsConvergent.comp {X: Type} {f:X } {g: X} (h: Bijective g) (hf: AbsConvergent f) : (f g:Series).absConverges := X:Typef:X g: Xh:Bijective ghf:AbsConvergent f{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConverges X:Typef:X g: Xh:Bijective gg': Xhbij:Bijective g'hconv:{ m := 0, seq := fun n if n 0 then (f g') n.toNat else 0, vanish := }.absConverges{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConverges X:Typef:X g: Xh:Bijective gg': Xhbij:Bijective g'hconv:{ m := 0, seq := fun n if n 0 then (f g') n.toNat else 0, vanish := }.absConvergesg'_inv:X hleft:LeftInverse g'_inv g'hright:RightInverse g'_inv g'{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConverges X:Typef:X g: Xh:Bijective gg': Xhbij:Bijective g'hconv:{ m := 0, seq := fun n if n 0 then (f g') n.toNat else 0, vanish := }.absConvergesg'_inv:X hleft:LeftInverse g'_inv g'hright:RightInverse g'_inv g'hG:Bijective (g'_inv g){ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConverges X:Typef:X g: Xh:Bijective gg': Xhbij:Bijective g'hconv:{ m := 0, seq := fun n if n 0 then (f g') n.toNat else 0, vanish := }.absConvergesg'_inv:X hleft:LeftInverse g'_inv g'hright:RightInverse g'_inv g'hG:Bijective (g'_inv g)n:a✝:n 0(f g) n.toNat = (fun n (f g') ((g'_inv g) n)) n.toNat All goals completed! 🐙theorem Sum.eq {X: Type} {f:X } {g: X} (h: Bijective g) (hfg: (f g:Series).absConverges) : (f g:Series).convergesTo (Sum f) := X:Typef:X g: Xh:Bijective ghfg:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConverges{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.convergesTo (Sum f) X:Typef:X g: Xh:Bijective ghfg:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesthis:AbsConvergent f{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.convergesTo (Sum f) X:Typef:X g: Xh:Bijective ghfg:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesthis:AbsConvergent f{ m := 0, seq := fun n if 0 n then f (g n.toNat) else 0, vanish := }.convergesTo { m := 0, seq := fun n if 0 n then f (.choose n.toNat) else 0, vanish := }.sum X:Typef:X g: Xh:Bijective ghfg:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesthis:AbsConvergent fhbij:Bijective (Exists.choose this)hconv:{ m := 0, seq := fun n if n 0 then (f Exists.choose this) n.toNat else 0, vanish := }.absConverges{ m := 0, seq := fun n if 0 n then f (g n.toNat) else 0, vanish := }.convergesTo { m := 0, seq := fun n if 0 n then f (.choose n.toNat) else 0, vanish := }.sum X:Typef:X g: Xh:Bijective ghfg:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesthis:AbsConvergent fg': X := Exists.choose thishbij:Bijective g'hconv:{ m := 0, seq := fun n if n 0 then (f g') n.toNat else 0, vanish := }.absConverges{ m := 0, seq := fun n if 0 n then f (g n.toNat) else 0, vanish := }.convergesTo { m := 0, seq := fun n if 0 n then f (.choose n.toNat) else 0, vanish := }.sum X:Typef:X g: Xh:Bijective ghfg:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesthis:AbsConvergent fg': X := Exists.choose thishbij:Bijective g'hconv:{ m := 0, seq := fun n if n 0 then (f g') n.toNat else 0, vanish := }.absConvergesg'_inv:X hleft:LeftInverse g'_inv g'hright:RightInverse g'_inv g'{ m := 0, seq := fun n if 0 n then f (g n.toNat) else 0, vanish := }.convergesTo { m := 0, seq := fun n if 0 n then f (.choose n.toNat) else 0, vanish := }.sum X:Typef:X g: Xh:Bijective ghfg:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesthis:AbsConvergent fg': X := Exists.choose thishbij:Bijective g'hconv:{ m := 0, seq := fun n if n 0 then (f g') n.toNat else 0, vanish := }.absConvergesg'_inv:X hleft:LeftInverse g'_inv g'hright:RightInverse g'_inv g'{ m := 0, seq := fun n if 0 n then f (.choose n.toNat) else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.sum X:Typef:X g: Xh:Bijective ghfg:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesthis:AbsConvergent fg': X := Exists.choose thishbij:Bijective g'hconv:{ m := 0, seq := fun n if n 0 then (f g') n.toNat else 0, vanish := }.absConvergesg'_inv:X hleft:LeftInverse g'_inv g'hright:RightInverse g'_inv g'hG:Bijective (g'_inv g){ m := 0, seq := fun n if 0 n then f (.choose n.toNat) else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.sum X:Typef:X g: Xh:Bijective ghfg:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesthis:AbsConvergent fg': X := Exists.choose thishbij:Bijective g'hconv:{ m := 0, seq := fun n if n 0 then (f g') n.toNat else 0, vanish := }.absConvergesg'_inv:X hleft:LeftInverse g'_inv g'hright:RightInverse g'_inv g'hG:Bijective (g'_inv g)n:(if n 0 then (f g) n.toNat else 0) = if n 0 then (fun n (f g') ((g'_inv g) n)) n.toNat else 0 X:Typef:X g: Xh:Bijective ghfg:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesthis:AbsConvergent fg': X := Exists.choose thishbij:Bijective g'hconv:{ m := 0, seq := fun n if n 0 then (f g') n.toNat else 0, vanish := }.absConvergesg'_inv:X hleft:LeftInverse g'_inv g'hright:RightInverse g'_inv g'hG:Bijective (g'_inv g)n:hn:n 0(if n 0 then (f g) n.toNat else 0) = if n 0 then (fun n (f g') ((g'_inv g) n)) n.toNat else 0X:Typef:X g: Xh:Bijective ghfg:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesthis:AbsConvergent fg': X := Exists.choose thishbij:Bijective g'hconv:{ m := 0, seq := fun n if n 0 then (f g') n.toNat else 0, vanish := }.absConvergesg'_inv:X hleft:LeftInverse g'_inv g'hright:RightInverse g'_inv g'hG:Bijective (g'_inv g)n:hn:¬n 0(if n 0 then (f g) n.toNat else 0) = if n 0 then (fun n (f g') ((g'_inv g) n)) n.toNat else 0 X:Typef:X g: Xh:Bijective ghfg:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesthis:AbsConvergent fg': X := Exists.choose thishbij:Bijective g'hconv:{ m := 0, seq := fun n if n 0 then (f g') n.toNat else 0, vanish := }.absConvergesg'_inv:X hleft:LeftInverse g'_inv g'hright:RightInverse g'_inv g'hG:Bijective (g'_inv g)n:hn:n 0(if n 0 then (f g) n.toNat else 0) = if n 0 then (fun n (f g') ((g'_inv g) n)) n.toNat else 0X:Typef:X g: Xh:Bijective ghfg:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesthis:AbsConvergent fg': X := Exists.choose thishbij:Bijective g'hconv:{ m := 0, seq := fun n if n 0 then (f g') n.toNat else 0, vanish := }.absConvergesg'_inv:X hleft:LeftInverse g'_inv g'hright:RightInverse g'_inv g'hG:Bijective (g'_inv g)n:hn:¬n 0(if n 0 then (f g) n.toNat else 0) = if n 0 then (fun n (f g') ((g'_inv g) n)) n.toNat else 0 All goals completed! 🐙theorem Sum.of_comp {X Y:Type} {f:X } (h: AbsConvergent f) {g: Y X} (hbij: Bijective g) : AbsConvergent (f g) Sum f = Sum (f g) := X:TypeY:Typef:X h:AbsConvergent fg:Y Xhbij:Bijective gAbsConvergent (f g) Sum f = Sum (f g) X:TypeY:Typef:X g:Y Xhbij:Bijective gg': Xhbij':Bijective g'hconv':{ m := 0, seq := fun n if n 0 then (f g') n.toNat else 0, vanish := }.absConvergesAbsConvergent (f g) Sum f = Sum (f g) X:TypeY:Typef:X g:Y Xhbij:Bijective gg': Xhbij':Bijective g'hconv':{ m := 0, seq := fun n if n 0 then (f g') n.toNat else 0, vanish := }.absConvergesg_inv:X Yhleft:LeftInverse g_inv ghright:RightInverse g_inv gAbsConvergent (f g) Sum f = Sum (f g) X:TypeY:Typef:X g:Y Xhbij:Bijective gg': Xhbij':Bijective g'hconv':{ m := 0, seq := fun n if n 0 then (f g') n.toNat else 0, vanish := }.absConvergesg_inv:X Yhleft:LeftInverse g_inv ghright:RightInverse g_inv ghbij_g_inv_g':Bijective (g_inv g')AbsConvergent (f g) Sum f = Sum (f g) have hident : (f g) g_inv g' = f g' := X:TypeY:Typef:X h:AbsConvergent fg:Y Xhbij:Bijective gAbsConvergent (f g) Sum f = Sum (f g) X:TypeY:Typef:X g:Y Xhbij:Bijective gg': Xhbij':Bijective g'hconv':{ m := 0, seq := fun n if n 0 then (f g') n.toNat else 0, vanish := }.absConvergesg_inv:X Yhleft:LeftInverse g_inv ghright:RightInverse g_inv ghbij_g_inv_g':Bijective (g_inv g')n:((f g) g_inv g') n = (f g') n; All goals completed! 🐙 refine g_inv g', hbij_g_inv_g', X:TypeY:Typef:X g:Y Xhbij:Bijective gg': Xhbij':Bijective g'hconv':{ m := 0, seq := fun n if n 0 then (f g') n.toNat else 0, vanish := }.absConvergesg_inv:X Yhleft:LeftInverse g_inv ghright:RightInverse g_inv ghbij_g_inv_g':Bijective (g_inv g')hident:(f g) g_inv g' = f g'{ m := 0, seq := fun n if n 0 then ((f g) g_inv g') n.toNat else 0, vanish := }.absConverges All goals completed! 🐙 , ?_ have h := eq (f := f g) hbij_g_inv_g' (X:TypeY:Typef:X g:Y Xhbij:Bijective gg': Xhbij':Bijective g'hconv':{ m := 0, seq := fun n if n 0 then (f g') n.toNat else 0, vanish := }.absConvergesg_inv:X Yhleft:LeftInverse g_inv ghright:RightInverse g_inv ghbij_g_inv_g':Bijective (g_inv g')hident:(f g) g_inv g' = f g'{ m := 0, seq := fun n if n 0 then ((f g) g_inv g') n.toNat else 0, vanish := }.absConverges All goals completed! 🐙) X:TypeY:Typef:X g:Y Xhbij:Bijective gg': Xhbij':Bijective g'hconv':{ m := 0, seq := fun n if n 0 then (f g') n.toNat else 0, vanish := }.absConvergesg_inv:X Yhleft:LeftInverse g_inv ghright:RightInverse g_inv ghbij_g_inv_g':Bijective (g_inv g')hident:(f g) g_inv g' = f g'h:{ m := 0, seq := fun n if n 0 then (f g') n.toNat else 0, vanish := }.convergesTo (Sum (f g))Sum f = Sum (f g) All goals completed! 🐙@[simp] theorem Finset.Icc_eq_cast (N:) : Icc 0 (N:) = map Nat.castEmbedding (.Icc 0 N) := N:Icc 0 N = Finset.map Nat.castEmbedding (Icc 0 N) N:n:n Icc 0 N n Finset.map Nat.castEmbedding (Icc 0 N); N:n:0 n n N a N, a = n; N:n:0 n n N a N, a = nN:n:(∃ a N, a = n) 0 n n N N:n:0 n n N a N, a = n N:n:hn:0 nright✝:n N a N, a = n; N:n:right✝:n N a N, a = n; N:n:right✝:n Nn N n = n; All goals completed! 🐙 N:w✝:left✝:w✝ N0 w✝ w✝ N; All goals completed! 🐙theorem Finset.Icc_empty {N:} (h: ¬ N 0) : Icc 0 N = := N:h:¬N 0Icc 0 N = N:h:¬N 0a✝:a✝ Icc 0 N a✝ ; N:h:¬N 0a✝:0 a✝ N < a✝; N:h:¬N 0a✝¹:a✝:0 a✝¹N < a✝¹; N:a✝¹:a✝:0 a✝¹h:a✝¹ NN 0; All goals completed! 🐙

Theorem 8.2.2, preliminary version. The arguments here are rearranged slightly from the text.

theorem declaration uses `sorry`sum_of_sum_of_AbsConvergent_nonneg {f: × } (hf:AbsConvergent f) (hpos: n m, 0 f (n, m)) : ( n, ((fun m f (n, m)):Series).converges) (fun n ((fun m f (n, m)):Series).sum:Series).convergesTo (Sum f) := f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)(∀ (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.converges) { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum f(∀ (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.converges) { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo L f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }(∀ (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.converges) { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo L have hLpos : 0 L := f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)(∀ (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.converges) { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }0 { m := 0, seq := fun n if 0 n then f (.choose n.toNat) else 0, vanish := }.sum; f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }{ m := 0, seq := fun n if 0 n then f (.choose n.toNat) else 0, vanish := }.nonneg; f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }n:{ m := 0, seq := fun n if 0 n then f (.choose n.toNat) else 0, vanish := }.seq n 0; f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }n:h:n 0{ m := 0, seq := fun n if 0 n then f (.choose n.toNat) else 0, vanish := }.seq n 0f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }n:h:¬n 0{ m := 0, seq := fun n if 0 n then f (.choose n.toNat) else 0, vanish := }.seq n 0 f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }n:h:n 0{ m := 0, seq := fun n if 0 n then f (.choose n.toNat) else 0, vanish := }.seq n 0f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }n:h:¬n 0{ m := 0, seq := fun n if 0 n then f (.choose n.toNat) else 0, vanish := }.seq n 0 All goals completed! 🐙; All goals completed! 🐙 have hfinsum (X: Finset ( × )) : p X, f p L := f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)(∀ (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.converges) { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) All goals completed! 🐙 have hfinsum' (n M:) : (a n).partial M L := f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)(∀ (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.converges) { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Ln:M: x Icc 0 M, f (n, x) L f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Ln:M: x Icc 0 M, f (n, x) = x Finset.map (Embedding.sectR n ) (Icc 0 M), f xf: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Ln:M: x Finset.map (Embedding.sectR n ) (Icc 0 M), f x L f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Ln:M: x Icc 0 M, f (n, x) = x Finset.map (Embedding.sectR n ) (Icc 0 M), f x All goals completed! 🐙 All goals completed! 🐙 have hnon (n:) : (a n).nonneg := f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)(∀ (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.converges) { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Ln: (n_1 : ), 0 if 0 n_1 then f (n, n_1.toNat) else 0; f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Ln:m:0 if 0 m then f (n, m.toNat) else 0; f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Ln:m:h✝:0 m0 f (n, m.toNat)f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Ln:m:h✝:¬0 m0 0 f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Ln:m:h✝:0 m0 f (n, m.toNat)f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Ln:m:h✝:¬0 m0 0 All goals completed! 🐙 have hconv (n:) : (a n).converges := f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)(∀ (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.converges) { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonnegn: M, (N : ), (a n).partial N M f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonnegn: (N : ), (a n).partial N L; f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonnegn:N:(a n).partial N L; f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonnegn:N:h:N 0(a n).partial N Lf: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonnegn:N:h:¬N 0(a n).partial N L f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonnegn:N:h:N 0(a n).partial N L f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonnegn:N:(a n).partial N L; All goals completed! 🐙 f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonnegn:N:h:¬N 00 L; All goals completed! 🐙 have (N M:) : n Icc 0 N, (a n.toNat).partial M L := f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)(∀ (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.converges) { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergesN:M:hN:N 0 n Icc 0 N, (a n.toNat).partial M Lf: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergesN:M:hN:¬N 0 n Icc 0 N, (a n.toNat).partial M L; f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergesN:M:hN:¬N 0 n Icc 0 N, (a n.toNat).partial M Lf: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergesN:M:hN:N 0 n Icc 0 N, (a n.toNat).partial M L f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergesN:M:hN:¬N 0 n Icc 0 N, (a n.toNat).partial M L All goals completed! 🐙 f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergesM:N: n Icc 0 N, (a n.toNat).partial M L f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergesM:N:hM:M 0 n Icc 0 N, (a n.toNat).partial M Lf: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergesM:N:hM:¬M 0 n Icc 0 N, (a n.toNat).partial M L; f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergesM:N:hM:¬M 0 n Icc 0 N, (a n.toNat).partial M Lf: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergesM:N:hM:M 0 n Icc 0 N, (a n.toNat).partial M L f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergesM:N:hM:¬M 0 n Icc 0 N, (a n.toNat).partial M L f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergesM:N:hM:¬M 0 n Icc 0 N, (a n.toNat).partial M = 0; f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergesM:N:hM:¬M 0 n Icc 0 N, n_1 Icc (a n.toNat).m M, (a n.toNat).seq n_1 = 0 f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergesM:N:hM:¬M 0 x Icc 0 N, n Icc (a x.toNat).m M, (a x.toNat).seq n = 0; intro n f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergesM:N:hM:¬M 0n:a✝:n Icc 0 N n_1 Icc (a n.toNat).m M, (a n.toNat).seq n_1 = 0 All goals completed! 🐙 f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergesN:M: n Icc 0 N, (a n.toNat).partial M L f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergesN:M: n Icc 0 N, (a n.toNat).partial M = x Icc 0 N ×ˢ Icc 0 M, f xf: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergesN:M: x Icc 0 N ×ˢ Icc 0 M, f x L f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergesN:M: n Icc 0 N, (a n.toNat).partial M = x Icc 0 N ×ˢ Icc 0 M, f x All goals completed! 🐙 All goals completed! 🐙 replace (N:) : n Icc 0 N, (a n.toNat).sum L := f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)(∀ (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.converges) { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergesthis: (N M : ), n Icc 0 N, (a n.toNat).partial M LN: i Icc 0 N, Tendsto (a i.toNat).partial atTop (nhds (a i.toNat).sum) All goals completed! 🐙 replace (N:) : (fun n (a n).sum:Series).partial N L := f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)(∀ (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.converges) { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergesthis: (N : ), n Icc 0 N, (a n.toNat).sum LN:n:hn:n Icc 0 N{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.seq n = (a n.toNat).sum; All goals completed! 🐙 have hnon' : (fun n (a n).sum:Series).nonneg := f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)(∀ (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.converges) { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergesthis: (N : ), { m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.partial N Ln:{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.seq n 0; f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergesthis: (N : ), { m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.partial N Ln:0 if 0 n then (a n.toNat).sum else 0; f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergesthis: (N : ), { m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.partial N Ln:h✝:0 n0 (a n.toNat).sumf: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergesthis: (N : ), { m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.partial N Ln:h✝:¬0 n0 0 f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergesthis: (N : ), { m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.partial N Ln:h✝:0 n0 (a n.toNat).sum All goals completed! 🐙 All goals completed! 🐙 have hconv' : (fun n (a n).sum:Series).converges := f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)(∀ (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.converges) { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergesthis: (N : ), { m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.partial N Lhnon':{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.nonneg M, (N : ), { m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.partial N M; All goals completed! 🐙 f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergeshnon':{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.nonneghconv':{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.convergesthis:{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.sum L(∀ (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.converges) { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo L replace : (fun n (a n).sum:Series).sum = L := f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)(∀ (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.converges) { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergeshnon':{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.nonneghconv':{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.convergesthis:{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.sum L ε > 0, L - ε { m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.sum; intro ε f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergeshnon':{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.nonneghconv':{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.convergesthis:{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.sum Lε::ε > 0L - ε { m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.sum replace : X, p X, f p L - ε := f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)(∀ (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.converges) { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) All goals completed! 🐙 f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergeshnon':{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.nonneghconv':{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.convergesε::ε > 0X:Finset ( × )hX: p X, f p L - εL - ε { m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.sum have : N, M, X (Icc 0 N) ×ˢ (Icc 0 M) := f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)(∀ (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.converges) { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) All goals completed! 🐙 f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergeshnon':{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.nonneghconv':{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.convergesε::ε > 0X:Finset ( × )hX: p X, f p L - εN:M:hX':X Icc 0 N ×ˢ Icc 0 ML - ε { m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.sum calc _ p X, f p := hX _ p (Icc 0 N) ×ˢ (Icc 0 M), f p := sum_le_sum_of_subset_of_nonneg hX' (f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergeshnon':{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.nonneghconv':{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.convergesε::ε > 0X:Finset ( × )hX: p X, f p L - εN:M:hX':X Icc 0 N ×ˢ Icc 0 M i Icc 0 N ×ˢ Icc 0 M, i X 0 f i All goals completed! 🐙) _ = n Icc 0 N, m Icc 0 M, f (n, m) := sum_product _ _ _ _ n Icc 0 N, (a n).sum := f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergeshnon':{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.nonneghconv':{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.convergesε::ε > 0X:Finset ( × )hX: p X, f p L - εN:M:hX':X Icc 0 N ×ˢ Icc 0 M n Icc 0 N, m Icc 0 M, f (n, m) n Icc 0 N, (a n).sum f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergeshnon':{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.nonneghconv':{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.convergesε::ε > 0X:Finset ( × )hX: p X, f p L - εN:M:hX':X Icc 0 N ×ˢ Icc 0 M i Icc 0 N, m Icc 0 M, f (i, m) (a i).sum; intro n f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergeshnon':{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.nonneghconv':{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.convergesε::ε > 0X:Finset ( × )hX: p X, f p L - εN:M:hX':X Icc 0 N ×ˢ Icc 0 Mn:a✝:n Icc 0 N m Icc 0 M, f (n, m) (a n).sum f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergeshnon':{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.nonneghconv':{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.convergesε::ε > 0X:Finset ( × )hX: p X, f p L - εN:M:hX':X Icc 0 N ×ˢ Icc 0 Mn:a✝:n Icc 0 N m Icc 0 M, f (n, m) = (a n).partial M All goals completed! 🐙 _ = (fun n (a n).sum:Series).partial N := f: × hf:AbsConvergent fhpos: (n m : ), 0 f (n, m)L: := Sum fa: Series := fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }hLpos:0 Lhfinsum: (X : Finset ( × )), p X, f p Lhfinsum': (n M : ), (a n).partial M Lhnon: (n : ), (a n).nonneghconv: (n : ), (a n).convergeshnon':{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.nonneghconv':{ m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.convergesε::ε > 0X:Finset ( × )hX: p X, f p L - εN:M:hX':X Icc 0 N ×ˢ Icc 0 M n Icc 0 N, (a n).sum = { m := 0, seq := fun n if n 0 then (fun n (a n).sum) n.toNat else 0, vanish := }.partial N All goals completed! 🐙 _ _ := partial_le_sum_of_nonneg hnon' hconv' _ All goals completed! 🐙

Theorem 8.2.2, second version

theorem declaration uses `sorry`sum_of_sum_of_AbsConvergent {f: × } (hf:AbsConvergent f) : ( n, ((fun m f (n, m)):Series).absConverges) (fun n ((fun m f (n, m)):Series).sum:Series).convergesTo (Sum f) := f: × hf:AbsConvergent f(∀ (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.absConverges) { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) f: × hf:AbsConvergent ffplus: × := f 0(∀ (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.absConverges) { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0(∀ (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.absConverges) { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) have hfplus_nonneg : n m, 0 fplus (n, m) := f: × hf:AbsConvergent f(∀ (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.absConverges) { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) intro n f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0n:m:0 fplus (n, m); All goals completed! 🐙 have hfminus_nonneg : n m, 0 fminus (n, m) := f: × hf:AbsConvergent f(∀ (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.absConverges) { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) intro n f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)n:m:0 fminus (n, m); All goals completed! 🐙 have hdiff : f = fplus - fminus := f: × hf:AbsConvergent f(∀ (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.absConverges) { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) All goals completed! 🐙 have hfplus_conv : AbsConvergent fplus := f: × hf:AbsConvergent f(∀ (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.absConverges) { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) All goals completed! 🐙 have hfminus_conv : AbsConvergent fminus := f: × hf:AbsConvergent f(∀ (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.absConverges) { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) All goals completed! 🐙 f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)(∀ (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.absConverges) { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus)(∀ (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.absConverges) { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus) (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.absConvergesf: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus){ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus) (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.absConverges f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus)n:{ m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.absConverges All goals completed! 🐙 f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus){ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := } = { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := } - { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus)Sum f = Sum fplus - Sum fminus f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus){ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := } = { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := } - { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := } -- encountered surprising difficulty with definitional equivalence here f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus){ m := 0, seq := fun n if 0 n then { m := 0, seq := fun n_1 if 0 n_1 then fplus (n.toNat, n_1.toNat) - fminus (n.toNat, n_1.toNat) else 0, vanish := }.sum else 0, vanish := } = { m := 0, seq := fun n if 0 n then { m := 0, seq := fun n_1 if 0 n_1 then fplus (n.toNat, n_1.toNat) else 0, vanish := }.sum else 0, vanish := } - { m := 0, seq := fun n if 0 n then { m := 0, seq := fun n_1 if 0 n_1 then fminus (n.toNat, n_1.toNat) else 0, vanish := }.sum else 0, vanish := } f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus){ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m (fplus - fminus) (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := } = { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := } - { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := } f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus){ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := } - { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := } = { m := 0, seq := fun n if n 0 then ((fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) - fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus){ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m (fplus - fminus) (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := } = { m := 0, seq := fun n if n 0 then ((fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) - fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := } f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus){ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := } - { m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := } = { m := 0, seq := fun n if n 0 then ((fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) - fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := } All goals completed! 🐙 f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus)x✝:n:(fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m (fplus - fminus) (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat = ((fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) - fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat; f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus)x✝:n:{ m := 0, seq := fun n_1 if 0 n_1 then fplus (n.toNat, n_1.toNat) - fminus (n.toNat, n_1.toNat) else 0, vanish := }.sum = { m := 0, seq := fun n_1 if 0 n_1 then fplus (n.toNat, n_1.toNat) else 0, vanish := }.sum - { m := 0, seq := fun n_1 if 0 n_1 then fminus (n.toNat, n_1.toNat) else 0, vanish := }.sum f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus)x✝:n:0 = ({ m := 0, seq := fun n_1 if 0 n_1 then fplus (n.toNat, n_1.toNat) else 0, vanish := } - { m := 0, seq := fun n_1 if 0 n_1 then fminus (n.toNat, n_1.toNat) else 0, vanish := }).mf: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus)x✝:n:m:(if 0 m then fplus (n.toNat, m.toNat) - fminus (n.toNat, m.toNat) else 0) = ({ m := 0, seq := fun n_1 if 0 n_1 then fplus (n.toNat, n_1.toNat) else 0, vanish := } - { m := 0, seq := fun n_1 if 0 n_1 then fminus (n.toNat, n_1.toNat) else 0, vanish := }).seq mf: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus)x✝:n:{ m := 0, seq := fun n_1 if 0 n_1 then fplus (n.toNat, n_1.toNat) else 0, vanish := }.convergesf: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus)x✝:n:{ m := 0, seq := fun n_1 if 0 n_1 then fminus (n.toNat, n_1.toNat) else 0, vanish := }.converges; f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus)x✝:n:m:(if 0 m then fplus (n.toNat, m.toNat) - fminus (n.toNat, m.toNat) else 0) = ({ m := 0, seq := fun n_1 if 0 n_1 then fplus (n.toNat, n_1.toNat) else 0, vanish := } - { m := 0, seq := fun n_1 if 0 n_1 then fminus (n.toNat, n_1.toNat) else 0, vanish := }).seq mf: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus)x✝:n:{ m := 0, seq := fun n_1 if 0 n_1 then fplus (n.toNat, n_1.toNat) else 0, vanish := }.convergesf: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus)x✝:n:{ m := 0, seq := fun n_1 if 0 n_1 then fminus (n.toNat, n_1.toNat) else 0, vanish := }.converges f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus)x✝:n:m:h:0 mfplus (n.toNat, m.toNat) - fminus (n.toNat, m.toNat) = ({ m := 0, seq := fun n_1 if 0 n_1 then fplus (n.toNat, n_1.toNat) else 0, vanish := } - { m := 0, seq := fun n_1 if 0 n_1 then fminus (n.toNat, n_1.toNat) else 0, vanish := }).seq mf: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus)x✝:n:m:h:¬0 m0 = ({ m := 0, seq := fun n_1 if 0 n_1 then fplus (n.toNat, n_1.toNat) else 0, vanish := } - { m := 0, seq := fun n_1 if 0 n_1 then fminus (n.toNat, n_1.toNat) else 0, vanish := }).seq m f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus)x✝:n:m:h:0 mfplus (n.toNat, m.toNat) - fminus (n.toNat, m.toNat) = ({ m := 0, seq := fun n_1 if 0 n_1 then fplus (n.toNat, n_1.toNat) else 0, vanish := } - { m := 0, seq := fun n_1 if 0 n_1 then fminus (n.toNat, n_1.toNat) else 0, vanish := }).seq mf: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus)x✝:n:m:h:¬0 m0 = ({ m := 0, seq := fun n_1 if 0 n_1 then fplus (n.toNat, n_1.toNat) else 0, vanish := } - { m := 0, seq := fun n_1 if 0 n_1 then fminus (n.toNat, n_1.toNat) else 0, vanish := }).seq m All goals completed! 🐙 f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus)x✝:n:{ m := 0, seq := fun n_1 if 0 n_1 then fplus (n.toNat, n_1.toNat) else 0, vanish := }.converges All goals completed! 🐙 All goals completed! 🐙 f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus)g: × hg:Bijective gright✝:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesSum f = Sum fplus - Sum fminus f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus)g: × hg:Bijective gright✝:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesh1:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.convergesTo (Sum f)Sum f = Sum fplus - Sum fminus f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus)g: × hg:Bijective gright✝:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesh1:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.convergesTo (Sum f)hplus:{ m := 0, seq := fun n if n 0 then (fplus g) n.toNat else 0, vanish := }.convergesTo (Sum fplus)Sum f = Sum fplus - Sum fminus f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus)g: × hg:Bijective gright✝:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesh1:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.convergesTo (Sum f)hplus:{ m := 0, seq := fun n if n 0 then (fplus g) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hminus:{ m := 0, seq := fun n if n 0 then (fminus g) n.toNat else 0, vanish := }.convergesTo (Sum fminus)Sum f = Sum fplus - Sum fminus f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus)g: × hg:Bijective gright✝:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesh1:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.convergesTo (Sum f)hplus:{ m := 0, seq := fun n if n 0 then (fplus g) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hminus:{ m := 0, seq := fun n if n 0 then (fminus g) n.toNat else 0, vanish := }.convergesTo (Sum fminus){ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.convergesTo (Sum fplus - Sum fminus) f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus)g: × hg:Bijective gright✝:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesh1:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.convergesTo (Sum f)hplus:{ m := 0, seq := fun n if n 0 then (fplus g) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hminus:{ m := 0, seq := fun n if n 0 then (fminus g) n.toNat else 0, vanish := }.convergesTo (Sum fminus)n:(if n 0 then (f g) n.toNat else 0) = ({ m := 0, seq := fun n if n 0 then (fplus g) n.toNat else 0, vanish := } - { m := 0, seq := fun n if n 0 then (fminus g) n.toNat else 0, vanish := }).seq n f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus)g: × hg:Bijective gright✝:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesh1:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.convergesTo (Sum f)hplus:{ m := 0, seq := fun n if n 0 then (fplus g) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hminus:{ m := 0, seq := fun n if n 0 then (fminus g) n.toNat else 0, vanish := }.convergesTo (Sum fminus)n:h:n 0(f g) n.toNat = ({ m := 0, seq := fun n if n 0 then (fplus g) n.toNat else 0, vanish := } - { m := 0, seq := fun n if n 0 then (fminus g) n.toNat else 0, vanish := }).seq nf: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus)g: × hg:Bijective gright✝:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesh1:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.convergesTo (Sum f)hplus:{ m := 0, seq := fun n if n 0 then (fplus g) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hminus:{ m := 0, seq := fun n if n 0 then (fminus g) n.toNat else 0, vanish := }.convergesTo (Sum fminus)n:h:¬n 00 = ({ m := 0, seq := fun n if n 0 then (fplus g) n.toNat else 0, vanish := } - { m := 0, seq := fun n if n 0 then (fminus g) n.toNat else 0, vanish := }).seq n f: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus)g: × hg:Bijective gright✝:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesh1:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.convergesTo (Sum f)hplus:{ m := 0, seq := fun n if n 0 then (fplus g) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hminus:{ m := 0, seq := fun n if n 0 then (fminus g) n.toNat else 0, vanish := }.convergesTo (Sum fminus)n:h:n 0(f g) n.toNat = ({ m := 0, seq := fun n if n 0 then (fplus g) n.toNat else 0, vanish := } - { m := 0, seq := fun n if n 0 then (fminus g) n.toNat else 0, vanish := }).seq nf: × hf:AbsConvergent ffplus: × := f 0fminus: × := -f 0hfplus_nonneg: (n m : ), 0 fplus (n, m)hfminus_nonneg: (n m : ), 0 fminus (n, m)hdiff:f = fplus - fminushfplus_conv:AbsConvergent fplushfminus_conv:AbsConvergent fminushfplus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.convergeshfplus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fplus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hfminus_conv': (n : ), { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.convergeshfminus_sum:{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m fminus (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum fminus)g: × hg:Bijective gright✝:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesh1:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.convergesTo (Sum f)hplus:{ m := 0, seq := fun n if n 0 then (fplus g) n.toNat else 0, vanish := }.convergesTo (Sum fplus)hminus:{ m := 0, seq := fun n if n 0 then (fminus g) n.toNat else 0, vanish := }.convergesTo (Sum fminus)n:h:¬n 00 = ({ m := 0, seq := fun n if n 0 then (fplus g) n.toNat else 0, vanish := } - { m := 0, seq := fun n if n 0 then (fminus g) n.toNat else 0, vanish := }).seq n All goals completed! 🐙

Theorem 8.2.2, third version

theorem sum_of_sum_of_AbsConvergent' {f: × } (hf:AbsConvergent f) : ( m, ((fun n f (n, m)):Series).absConverges) (fun m ((fun n f (n, m)):Series).sum:Series).convergesTo (Sum f) := f: × hf:AbsConvergent f(∀ (m : ), { m := 0, seq := fun n if n 0 then (fun n f (n, m)) n.toNat else 0, vanish := }.absConverges) { m := 0, seq := fun n if n 0 then (fun m { m := 0, seq := fun n if n 0 then (fun n f (n, m)) n.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) f: × hf:AbsConvergent fπ: × × := fun p (p.2, p.1)(∀ (m : ), { m := 0, seq := fun n if n 0 then (fun n f (n, m)) n.toNat else 0, vanish := }.absConverges) { m := 0, seq := fun n if n 0 then (fun m { m := 0, seq := fun n if n 0 then (fun n f (n, m)) n.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) f: × hf:AbsConvergent fπ: × × := fun p (p.2, p.1):Bijective π(∀ (m : ), { m := 0, seq := fun n if n 0 then (fun n f (n, m)) n.toNat else 0, vanish := }.absConverges) { m := 0, seq := fun n if n 0 then (fun m { m := 0, seq := fun n if n 0 then (fun n f (n, m)) n.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) f: × hf:AbsConvergent fπ: × × := fun p (p.2, p.1):Bijective πg: × hg:Bijective ghconv:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConverges(∀ (m : ), { m := 0, seq := fun n if n 0 then (fun n f (n, m)) n.toNat else 0, vanish := }.absConverges) { m := 0, seq := fun n if n 0 then (fun m { m := 0, seq := fun n if n 0 then (fun n f (n, m)) n.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.convergesTo (Sum f) f: × hf:AbsConvergent fπ: × × := fun p (p.2, p.1):Bijective πg: × hg:Bijective ghconv:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesSum f = Sum (f π)f: × hf:AbsConvergent fπ: × × := fun p (p.2, p.1):Bijective πg: × hg:Bijective ghconv:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesAbsConvergent (f π) f: × hf:AbsConvergent fπ: × × := fun p (p.2, p.1):Bijective πg: × hg:Bijective ghconv:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConvergesSum f = Sum (f π) All goals completed! 🐙 f: × hf:AbsConvergent fπ: × × := fun p (p.2, p.1):Bijective πg: × hg:Bijective ghconv:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConverges{ m := 0, seq := fun n if n 0 then ((f π) π g) n.toNat else 0, vanish := }.absConverges All goals completed! 🐙

Theorem 8.2.2, fourth version

theorem sum_comm {f: × } (hf:AbsConvergent f) : (fun n ((fun m f (n, m)):Series).sum:Series).sum = (fun m ((fun n f (n, m)):Series).sum:Series).sum := f: × hf:AbsConvergent f{ m := 0, seq := fun n if n 0 then (fun n { m := 0, seq := fun n_1 if n_1 0 then (fun m f (n, m)) n_1.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (fun m { m := 0, seq := fun n if n 0 then (fun n f (n, m)) n.toNat else 0, vanish := }.sum) n.toNat else 0, vanish := }.sum All goals completed! 🐙

Lemma 8.2.3 / Exercise 8.2.1

theorem declaration uses `sorry`AbsConvergent.iff {X:Type} (hX:CountablyInfinite X) (f : X ) : AbsConvergent f BddAbove ( (fun A x A, |f x|) '' .univ ) := X:TypehX:CountablyInfinite Xf:X AbsConvergent f BddAbove ((fun A x A, |f x|) '' Set.univ) All goals completed! 🐙
abbrev AbsConvergent' {X:Type} (f: X ) : Prop := BddAbove ( (fun A x A, |f x|) '' .univ )theorem AbsConvergent'.of_finite {X:Type} [Finite X] (f:X ) : AbsConvergent' f := X:Typeinst✝:Finite Xf:X AbsConvergent' f X:Typeinst✝:Finite Xf:X x✝:Fintype XAbsConvergent' f X:Typeinst✝:Finite Xf:X x✝:Fintype X x, (a : Finset X), x a, |f x| x; X:Typeinst✝:Finite Xf:X x✝:Fintype X (a : Finset X), x a, |f x| x, |f x|; X:Typeinst✝:Finite Xf:X x✝:Fintype XA:Finset X x A, |f x| x, |f x|; X:Typeinst✝:Finite Xf:X x✝:Fintype XA:Finset X (x : X), 0 |f x|; All goals completed! 🐙

Not in textbook, but should have been included.

theorem AbsConvergent'.of_countable {X:Type} (hX:CountablyInfinite X) {f:X } : AbsConvergent' f AbsConvergent f := X:TypehX:CountablyInfinite Xf:X AbsConvergent' f AbsConvergent f X:TypehX:CountablyInfinite Xf:X AbsConvergent' f AbsConvergent fX:TypehX:CountablyInfinite Xf:X AbsConvergent f AbsConvergent' f X:TypehX:CountablyInfinite Xf:X AbsConvergent' f AbsConvergent f X:TypehX:CountablyInfinite Xf:X hf:AbsConvergent' fAbsConvergent f; X:TypehX:CountablyInfinite Xf:X hf: x, (a : Finset X), x a, |f x| xAbsConvergent f; X:TypehX:CountablyInfinite Xf:X L:hL: (a : Finset X), x a, |f x| LAbsConvergent f X:TypehX:CountablyInfinite Xf:X L:hL: (a : Finset X), x a, |f x| Lg: Xhg:Bijective gAbsConvergent f; X:TypehX:CountablyInfinite Xf:X L:hL: (a : Finset X), x a, |f x| Lg: Xhg:Bijective g{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.absConverges X:TypehX:CountablyInfinite Xf:X L:hL: (a : Finset X), x a, |f x| Lg: Xhg:Bijective g{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.abs.converges; X:TypehX:CountablyInfinite Xf:X L:hL: (a : Finset X), x a, |f x| Lg: Xhg:Bijective g M, (N : ), { m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.abs.partial N MX:TypehX:CountablyInfinite Xf:X L:hL: (a : Finset X), x a, |f x| Lg: Xhg:Bijective g{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.abs.nonneg X:TypehX:CountablyInfinite Xf:X L:hL: (a : Finset X), x a, |f x| Lg: Xhg:Bijective g M, (N : ), { m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.abs.partial N M X:TypehX:CountablyInfinite Xf:X L:hL: (a : Finset X), x a, |f x| Lg: Xhg:Bijective g (N : ), { m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.abs.partial N L; X:TypehX:CountablyInfinite Xf:X L:hL: (a : Finset X), x a, |f x| Lg: Xhg:Bijective gN:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.abs.partial N L; X:TypehX:CountablyInfinite Xf:X L:hL: (a : Finset X), x a, |f x| Lg: Xhg:Bijective gN:hN:N 0{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.abs.partial N LX:TypehX:CountablyInfinite Xf:X L:hL: (a : Finset X), x a, |f x| Lg: Xhg:Bijective gN:hN:¬N 0{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.abs.partial N L X:TypehX:CountablyInfinite Xf:X L:hL: (a : Finset X), x a, |f x| Lg: Xhg:Bijective gN:hN:N 0{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.abs.partial N L X:TypehX:CountablyInfinite Xf:X L:hL: (a : Finset X), x a, |f x| Lg: Xhg:Bijective gN:{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.abs.partial N L X:TypehX:CountablyInfinite Xf:X L:hL: (a : Finset X), x a, |f x| Lg: Xhg:Bijective gN:g': X := { toFun := g, inj' := }{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.abs.partial N L X:TypehX:CountablyInfinite Xf:X L:hL: (a : Finset X), x a, |f x| Lg: Xhg:Bijective gN:g': X := { toFun := g, inj' := }{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.abs.partial N = x Finset.map g' (Icc 0 N), |f x| X:TypehX:CountablyInfinite Xf:X L:hL: (a : Finset X), x a, |f x| Lg: Xhg:Bijective gN:g': X := { toFun := g, inj' := } x Icc 0 N, |f (g x)| = x Icc 0 N, |f (g' x)|; All goals completed! 🐙 X:TypehX:CountablyInfinite Xf:X L:hL: (a : Finset X), x a, |f x| Lg: Xhg:Bijective gN:hN:¬N 0{ m := 0, seq := fun n if n 0 then (f g) n.toNat else 0, vanish := }.abs.partial N = x , |f x| X:TypehX:CountablyInfinite Xf:X L:hL: (a : Finset X), x a, |f x| Lg: Xhg:Bijective gN:hN:¬N 0{ m := 0, seq := fun n if 0 n then f (g n.toNat) else 0, vanish := }.abs.partial N = 0; X:TypehX:CountablyInfinite Xf:X L:hL: (a : Finset X), x a, |f x| Lg: Xhg:Bijective gN:hN:¬N 0N < { m := 0, seq := fun n if 0 n then f (g n.toNat) else 0, vanish := }.abs.m; All goals completed! 🐙 X:TypehX:CountablyInfinite Xf:X L:hL: (a : Finset X), x a, |f x| Lg: Xhg:Bijective g (n : ), 0 if 0 n then |if 0 n then f (g n.toNat) else 0| else 0 X:TypehX:CountablyInfinite Xf:X L:hL: (a : Finset X), x a, |f x| Lg: Xhg:Bijective gn:0 if 0 n then |if 0 n then f (g n.toNat) else 0| else 0; X:TypehX:CountablyInfinite Xf:X L:hL: (a : Finset X), x a, |f x| Lg: Xhg:Bijective gn:h:n 00 if 0 n then |if 0 n then f (g n.toNat) else 0| else 0X:TypehX:CountablyInfinite Xf:X L:hL: (a : Finset X), x a, |f x| Lg: Xhg:Bijective gn:h:¬n 00 if 0 n then |if 0 n then f (g n.toNat) else 0| else 0 X:TypehX:CountablyInfinite Xf:X L:hL: (a : Finset X), x a, |f x| Lg: Xhg:Bijective gn:h:n 00 if 0 n then |if 0 n then f (g n.toNat) else 0| else 0X:TypehX:CountablyInfinite Xf:X L:hL: (a : Finset X), x a, |f x| Lg: Xhg:Bijective gn:h:¬n 00 if 0 n then |if 0 n then f (g n.toNat) else 0| else 0 All goals completed! 🐙 X:TypehX:CountablyInfinite Xf:X hf:AbsConvergent fAbsConvergent' f; rwa [AbsConvergent.iff hX fX:TypehX:CountablyInfinite Xf:X hf:BddAbove ((fun A x A, |f x|) '' Set.univ)AbsConvergent' f at hf

Lemma 8.2.5 / Exercise 8.2.2

theorem declaration uses `sorry`AbsConvergent'.countable_supp {X:Type} {f:X } (hf: AbsConvergent' f) : AtMostCountable { x | f x 0 } := X:Typef:X hf:AbsConvergent' fAtMostCountable {x | f x 0} All goals completed! 🐙

Compare with Mathlib's Summable.­subtype

theorem AbsConvergent'.subtype {X:Type} {f:X } (hf: AbsConvergent' f) (A: Set X) : AbsConvergent' (fun x:A f x) := X:Typef:X hf:AbsConvergent' fA:Set XAbsConvergent' fun x f x X:Typef:X hf:AbsConvergent' fA:Set X(fun A_1 x A_1, |(fun x f x) x|) '' Set.univ (fun A x A, |f x|) '' Set.univ intro z X:Typef:X hf:AbsConvergent' fA:Set Xz:hz:z (fun A_1 x A_1, |(fun x f x) x|) '' Set.univz (fun A x A, |f x|) '' Set.univ; X:Typef:X hf:AbsConvergent' fA:Set Xz:hz: y, x y, |f x| = z y, x y, |f x| = z; X:Typef:X hf:AbsConvergent' fA✝:Set Xz:A:Finset A✝hA: x A, |f x| = z y, x y, |f x| = z X:Typef:X hf:AbsConvergent' fA✝:Set Xz:A:Finset A✝hA: x A, |f x| = z x Finset.map (Embedding.subtype fun x x A✝) A, |f x| = z; All goals completed! 🐙

A generalized sum. Note that this will give junk values if f is not AbsConvergent'.

noncomputable abbrev Sum' {X:Type} (f: X ) : := Sum (fun x : { x | f x 0 } f x)

Not in textbook, but should have been included (the series laws are significantly harder to establish without this)

theorem Sum'.of_finsupp {X:Type} {f:X } {A: Finset X} (h: x A, f x = 0) : Sum' f = x A, f x := X:Typef:X A:Finset Xh: x A, f x = 0Sum' f = x A, f x X:Typef:X A:Finset Xh: x A, f x = 0(Sum fun x f x) = x A, f x X:Typef:X A:Finset Xh: x A, f x = 0E:Set X := {x | f x 0}(Sum fun x f x) = x A, f x have hE : E A := X:Typef:X A:Finset Xh: x A, f x = 0Sum' f = x A, f x X:Typef:X A:Finset Xh: x A, f x = 0E:Set X := {x | f x 0}a✝:Xa✝ E a✝ A; X:Typef:X A:Finset Xh: x A, f x = 0E:Set X := {x | f x 0}a✝:X¬f a✝ = 0 a✝ A; All goals completed! 🐙 X:Typef:X A:Finset Xh: x A, f x = 0E:Set X := {x | f x 0}hE:E Ahfin:Finite E(Sum fun x f x) = x A, f x X:Typef:X A:Finset Xh: x A, f x = 0E:Set X := {x | f x 0}hE:E Ahfin:Finite EE':Finset X := .toFinset(Sum fun x f x) = x A, f x X:Typef:X A:Finset Xh: x A, f x = 0E:Set X := {x | f x 0}hE:E Ahfin:Finite EE':Finset X := .toFinset a E', f a = x A, f x replace hE : E' A := X:Typef:X A:Finset Xh: x A, f x = 0Sum' f = x A, f x All goals completed! 🐙 X:Typef:X A:Finset Xh: x A, f x = 0E:Set X := {x | f x 0}hfin:Finite EE':Finset X := .toFinsethE:E' A x A, x E' f x = 0; All goals completed! 🐙

Not in textbook, but should have been included (the series laws are significantly harder to establish without this)

theorem Sum'.of_countable_supp {X:Type} {f:X } {A: Set X} (hA: CountablyInfinite A) (hfA : x A, f x = 0) (hconv: AbsConvergent' f): AbsConvergent' (fun x:A f x) Sum' f = Sum (fun x:A f x) := X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' f(AbsConvergent' fun x f x) Sum' f = Sum fun x f x -- We can adapt the proof of `AbsConvergent'.of_countable` to establish absolute convergence on A. X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f x(AbsConvergent' fun x f x) Sum' f = Sum fun x f x X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f x(AbsConvergent fun x f x) Sum' f = Sum fun x f x X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xSum' f = Sum fun x f x X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}Sum' f = Sum fun x f x -- The main challenge here is to relate a sum on E with a sum on A. First, we show containment. have hE : E A := X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' f(AbsConvergent' fun x f x) Sum' f = Sum fun x f x X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}a✝:Xa✝ E a✝ A; X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}a✝:X¬f a✝ = 0 a✝ A; X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}a✝:Xthis:f a✝ 0 a✝ AFalse; All goals completed! 🐙 -- Now, we map A back to the natural numbers, thus identifying E with a subset E' of ℕ. X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective gSum' f = Sum fun x f x X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)Sum' f = Sum fun x f x X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}Sum' f = Sum fun x f x set ι : E' E := fun n, hn g n, X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}x✝:E'n:hn:n E'(g n) E All goals completed! 🐙 have : Bijective ι := X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' f(AbsConvergent' fun x f x) Sum' f = Sum fun x f x X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), Injective ιX:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), Surjective ι X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), Injective ι intro _, _ X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), val✝¹:property✝¹:val✝¹ E'val✝:property✝:val✝ E'ι val✝¹, property✝¹ = ι val✝, property✝ val✝¹, property✝¹ = val✝, property✝ X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), val✝¹:property✝¹:val✝¹ E'val✝:property✝:val✝ E'h:ι val✝¹, property✝¹ = ι val✝, property✝val✝¹, property✝¹ = val✝, property✝; X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective gE':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), val✝¹:property✝¹:val✝¹ E'val✝:property✝:val✝ E'hsum:{ m := 0, seq := fun n if 0 n then f (g n.toNat) else 0, vanish := }.convergesTo (Sum fun x f x)h:g val✝¹ = g val✝val✝¹ = val✝; All goals completed! 🐙 X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), Surjective ι X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), x:Xhx:x E a, ι a = x, hx; X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), x:Xhx:x En:hn:g n = x, a, ι a = x, hx; use n, X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), x:Xhx:x En:hn:g n = x, n E' All goals completed! 🐙 ; All goals completed! 🐙 -- The cases of infinite and finite E' are handled separately. X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'Sum' f = Sum fun x f xX:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':Finite E'Sum' f = Sum fun x f x X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'Sum' f = Sum fun x f x -- use Nat.monotone_enum_of_infinite to enumerate E' -- show the partial sums of E' are a subsequence of the partial sums of A X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···Sum' f = Sum fun x f x X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono aSum' f = Sum fun x f x have : atTop.Tendsto (Nat.cast Subtype.val a: ) atTop := X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' f(AbsConvergent' fun x f x) Sum' f = Sum fun x f x X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono aStrictMono (Subtype.val a) intro _ X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono aa✝:b✝:a✝ < b✝ (Subtype.val a) a✝ < (Subtype.val a) b✝ X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono aa✝:b✝:hnm:a✝ < b✝(Subtype.val a) a✝ < (Subtype.val a) b✝; All goals completed! 🐙 X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono athis:Tendsto (Nat.cast Subtype.val a) atTop atTopTendsto ({ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.partial Nat.cast Subtype.val a) atTop (nhds (Sum' f)) have hconv'' : AbsConvergent (fun x:E f x) := X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' f(AbsConvergent' fun x f x) Sum' f = Sum fun x f x X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono athis:Tendsto (Nat.cast Subtype.val a) atTop atTopAbsConvergent' fun x f xX:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono athis:Tendsto (Nat.cast Subtype.val a) atTop atTopCountablyInfinite E X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono athis:Tendsto (Nat.cast Subtype.val a) atTop atTopAbsConvergent' fun x f x All goals completed! 🐙 X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono athis:Tendsto (Nat.cast Subtype.val a) atTop atTopEqualCard E' E; All goals completed! 🐙 X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)Tendsto ({ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.partial Nat.cast Subtype.val a) atTop (nhds (Sum' f)) X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x){ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.partial Nat.cast Subtype.val a = { m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.partial Nat.cast; X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)N:({ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.partial Nat.cast Subtype.val a) N = ({ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.partial Nat.cast) N X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)N: x Icc 0 (a N), f (g x) = x Icc 0 N, f (g (a x)) calc _ = x .image (Subtype.val a) (.Icc 0 N), f (g x) := X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)N: x Icc 0 (a N), f (g x) = x image (Subtype.val a) (Icc 0 N), f (g x) X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)N: x image (Subtype.val a) (Icc 0 N), f (g x) = x Icc 0 (a N), f (g x); X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)N:image (Subtype.val a) (Icc 0 N) Icc 0 (a N)X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)N: x Icc 0 (a N), x image (Subtype.val a) (Icc 0 N) f (g x) = 0 X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)N:image (Subtype.val a) (Icc 0 N) Icc 0 (a N) intro m X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)N:m:hm:m image (Subtype.val a) (Icc 0 N)m Icc 0 (a N); X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)N:m:hm: a_1 N, (a a_1) = mm (a N); X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)N:n:hn:n N(a n) (a N) All goals completed! 🐙 intro x X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)N:x:hx:x Icc 0 (a N)x image (Subtype.val a) (Icc 0 N) f (g x) = 0 X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)N:x:hx:x Icc 0 (a N)hx':x image (Subtype.val a) (Icc 0 N)f (g x) = 0; X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)N:x:hx:x (a N)hx': x_1 N, ¬(a x_1) = xf (g x) = 0; X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)N:x:hx:x (a N)hx':f (g x) 0 x_1 N, (a x_1) = x X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)N:x:hx:x (a N)hx':f (g x) 0n:hn:(ι a) n = (g x), hx' x_1 N, (a x_1) = x X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)N:x:hx:x (a N)hx':f (g x) 0n:hn:g (a n) = g x x_1 N, (a x_1) = x X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)N:x:hx:x (a N)hx':f (g x) 0n:hn:(a n) = x x_1 N, (a x_1) = x; X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)N:n:hx:(a n) (a N)hx':f (g (a n)) 0 x N, (a x) = (a n) X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)N:n:hx:(a n) (a N)hx':f (g (a n)) 0n N (a n) = (a n); All goals completed! 🐙 _ = _ := X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)N: x image (Subtype.val a) (Icc 0 N), f (g x) = x Icc 0 N, f (g (a x)) X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)N:Set.InjOn (Subtype.val a) (Icc 0 N) intro _ X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)N:x₁✝:a✝:x₁✝ (Icc 0 N) x₂ : ⦄, x₂ (Icc 0 N) (Subtype.val a) x₁✝ = (Subtype.val a) x₂ x₁✝ = x₂ X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)N:x₁✝:a✝:x₁✝ (Icc 0 N)x₂✝:x₂✝ (Icc 0 N) (Subtype.val a) x₁✝ = (Subtype.val a) x₂✝ x₁✝ = x₂✝ X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)N:x₁✝:a✝¹:x₁✝ (Icc 0 N)x₂✝:a✝:x₂✝ (Icc 0 N)(Subtype.val a) x₁✝ = (Subtype.val a) x₂✝ x₁✝ = x₂✝ X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)N:x₁✝:a✝¹:x₁✝ (Icc 0 N)x₂✝:a✝:x₂✝ (Icc 0 N)h:(Subtype.val a) x₁✝ = (Subtype.val a) x₂✝x₁✝ = x₂✝; X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':CountablyInfinite E'hinf:Infinite E' := ···a: E'ha_bij:Bijective aha_mono:StrictMono ahconv'':AbsConvergent fun x f xthis:{ m := 0, seq := fun n if n 0 then ((fun x f x) ι a) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)N:x₁✝:a✝¹:x₁✝ (Icc 0 N)x₂✝:a✝:x₂✝ (Icc 0 N)h:a x₁✝ = a x₂✝x₁✝ = x₂✝; All goals completed! 🐙 -- When E' is finite, we show that all sufficiently large partial sums of A are equal to -- the sum of E'. X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':Finite E'hEfin:Finite E := ···Sum' f = Sum fun x f x X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':Finite E'hEfin:Finite E := ···hE'fintype:Fintype E' := Fintype.ofFinite E'Sum' f = Sum fun x f x X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':Finite E'hEfin:Finite E := ···hE'fintype:Fintype E' := Fintype.ofFinite E'hEfintype:Fintype E := Fintype.ofFinite ESum' f = Sum fun x f x X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':Finite E'hEfin:Finite E := ···hE'fintype:Fintype E' := Fintype.ofFinite E'hEfintype:Fintype E := Fintype.ofFinite E{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum' f) X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':Finite E'hEfin:Finite E := ···hE'fintype:Fintype E' := Fintype.ofFinite E'hEfintype:Fintype E := Fintype.ofFinite ETendsto { m := 0, seq := fun n if 0 n then f (g n.toNat) else 0, vanish := }.partial atTop (nhds (∑ x, f x)) X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':Finite E'hEfin:Finite E := ···hE'fintype:Fintype E' := Fintype.ofFinite E'hEfintype:Fintype E := Fintype.ofFinite E∀ᶠ (x' : ) in atTop, { m := 0, seq := fun n if 0 n then f (g n.toNat) else 0, vanish := }.partial x' = x, f x X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':Finite E'hEfin:Finite E := ···hE'fintype:Fintype E' := Fintype.ofFinite E'hEfintype:Fintype E := Fintype.ofFinite EhE'bound:BddAbove E'∀ᶠ (x' : ) in atTop, { m := 0, seq := fun n if 0 n then f (g n.toNat) else 0, vanish := }.partial x' = x, f x X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':Finite E'hEfin:Finite E := ···hE'fintype:Fintype E' := Fintype.ofFinite E'hEfintype:Fintype E := Fintype.ofFinite EhE'bound: x, y E', y x∀ᶠ (x' : ) in atTop, { m := 0, seq := fun n if 0 n then f (g n.toNat) else 0, vanish := }.partial x' = x, f x; X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':Finite E'hEfin:Finite E := ···hE'fintype:Fintype E' := Fintype.ofFinite E'hEfintype:Fintype E := Fintype.ofFinite EN:hN: y E', y N∀ᶠ (x' : ) in atTop, { m := 0, seq := fun n if 0 n then f (g n.toNat) else 0, vanish := }.partial x' = x, f x X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':Finite E'hEfin:Finite E := ···hE'fintype:Fintype E' := Fintype.ofFinite E'hEfintype:Fintype E := Fintype.ofFinite EN:hN: y E', y N a, b a, { m := 0, seq := fun n if 0 n then f (g n.toNat) else 0, vanish := }.partial b = x, f x X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':Finite E'hEfin:Finite E := ···hE'fintype:Fintype E' := Fintype.ofFinite E'hEfintype:Fintype E := Fintype.ofFinite EN:hN: y E', y N b N, { m := 0, seq := fun n if 0 n then f (g n.toNat) else 0, vanish := }.partial b = x, f x; intro N' X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':Finite E'hEfin:Finite E := ···hE'fintype:Fintype E' := Fintype.ofFinite E'hEfintype:Fintype E := Fintype.ofFinite EN:hN: y E', y NN':hN':N' N{ m := 0, seq := fun n if 0 n then f (g n.toNat) else 0, vanish := }.partial N' = x, f x lift N' to using (LE.le.trans (X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':Finite E'hEfin:Finite E := ···hE'fintype:Fintype E' := Fintype.ofFinite E'hEfintype:Fintype E := Fintype.ofFinite EN:hN: y E', y NN':hN':N' N0 N All goals completed! 🐙) hN') X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':Finite E'hEfin:Finite E := ···hE'fintype:Fintype E' := Fintype.ofFinite E'hEfintype:Fintype E := Fintype.ofFinite EN:hN: y E', y NN':hN':N N' x Icc 0 N', f (g x) = x, f x calc _ = n E', f (g n) := X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':Finite E'hEfin:Finite E := ···hE'fintype:Fintype E' := Fintype.ofFinite E'hEfintype:Fintype E := Fintype.ofFinite EN:hN: y E', y NN':hN':N N' x Icc 0 N', f (g x) = n E'.toFinset, f (g n) X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':Finite E'hEfin:Finite E := ···hE'fintype:Fintype E' := Fintype.ofFinite E'hEfintype:Fintype E := Fintype.ofFinite EN:hN: y E', y NN':hN':N N' n E'.toFinset, f (g n) = x Icc 0 N', f (g x); X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':Finite E'hEfin:Finite E := ···hE'fintype:Fintype E' := Fintype.ofFinite E'hEfintype:Fintype E := Fintype.ofFinite EN:hN: y E', y NN':hN':N N'E'.toFinset Icc 0 N'X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':Finite E'hEfin:Finite E := ···hE'fintype:Fintype E' := Fintype.ofFinite E'hEfintype:Fintype E := Fintype.ofFinite EN:hN: y E', y NN':hN':N N' x Icc 0 N', x E'.toFinset f (g x) = 0 X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':Finite E'hEfin:Finite E := ···hE'fintype:Fintype E' := Fintype.ofFinite E'hEfintype:Fintype E := Fintype.ofFinite EN:hN: y E', y NN':hN':N N'E'.toFinset Icc 0 N' intro x X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':Finite E'hEfin:Finite E := ···hE'fintype:Fintype E' := Fintype.ofFinite E'hEfintype:Fintype E := Fintype.ofFinite EN:hN: y E', y NN':hN':N N'x:hx:x E'.toFinsetx Icc 0 N'; X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective gE':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':Finite E'hEfin:Finite E := ···hE'fintype:Fintype E' := Fintype.ofFinite E'hEfintype:Fintype E := Fintype.ofFinite EN:hN: y E', y NN':hN':N N'x:hsum:{ m := 0, seq := fun n if 0 n then f (g n.toNat) else 0, vanish := }.convergesTo (Sum fun x f x)hx:x E'x N'; All goals completed! 🐙 intro _ X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':Finite E'hEfin:Finite E := ···hE'fintype:Fintype E' := Fintype.ofFinite E'hEfintype:Fintype E := Fintype.ofFinite EN:hN: y E', y NN':hN':N N'x✝:a✝:x✝ Icc 0 N'x✝ E'.toFinset f (g x✝) = 0 X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':Finite E'hEfin:Finite E := ···hE'fintype:Fintype E' := Fintype.ofFinite E'hEfintype:Fintype E := Fintype.ofFinite EN:hN: y E', y NN':hN':N N'x✝:a✝:x✝ Icc 0 N'hx':x✝ E'.toFinsetf (g x✝) = 0; All goals completed! 🐙 _ = n:E', f (g n) := X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':Finite E'hEfin:Finite E := ···hE'fintype:Fintype E' := Fintype.ofFinite E'hEfintype:Fintype E := Fintype.ofFinite EN:hN: y E', y NN':hN':N N' n E'.toFinset, f (g n) = n, f (g n) All goals completed! 🐙 _ = n, f (ι n) := sum_congr rfl (X:Typef:X A:Set XhA:CountablyInfinite AhfA: x A, f x = 0hconv:AbsConvergent' fhconv':AbsConvergent fun x f xE:Set X := {x | f x 0}hE:E Ag: Ahg:Bijective ghsum:{ m := 0, seq := fun n if n 0 then ((fun x f x) g) n.toNat else 0, vanish := }.convergesTo (Sum fun x f x)E':Set := {n | (g n) E}ι:E' E := fun x match x with | n, hn => (g n), :Bijective ιhE':Finite E'hEfin:Finite E := ···hE'fintype:Fintype E' := Fintype.ofFinite E'hEfintype:Fintype E := Fintype.ofFinite EN:hN: y E', y NN':hN':N N' x univ, f (g x) = f (ι x) All goals completed! 🐙) _ = _ := .sum_comp (g := fun x f x)

Connection with Mathlib's Summable property. Some version of this might be suitable for Mathlib?

theorem AbsConvergent'.iff_Summable {X:Type} (f:X ) : AbsConvergent' f Summable f := X:Typef:X AbsConvergent' f Summable f X:Typef:X BddAbove (Set.range fun A x A, |f x|) Summable fun x |(|f x|)| X:Typef:X BddAbove (Set.range fun A x A, |f x|) (ε : ), 0 < ε s, (t : Finset X), Disjoint t s | x t, |f x|| < ε classical X:Typef:X BddAbove (Set.range fun A x A, |f x|) (ε : ), 0 < ε s, (t : Finset X), Disjoint t s | x t, |f x|| < εX:Typef:X (∀ (ε : ), 0 < ε s, (t : Finset X), Disjoint t s | x t, |f x|| < ε) BddAbove (Set.range fun A x A, |f x|) X:Typef:X BddAbove (Set.range fun A x A, |f x|) (ε : ), 0 < ε s, (t : Finset X), Disjoint t s | x t, |f x|| < ε intro h X:Typef:X h:BddAbove (Set.range fun A x A, |f x|)ε:0 < ε s, (t : Finset X), Disjoint t s | x t, |f x|| < ε X:Typef:X h:BddAbove (Set.range fun A x A, |f x|)ε::0 < ε s, (t : Finset X), Disjoint t s | x t, |f x|| < ε X:Typef:X ε::0 < εs:Set := Set.range fun A x A, |f x|h:BddAbove s s, (t : Finset X), Disjoint t s | x t, |f x|| < ε have hnon : s.Nonempty := X:Typef:X AbsConvergent' f Summable f X:Typef:X ε::0 < εs:Set := Set.range fun A x A, |f x|h:BddAbove s(Set.range fun A x A, |f x|).Nonempty; X:Typef:X ε::0 < εs:Set := Set.range fun A x A, |f x|h:BddAbove s(fun A x A, |f x|) = 0; All goals completed! 🐙 have : (sSup s)-ε < sSup s := X:Typef:X AbsConvergent' f Summable f All goals completed! 🐙 X:Typef:X ε::0 < εs:Set := Set.range fun A x A, |f x|h:BddAbove shnon:s.Nonemptythis: a, sSup (Set.range fun A x A, |f x|) - ε < x a, |f x| s, (t : Finset X), Disjoint t s | x t, |f x|| < ε; X:Typef:X ε::0 < εs:Set := Set.range fun A x A, |f x|h:BddAbove shnon:s.NonemptyS:Finset XhS:sSup (Set.range fun A x A, |f x|) - ε < x S, |f x| s, (t : Finset X), Disjoint t s | x t, |f x|| < ε X:Typef:X ε::0 < εs:Set := Set.range fun A x A, |f x|h:BddAbove shnon:s.NonemptyS:Finset XhS:sSup (Set.range fun A x A, |f x|) - ε < x S, |f x| (t : Finset X), Disjoint t S | x t, |f x|| < ε; intro T X:Typef:X ε::0 < εs:Set := Set.range fun A x A, |f x|h:BddAbove shnon:s.NonemptyS:Finset XhS:sSup (Set.range fun A x A, |f x|) - ε < x S, |f x|T:Finset XhT:Disjoint T S| x T, |f x|| < ε X:Typef:X ε::0 < εs:Set := Set.range fun A x A, |f x|h:BddAbove shnon:s.NonemptyS:Finset XhS:sSup (Set.range fun A x A, |f x|) - ε < x S, |f x|T:Finset XhT:Disjoint T S x T, |f x| < ε have : x T, |f x| + x S, |f x| sSup s := X:Typef:X AbsConvergent' f Summable f X:Typef:X ε::0 < εs:Set := Set.range fun A x A, |f x|h:BddAbove shnon:s.NonemptyS:Finset XhS:sSup (Set.range fun A x A, |f x|) - ε < x S, |f x|T:Finset XhT:Disjoint T S x T, |f x| + x S, |f x| s X:Typef:X ε::0 < εs:Set := Set.range fun A x A, |f x|h:BddAbove shnon:s.NonemptyS:Finset XhS:sSup (Set.range fun A x A, |f x|) - ε < x S, |f x|T:Finset XhT:Disjoint T S y, x y, |f x| = x T, |f x| + x S, |f x|; All goals completed! 🐙 All goals completed! 🐙 X:Typef:X h: (ε : ), 0 < ε s, (t : Finset X), Disjoint t s | x t, |f x|| < εBddAbove (Set.range fun A x A, |f x|); choose S hS using h 1 (X:Typef:X h: (ε : ), 0 < ε s, (t : Finset X), Disjoint t s | x t, |f x|| < ε0 < 1 All goals completed! 🐙) X:Typef:X h: (ε : ), 0 < ε s, (t : Finset X), Disjoint t s | x t, |f x|| < εS:Finset XhS: (t : Finset X), Disjoint t S | x t, |f x|| < 1 x, y Set.range fun A x A, |f x|, y x X:Typef:X h: (ε : ), 0 < ε s, (t : Finset X), Disjoint t s | x t, |f x|| < εS:Finset XhS: (t : Finset X), Disjoint t S | x t, |f x|| < 1 y Set.range fun A x A, |f x|, y x S, |f x| + 1; X:Typef:X h: (ε : ), 0 < ε s, (t : Finset X), Disjoint t s | x t, |f x|| < εS:Finset XhS: (t : Finset X), Disjoint t S | x t, |f x|| < 1 (a : Finset X), x a, |f x| x S, |f x| + 1; X:Typef:X h: (ε : ), 0 < ε s, (t : Finset X), Disjoint t s | x t, |f x|| < εS:Finset XhS: (t : Finset X), Disjoint t S | x t, |f x|| < 1T:Finset X x T, |f x| x S, |f x| + 1 calc _ = x (T S), |f x| + x (T \ S), |f x| := (sum_inter_add_sum_diff _ _ _).symm _ _ := X:Typef:X h: (ε : ), 0 < ε s, (t : Finset X), Disjoint t s | x t, |f x|| < εS:Finset XhS: (t : Finset X), Disjoint t S | x t, |f x|| < 1T:Finset X x T S, |f x| + x T \ S, |f x| x S, |f x| + 1 X:Typef:X h: (ε : ), 0 < ε s, (t : Finset X), Disjoint t s | x t, |f x|| < εS:Finset XhS: (t : Finset X), Disjoint t S | x t, |f x|| < 1T:Finset XT S SX:Typef:X h: (ε : ), 0 < ε s, (t : Finset X), Disjoint t s | x t, |f x|| < εS:Finset XhS: (t : Finset X), Disjoint t S | x t, |f x|| < 1T:Finset X x T \ S, |f x| 1 X:Typef:X h: (ε : ), 0 < ε s, (t : Finset X), Disjoint t s | x t, |f x|| < εS:Finset XhS: (t : Finset X), Disjoint t S | x t, |f x|| < 1T:Finset XT S S All goals completed! 🐙 All goals completed! 🐙

Maybe suitable for porting to Mathlib?

theorem Filter.Eventually.int_natCast_atTop (p: Prop) : (∀ᶠ n in .atTop, p n) ∀ᶠ n: in .atTop, p n := p: Prop(∀ᶠ (n : ) in atTop, p n) ∀ᶠ (n : ) in atTop, p n p: Prop(∀ᶠ (n : ) in atTop, p n) ∀ᶠ (n : ) in atTop, p n p: Prop (x : ), (∀ (b : ), x b p b) a, (b : ), a b p b intro N p: PropN:hN: (b : ), N b p b a, (b : ), a b p b; p: PropN:hN: (b : ), N b p b (b : ), N b p b; intro n p: PropN:hN: (b : ), N b p bn:hn:N np n lift n to using (p: PropN:hN: (b : ), N b p bn:hn:N n0 n All goals completed! 🐙) p: PropN:hN: (b : ), N b p bn:hn:N np n; All goals completed! 🐙
theorem Filter.Tendsto.int_natCast_atTop {R:Type} (f: R) (l: Filter R) : atTop.Tendsto f l atTop.Tendsto (f Nat.cast) l := R:Typef: Rl:Filter RTendsto f atTop l Tendsto (f Nat.cast) atTop l R:Typef: Rl:Filter R(∀ p : R Prop⦄, (∀ᶠ (y : R) in l, p y) a, (b : ), a b p (f b)) p : R Prop⦄, (∀ᶠ (y : R) in l, p y) a, (b : ), a b p (f b) R:Typef: Rl:Filter Rp:R Proph:∀ᶠ (y : R) in l, p y(∃ a, (b : ), a b p (f b)) a, (b : ), a b p (f b) R:Typef: Rl:Filter Rp:R Proph:∀ᶠ (y : R) in l, p y(∀ᶠ (x : ) in atTop, p (f x)) ∀ᶠ (x : ) in atTop, p (f x) All goals completed! 🐙

Connection with Mathlib's tsum (or Σ') operation

theorem Sum'.eq_tsum {X:Type} (f:X ) (h: AbsConvergent' f) : Sum' f = ∑' x, f x := X:Typef:X h:AbsConvergent' fSum' f = ∑' (x : X), f x X:Typef:X h:AbsConvergent' fE:Set X := {x | f x 0}Sum' f = ∑' (x : X), f x X:Typef:X h:AbsConvergent' fE:Set X := {x | f x 0}hE:CountablyInfinite {x | f x 0}Sum' f = ∑' (x : X), f xX:Typef:X h:AbsConvergent' fE:Set X := {x | f x 0}hE:Finite {x | f x 0}Sum' f = ∑' (x : X), f x X:Typef:X h:AbsConvergent' fE:Set X := {x | f x 0}hE:CountablyInfinite {x | f x 0}Sum' f = ∑' (x : X), f x X:Typef:X h:AbsConvergent' fE:Set X := {x | f x 0}hE:CountablyInfinite {x | f x 0}(Sum fun x f x) = ∑' (x : X), f x X:Typef:X h:AbsConvergent' fE:Set X := {x | f x 0}hE:CountablyInfinite {x | f x 0}g: {x | f x 0}hg:Bijective g(Sum fun x f x) = ∑' (x : X), f x have : ((f Subtype.val) g:Series).absConverges := X:Typef:X h:AbsConvergent' fSum' f = ∑' (x : X), f x X:Typef:X h:AbsConvergent' fE:Set X := {x | f x 0}hE:CountablyInfinite {x | f x 0}g: {x | f x 0}hg:Bijective gAbsConvergent (f Subtype.val) X:Typef:X h:AbsConvergent' fE:Set X := {x | f x 0}hE:CountablyInfinite {x | f x 0}g: {x | f x 0}hg:Bijective gAbsConvergent' (f Subtype.val) All goals completed! 🐙 X:Typef:X h:AbsConvergent' fE:Set X := {x | f x 0}hE:CountablyInfinite {x | f x 0}g: {x | f x 0}hg:Bijective gthis:{ m := 0, seq := fun n if n 0 then ((f Subtype.val) g) n.toNat else 0, vanish := }.convergesTo (Sum (f Subtype.val))(Sum fun x f x) = ∑' (x : X), f x X:Typef:X h:AbsConvergent' fE:Set X := {x | f x 0}hE:CountablyInfinite {x | f x 0}g: {x | f x 0}hg:Bijective gthis:{ m := 0, seq := fun n if n 0 then ((f Subtype.val) g) n.toNat else 0, vanish := }.convergesTo (Sum (f Subtype.val)){ m := 0, seq := fun n if n 0 then ((f Subtype.val) g) n.toNat else 0, vanish := }.convergesTo (∑' (x : X), f x) X:Typef:X h:AbsConvergent' fE:Set X := {x | f x 0}hE:CountablyInfinite {x | f x 0}g: {x | f x 0}hg:Bijective gthis:{ m := 0, seq := fun n if n 0 then ((f Subtype.val) g) n.toNat else 0, vanish := }.convergesTo (Sum (f Subtype.val)){ m := 0, seq := fun n if n 0 then ((f Subtype.val) g) n.toNat else 0, vanish := }.convergesTo (∑' (x : X), f x) replace : ∑' x, f x = ∑' n, f (g n) := calc _ = ∑' x:E, f x := X:Typef:X h:AbsConvergent' fE:Set X := {x | f x 0}hE:CountablyInfinite {x | f x 0}g: {x | f x 0}hg:Bijective gthis:{ m := 0, seq := fun n if n 0 then ((f Subtype.val) g) n.toNat else 0, vanish := }.convergesTo (Sum (f Subtype.val))∑' (x : X), f x = ∑' (x : E), f x All goals completed! 🐙 _ = _ := (Equiv.tsum_eq (Equiv.ofBijective _ hg) _).symm X:Typef:X h:AbsConvergent' fE:Set X := {x | f x 0}hE:CountablyInfinite {x | f x 0}g: {x | f x 0}hg:Bijective gthis:∑' (x : X), f x = ∑' (n : ), f (g n){ m := 0, seq := fun n if n 0 then ((f Subtype.val) g) n.toNat else 0, vanish := }.convergesTo (∑' (n : ), f (g n)) X:Typef:X h:AbsConvergent' fE:Set X := {x | f x 0}hE:CountablyInfinite {x | f x 0}g: {x | f x 0}hg:Bijective gthis:∑' (x : X), f x = ∑' (n : ), f (g n)Tendsto { m := 0, seq := fun n if n 0 then ((f Subtype.val) g) n.toNat else 0, vanish := }.partial atTop (nhds (∑' (n : ), f (g n))); X:Typef:X h:AbsConvergent' fE:Set X := {x | f x 0}hE:CountablyInfinite {x | f x 0}g: {x | f x 0}hg:Bijective gthis:∑' (x : X), f x = ∑' (n : ), f (g n)Tendsto ({ m := 0, seq := fun n if n 0 then ((f Subtype.val) g) n.toNat else 0, vanish := }.partial Nat.cast) atTop (nhds (∑' (n : ), f (g n))) X:Typef:X h:AbsConvergent' fE:Set X := {x | f x 0}hE:CountablyInfinite {x | f x 0}g: {x | f x 0}hg:Bijective gthis:∑' (x : X), f x = ∑' (n : ), f (g n){ m := 0, seq := fun n if n 0 then ((f Subtype.val) g) n.toNat else 0, vanish := }.partial Nat.cast = (fun n i range n, f (g i)) fun a a + 1X:Typef:X h:AbsConvergent' fE:Set X := {x | f x 0}hE:CountablyInfinite {x | f x 0}g: {x | f x 0}hg:Bijective gthis:∑' (x : X), f x = ∑' (n : ), f (g n)Summable fun n f (g n) X:Typef:X h:AbsConvergent' fE:Set X := {x | f x 0}hE:CountablyInfinite {x | f x 0}g: {x | f x 0}hg:Bijective gthis:∑' (x : X), f x = ∑' (n : ), f (g n){ m := 0, seq := fun n if n 0 then ((f Subtype.val) g) n.toNat else 0, vanish := }.partial Nat.cast = (fun n i range n, f (g i)) fun a a + 1 X:Typef:X h:AbsConvergent' fE:Set X := {x | f x 0}hE:CountablyInfinite {x | f x 0}g: {x | f x 0}hg:Bijective gthis:∑' (x : X), f x = ∑' (n : ), f (g n)N:({ m := 0, seq := fun n if n 0 then ((f Subtype.val) g) n.toNat else 0, vanish := }.partial Nat.cast) N = ((fun n i range n, f (g i)) fun a a + 1) N; All goals completed! 🐙 X:Typef:X h:Summable fE:Set X := {x | f x 0}hE:CountablyInfinite {x | f x 0}g: {x | f x 0}hg:Bijective gthis:∑' (x : X), f x = ∑' (n : ), f (g n)Summable fun n f (g n) All goals completed! 🐙 X:Typef:X h:AbsConvergent' fE:Set X := {x | f x 0}hE:Finite {x | f x 0} x .toFinset, f x = ∑' (x : X), f xX:Typef:X h:AbsConvergent' fE:Set X := {x | f x 0}hE:Finite {x | f x 0} x .toFinset, f x = 0; X:Typef:X h:AbsConvergent' fE:Set X := {x | f x 0}hE:Finite {x | f x 0}∑' (x : X), f x = x .toFinset, f xX:Typef:X h:AbsConvergent' fE:Set X := {x | f x 0}hE:Finite {x | f x 0} x .toFinset, f x = 0; X:Typef:X h:AbsConvergent' fE:Set X := {x | f x 0}hE:Finite {x | f x 0} b .toFinset, f b = 0X:Typef:X h:AbsConvergent' fE:Set X := {x | f x 0}hE:Finite {x | f x 0} x .toFinset, f x = 0 all_goals All goals completed! 🐙

Proposition 8.2.6 (a) (Absolutely convergent series laws) / Exercise 8.2.3

theorem declaration uses `sorry`Sum'.add {X:Type} {f g:X } (hf: AbsConvergent' f) (hg: AbsConvergent' g) : AbsConvergent' (f+g) Sum' (f + g) = Sum' f + Sum' g := X:Typef:X g:X hf:AbsConvergent' fhg:AbsConvergent' gAbsConvergent' (f + g) Sum' (f + g) = Sum' f + Sum' g All goals completed! 🐙

Proposition 8.2.6 (b) (Absolutely convergent series laws) / Exercise 8.2.3

theorem declaration uses `sorry`Sum'.smul {X:Type} {f:X } (hf: AbsConvergent' f) (c: ) : AbsConvergent' (c f) Sum' (c f) = c * Sum' f := X:Typef:X hf:AbsConvergent' fc:AbsConvergent' (c f) Sum' (c f) = c * Sum' f All goals completed! 🐙

This law is not explicitly stated in Proposition 8.2.6, but follows easily from parts (a) and (b).

theorem Sum'.sub {X:Type} {f g:X } (hf: AbsConvergent' f) (hg: AbsConvergent' g) : AbsConvergent' (f-g) Sum' (f - g) = Sum' f - Sum' g := X:Typef:X g:X hf:AbsConvergent' fhg:AbsConvergent' gAbsConvergent' (f - g) Sum' (f - g) = Sum' f - Sum' g X:Typef:X g:X hf:AbsConvergent' fhg:AbsConvergent' gf - g = f + -1 gX:Typef:X g:X hf:AbsConvergent' fhg:AbsConvergent' gSum' (f - g) = Sum' (f + -1 g)X:Typef:X g:X hf:AbsConvergent' fhg:AbsConvergent' gSum' f - Sum' g = Sum' f + Sum' (-1 g) X:Typef:X g:X hf:AbsConvergent' fhg:AbsConvergent' gf - g = f + -1 g X:Typef:X g:X hf:AbsConvergent' fhg:AbsConvergent' gf - g = f + -g; All goals completed! 🐙 X:Typef:X g:X hf:AbsConvergent' fhg:AbsConvergent' gSum' (f - g) = Sum' (f + -1 g) X:Typef:X g:X hf:AbsConvergent' fhg:AbsConvergent' gf - g = f + -1 g; X:Typef:X g:X hf:AbsConvergent' fhg:AbsConvergent' gf - g = f + -g; All goals completed! 🐙 X:Typef:X g:X hf:AbsConvergent' fhg:AbsConvergent' gSum' f - Sum' g = Sum' f + -1 * Sum' g; All goals completed! 🐙

Proposition 8.2.6 (c) (Absolutely convergent series laws) / Exercise 8.2.3. The first part of this proposition has been moved to AbsConvergent'.­subtype.

theorem declaration uses `sorry`Sum'.of_disjoint_union {X:Type} {f:X } (hf: AbsConvergent' f) {X₁ X₂ : Set X} (hdisj: Disjoint X₁ X₂): Sum' (fun x: (X₁ X₂: Set X) f x) = Sum' (fun x : X₁ f x) + Sum' (fun x : X₂ f x) := X:Typef:X hf:AbsConvergent' fX₁:Set XX₂:Set Xhdisj:Disjoint X₁ X₂(Sum' fun x f x) = (Sum' fun x f x) + Sum' fun x f x All goals completed! 🐙

This technical claim, the analogue of tsum_univ, is required due to the way Mathlib handles sets.

theorem declaration uses `sorry`Sum'.of_univ {X:Type} {f:X } (hf: AbsConvergent' f) : Sum' (fun x: (.univ : Set X) f x) = Sum' f := X:Typef:X hf:AbsConvergent' f(Sum' fun x f x) = Sum' f All goals completed! 🐙
theorem declaration uses `sorry`Sum'.of_comp {X Y:Type} {f:X } (hf: AbsConvergent' f) {φ: Y X} (: Function.Bijective φ) : AbsConvergent' (f φ) Sum' f = Sum' (f φ) := X:TypeY:Typef:X hf:AbsConvergent' fφ:Y X:Bijective φAbsConvergent' (f φ) Sum' f = Sum' (f φ) All goals completed! 🐙

Lemma 8.2.7 / Exercise 8.2.4

theorem declaration uses `sorry`divergent_parts_of_divergent {a: } (ha: (a:Series).converges) (ha': ¬ (a:Series).absConverges) : ¬ AbsConvergent (fun n : {n | a n 0} a n) ¬ AbsConvergent (fun n : {n | a n < 0} a n) := a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConverges(¬AbsConvergent fun n a n) ¬AbsConvergent fun n a n All goals completed! 🐙

Theorem 8.2.8 (Riemann rearrangement theorem) / Exercise 8.2.5

theorem declaration uses `sorry`permute_convergesTo_of_divergent {a: } (ha: (a:Series).converges) (ha': ¬ (a:Series).absConverges) (L:) : f : , Bijective f (a f:Series).convergesTo L := a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL: f, Bijective f { m := 0, seq := fun n if n 0 then (a f) n.toNat else 0, vanish := }.convergesTo L -- This proof is written to follow the structure of the original text. a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL:h1:¬AbsConvergent fun n a nh2:¬AbsConvergent fun n a n f, Bijective f { m := 0, seq := fun n if n 0 then (a f) n.toNat else 0, vanish := }.convergesTo L a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL:h2:¬AbsConvergent fun n a nA_plus:Set := {n | a n 0}h1:¬AbsConvergent fun n a n f, Bijective f { m := 0, seq := fun n if n 0 then (a f) n.toNat else 0, vanish := }.convergesTo L a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL:A_plus:Set := {n | a n 0}h1:¬AbsConvergent fun n a nA_minus:Set := {n | a n < 0}h2:¬AbsConvergent fun n a n f, Bijective f { m := 0, seq := fun n if n 0 then (a f) n.toNat else 0, vanish := }.convergesTo L have hdisj : Disjoint A_plus A_minus := a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL: f, Bijective f { m := 0, seq := fun n if n 0 then (a f) n.toNat else 0, vanish := }.convergesTo L a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL:A_plus:Set := {n | a n 0}h1:¬AbsConvergent fun n a nA_minus:Set := {n | a n < 0}h2:¬AbsConvergent fun n a nA_plus A_minus = ; a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL:A_plus:Set := {n | a n 0}h1:¬AbsConvergent fun n a nA_minus:Set := {n | a n < 0}h2:¬AbsConvergent fun n a nx✝:x✝ A_plus A_minus x✝ ; All goals completed! 🐙 have hunion : A_plus A_minus = .univ := a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL: f, Bijective f { m := 0, seq := fun n if n 0 then (a f) n.toNat else 0, vanish := }.convergesTo L a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL:A_plus:Set := {n | a n 0}h1:¬AbsConvergent fun n a nA_minus:Set := {n | a n < 0}h2:¬AbsConvergent fun n a nhdisj:Disjoint A_plus A_minusx✝:x✝ A_plus A_minus x✝ Set.univ; a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL:A_plus:Set := {n | a n 0}h1:¬AbsConvergent fun n a nA_minus:Set := {n | a n < 0}h2:¬AbsConvergent fun n a nhdisj:Disjoint A_plus A_minusx✝:0 a x✝ a x✝ < 0; All goals completed! 🐙 a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL:A_plus:Set := {n | a n 0}h1:¬AbsConvergent fun n a nA_minus:Set := {n | a n < 0}h2:¬AbsConvergent fun n a nhdisj:Disjoint A_plus A_minushunion:A_plus A_minus = Set.univhA_plus_inf:Infinite A_plus f, Bijective f { m := 0, seq := fun n if n 0 then (a f) n.toNat else 0, vanish := }.convergesTo L a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL:A_plus:Set := {n | a n 0}h1:¬AbsConvergent fun n a nA_minus:Set := {n | a n < 0}h2:¬AbsConvergent fun n a nhdisj:Disjoint A_plus A_minushunion:A_plus A_minus = Set.univhA_plus_inf:Infinite A_plushA_minus_inf:Infinite A_minus f, Bijective f { m := 0, seq := fun n if n 0 then (a f) n.toNat else 0, vanish := }.convergesTo L a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL:A_plus:Set := {n | a n 0}h1:¬AbsConvergent fun n a nA_minus:Set := {n | a n < 0}h2:¬AbsConvergent fun n a nhdisj:Disjoint A_plus A_minushunion:A_plus A_minus = Set.univhA_plus_inf:Infinite A_plushA_minus_inf:Infinite A_minusa_plus: A_plusha_plus_bij:Bijective a_plusha_plus_mono:StrictMono a_plus f, Bijective f { m := 0, seq := fun n if n 0 then (a f) n.toNat else 0, vanish := }.convergesTo L a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL:A_plus:Set := {n | a n 0}h1:¬AbsConvergent fun n a nA_minus:Set := {n | a n < 0}h2:¬AbsConvergent fun n a nhdisj:Disjoint A_plus A_minushunion:A_plus A_minus = Set.univhA_plus_inf:Infinite A_plushA_minus_inf:Infinite A_minusa_plus: A_plusha_plus_bij:Bijective a_plusha_plus_mono:StrictMono a_plusa_minus: A_minusha_minus_bij:Bijective a_minusha_minus_mono:StrictMono a_minus f, Bijective f { m := 0, seq := fun n if n 0 then (a f) n.toNat else 0, vanish := }.convergesTo L let F : (n : ) ((m : ) m < n ) := fun j n' if i:Fin j, a (n' i (a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL:A_plus:Set := {n | a n 0}h1:¬AbsConvergent fun n a nA_minus:Set := {n | a n < 0}h2:¬AbsConvergent fun n a nhdisj:Disjoint A_plus A_minushunion:A_plus A_minus = Set.univhA_plus_inf:Infinite A_plushA_minus_inf:Infinite A_minusa_plus: A_plusha_plus_bij:Bijective a_plusha_plus_mono:StrictMono a_plusa_minus: A_minusha_minus_bij:Bijective a_minusha_minus_mono:StrictMono a_minusj:n':(m : ) m < j i:Fin ji < j All goals completed! 🐙)) < L then Nat.min { n A_plus | i:Fin j, n n' i (a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL:A_plus:Set := {n | a n 0}h1:¬AbsConvergent fun n a nA_minus:Set := {n | a n < 0}h2:¬AbsConvergent fun n a nhdisj:Disjoint A_plus A_minushunion:A_plus A_minus = Set.univhA_plus_inf:Infinite A_plushA_minus_inf:Infinite A_minusa_plus: A_plusha_plus_bij:Bijective a_plusha_plus_mono:StrictMono a_plusa_minus: A_minusha_minus_bij:Bijective a_minusha_minus_mono:StrictMono a_minusj:n':(m : ) m < j n:i:Fin ji < j All goals completed! 🐙) } else Nat.min { n A_minus | i:Fin j, n n' i (a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL:A_plus:Set := {n | a n 0}h1:¬AbsConvergent fun n a nA_minus:Set := {n | a n < 0}h2:¬AbsConvergent fun n a nhdisj:Disjoint A_plus A_minushunion:A_plus A_minus = Set.univhA_plus_inf:Infinite A_plushA_minus_inf:Infinite A_minusa_plus: A_plusha_plus_bij:Bijective a_plusha_plus_mono:StrictMono a_plusa_minus: A_minusha_minus_bij:Bijective a_minusha_minus_mono:StrictMono a_minusj:n':(m : ) m < j n:i:Fin ji < j All goals completed! 🐙) } a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL:A_plus:Set := {n | a n 0}h1:¬AbsConvergent fun n a nA_minus:Set := {n | a n < 0}h2:¬AbsConvergent fun n a nhdisj:Disjoint A_plus A_minushunion:A_plus A_minus = Set.univhA_plus_inf:Infinite A_plushA_minus_inf:Infinite A_minusa_plus: A_plusha_plus_bij:Bijective a_plusha_plus_mono:StrictMono a_plusa_minus: A_minusha_minus_bij:Bijective a_minusha_minus_mono:StrictMono a_minusF:(n : ) ((m : ) m < n ) := fun j n' if i, a (n' i ) < L then Nat.min {n | n A_plus (i : Fin j), n n' i } else Nat.min {n | n A_minus (i : Fin j), n n' i }n': := fun t Nat.strongRec F t f, Bijective f { m := 0, seq := fun n if n 0 then (a f) n.toNat else 0, vanish := }.convergesTo L a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL:A_plus:Set := {n | a n 0}h1:¬AbsConvergent fun n a nA_minus:Set := {n | a n < 0}h2:¬AbsConvergent fun n a nhdisj:Disjoint A_plus A_minushunion:A_plus A_minus = Set.univhA_plus_inf:Infinite A_plushA_minus_inf:Infinite A_minusa_plus: A_plusha_plus_bij:Bijective a_plusha_plus_mono:StrictMono a_plusa_minus: A_minusha_minus_bij:Bijective a_minusha_minus_mono:StrictMono a_minusF:(n : ) ((m : ) m < n ) := fun j n' if i, a (n' i ) < L then Nat.min {n | n A_plus (i : Fin j), n n' i } else Nat.min {n | n A_minus (i : Fin j), n n' i }n': := fun t Nat.strongRec F thn': (j : ), n' j = if i, a (n' i) < L then Nat.min {n | n A_plus (i : Fin j), n n' i} else Nat.min {n | n A_minus (i : Fin j), n n' i} f, Bijective f { m := 0, seq := fun n if n 0 then (a f) n.toNat else 0, vanish := }.convergesTo L have hn'_plus_inf (j:) : Infinite { n A_plus | i:Fin j, n n' i } := a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL: f, Bijective f { m := 0, seq := fun n if n 0 then (a f) n.toNat else 0, vanish := }.convergesTo L All goals completed! 🐙 have hn'_minus_inf (j:) : Infinite { n A_minus | i:Fin j, n n' i } := a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL: f, Bijective f { m := 0, seq := fun n if n 0 then (a f) n.toNat else 0, vanish := }.convergesTo L All goals completed! 🐙 have hn'_inj : Injective n' := a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL: f, Bijective f { m := 0, seq := fun n if n 0 then (a f) n.toNat else 0, vanish := }.convergesTo L All goals completed! 🐙 have h_case_I : Infinite { j | i:Fin j, a (n' i) < L } := a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL: f, Bijective f { m := 0, seq := fun n if n 0 then (a f) n.toNat else 0, vanish := }.convergesTo L All goals completed! 🐙 have h_case_II : Infinite { j | i:Fin j, a (n' i) L } := a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL: f, Bijective f { m := 0, seq := fun n if n 0 then (a f) n.toNat else 0, vanish := }.convergesTo L All goals completed! 🐙 have hn'_surj : Surjective n' := a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL: f, Bijective f { m := 0, seq := fun n if n 0 then (a f) n.toNat else 0, vanish := }.convergesTo L All goals completed! 🐙 have hconv : atTop.Tendsto (a n') (nhds 0) := a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL: f, Bijective f { m := 0, seq := fun n if n 0 then (a f) n.toNat else 0, vanish := }.convergesTo L All goals completed! 🐙 have hsum : (a n':Series).convergesTo L := a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL: f, Bijective f { m := 0, seq := fun n if n 0 then (a f) n.toNat else 0, vanish := }.convergesTo L All goals completed! 🐙 a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL:A_plus:Set := {n | a n 0}h1:¬AbsConvergent fun n a nA_minus:Set := {n | a n < 0}h2:¬AbsConvergent fun n a nhdisj:Disjoint A_plus A_minushunion:A_plus A_minus = Set.univhA_plus_inf:Infinite A_plushA_minus_inf:Infinite A_minusa_plus: A_plusha_plus_bij:Bijective a_plusha_plus_mono:StrictMono a_plusa_minus: A_minusha_minus_bij:Bijective a_minusha_minus_mono:StrictMono a_minusF:(n : ) ((m : ) m < n ) := fun j n' if i, a (n' i ) < L then Nat.min {n | n A_plus (i : Fin j), n n' i } else Nat.min {n | n A_minus (i : Fin j), n n' i }n': := fun t Nat.strongRec F thn': (j : ), n' j = if i, a (n' i) < L then Nat.min {n | n A_plus (i : Fin j), n n' i} else Nat.min {n | n A_minus (i : Fin j), n n' i}hn'_plus_inf: (j : ), Infinite {n | n A_plus (i : Fin j), n n' i}hn'_minus_inf: (j : ), Infinite {n | n A_minus (i : Fin j), n n' i}hn'_inj:Injective n'h_case_I:Infinite {j | i, a (n' i) < L}h_case_II:Infinite {j | i, a (n' i) L}hn'_surj:Surjective n'hconv:Tendsto (a n') atTop (nhds 0)hsum:{ m := 0, seq := fun n if n 0 then (a n') n.toNat else 0, vanish := }.convergesTo LBijective n' { m := 0, seq := fun n if n 0 then (a n') n.toNat else 0, vanish := }.convergesTo L a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesL:A_plus:Set := {n | a n 0}h1:¬AbsConvergent fun n a nA_minus:Set := {n | a n < 0}h2:¬AbsConvergent fun n a nhdisj:Disjoint A_plus A_minushunion:A_plus A_minus = Set.univhA_plus_inf:Infinite A_plushA_minus_inf:Infinite A_minusa_plus: A_plusha_plus_bij:Bijective a_plusha_plus_mono:StrictMono a_plusa_minus: A_minusha_minus_bij:Bijective a_minusha_minus_mono:StrictMono a_minusF:(n : ) ((m : ) m < n ) := fun j n' if i, a (n' i ) < L then Nat.min {n | n A_plus (i : Fin j), n n' i } else Nat.min {n | n A_minus (i : Fin j), n n' i }n': := fun t Nat.strongRec F thn': (j : ), n' j = if i, a (n' i) < L then Nat.min {n | n A_plus (i : Fin j), n n' i} else Nat.min {n | n A_minus (i : Fin j), n n' i}hn'_plus_inf: (j : ), Infinite {n | n A_plus (i : Fin j), n n' i}hn'_minus_inf: (j : ), Infinite {n | n A_minus (i : Fin j), n n' i}hn'_inj:Injective n'h_case_I:Infinite {j | i, a (n' i) < L}h_case_II:Infinite {j | i, a (n' i) L}hn'_surj:Surjective n'hconv:Tendsto (a n') atTop (nhds 0)hsum:{ m := 0, seq := fun n if n 0 then (a n') n.toNat else 0, vanish := }.convergesTo L{ m := 0, seq := fun n if n 0 then (a n') n.toNat else 0, vanish := }.convergesTo L; All goals completed! 🐙

Exercise 8.2.6

theorem declaration uses `sorry`permute_diverges_of_divergent {a: } (ha: (a:Series).converges) (ha': ¬ (a:Series).absConverges) : f : , Bijective f atTop.Tendsto (fun N ((a f:Series).partial N : EReal)) (nhds ) := a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConverges f, Bijective f Tendsto (fun N ({ m := 0, seq := fun n if n 0 then (a f) n.toNat else 0, vanish := }.partial N)) atTop (nhds ) All goals completed! 🐙
theorem declaration uses `sorry`permute_diverges_of_divergent' {a: } (ha: (a:Series).converges) (ha': ¬ (a:Series).absConverges) : f : , Bijective f atTop.Tendsto (fun N ((a f:Series).partial N : EReal)) (nhds ) := a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesha':¬{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConverges f, Bijective f Tendsto (fun N ({ m := 0, seq := fun n if n 0 then (a f) n.toNat else 0, vanish := }.partial N)) atTop (nhds ) All goals completed! 🐙end Chapter8