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.
-
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).absConvergestheorem 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 := ⋯ }.absConverges⊢ AbsConvergent f All goals completed! 🐙open Classical in
/-- The definition has been chosen to give a sensible value when `X` is finite, even though
`AbsConvergent` is by definition false in this context. -/
noncomputable 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 0theorem 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 f⊢ False; 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 := ⋯ }.absConverges⊢ False
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 := ⋯ }.absConverges⊢ False; 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 := ⋯ }.absConverges⊢ Infinite ℕ; 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:Function.Bijective (_fvar.10895 ∘ _fvar.10859) :=
Function.Bijective.comp ⟨Function.RightInverse.injective _fvar.10907, Function.LeftInverse.surjective _fvar.10903⟩
_fvar.10860⊢ { 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:Function.Bijective (_fvar.10895 ∘ _fvar.10859) :=
Function.Bijective.comp ⟨Function.RightInverse.injective _fvar.10907, Function.LeftInverse.surjective _fvar.10903⟩
_fvar.10860n:ℤ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:Chapter8.AbsConvergent _fvar.12539 := Chapter8.AbsConvergent.mk _fvar.12541 _fvar.12542⊢ { 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:Chapter8.AbsConvergent _fvar.12539 := Chapter8.AbsConvergent.mk _fvar.12541 _fvar.12542⊢ { 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:Chapter8.AbsConvergent _fvar.12539 := Chapter8.AbsConvergent.mk _fvar.12541 _fvar.12542hbij: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:Chapter8.AbsConvergent _fvar.12539 := Chapter8.AbsConvergent.mk _fvar.12541 _fvar.12542g':ℕ → _fvar.12538 :=
@Exists.choose (ℕ → _fvar.12538)
(fun g =>
Function.Bijective g ∧
{ m := 0, seq := fun n => if n ≥ 0 then (_fvar.12539 ∘ g) n.toNat else 0, vanish := ⋯ }.absConverges)
_fvar.12561hbij: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:Chapter8.AbsConvergent _fvar.12539 := Chapter8.AbsConvergent.mk _fvar.12541 _fvar.12542g':ℕ → _fvar.12538 :=
@Exists.choose (ℕ → _fvar.12538)
(fun g =>
Function.Bijective g ∧
{ m := 0, seq := fun n => if n ≥ 0 then (_fvar.12539 ∘ g) n.toNat else 0, vanish := ⋯ }.absConverges)
_fvar.12561hbij: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:Chapter8.AbsConvergent _fvar.12539 := Chapter8.AbsConvergent.mk _fvar.12541 _fvar.12542g':ℕ → _fvar.12538 :=
@Exists.choose (ℕ → _fvar.12538)
(fun g =>
Function.Bijective g ∧
{ m := 0, seq := fun n => if n ≥ 0 then (_fvar.12539 ∘ g) n.toNat else 0, vanish := ⋯ }.absConverges)
_fvar.12561hbij: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:Chapter8.AbsConvergent _fvar.12539 := Chapter8.AbsConvergent.mk _fvar.12541 _fvar.12542g':ℕ → _fvar.12538 :=
@Exists.choose (ℕ → _fvar.12538)
(fun g =>
Function.Bijective g ∧
{ m := 0, seq := fun n => if n ≥ 0 then (_fvar.12539 ∘ g) n.toNat else 0, vanish := ⋯ }.absConverges)
_fvar.12561hbij: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:Function.Bijective (_fvar.30992 ∘ _fvar.12540) :=
Function.Bijective.comp ⟨Function.RightInverse.injective _fvar.31004, Function.LeftInverse.surjective _fvar.31000⟩
_fvar.12541⊢ { 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:Chapter8.AbsConvergent _fvar.12539 := Chapter8.AbsConvergent.mk _fvar.12541 _fvar.12542g':ℕ → _fvar.12538 :=
@Exists.choose (ℕ → _fvar.12538)
(fun g =>
Function.Bijective g ∧
{ m := 0, seq := fun n => if n ≥ 0 then (_fvar.12539 ∘ g) n.toNat else 0, vanish := ⋯ }.absConverges)
_fvar.12561hbij: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:Function.Bijective (_fvar.30992 ∘ _fvar.12540) :=
Function.Bijective.comp ⟨Function.RightInverse.injective _fvar.31004, Function.LeftInverse.surjective _fvar.31000⟩
_fvar.12541n:ℤ⊢ (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:Chapter8.AbsConvergent _fvar.12539 := Chapter8.AbsConvergent.mk _fvar.12541 _fvar.12542g':ℕ → _fvar.12538 :=
@Exists.choose (ℕ → _fvar.12538)
(fun g =>
Function.Bijective g ∧
{ m := 0, seq := fun n => if n ≥ 0 then (_fvar.12539 ∘ g) n.toNat else 0, vanish := ⋯ }.absConverges)
_fvar.12561hbij: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:Function.Bijective (_fvar.30992 ∘ _fvar.12540) :=
Function.Bijective.comp ⟨Function.RightInverse.injective _fvar.31004, Function.LeftInverse.surjective _fvar.31000⟩
_fvar.12541n:ℤ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:Chapter8.AbsConvergent _fvar.12539 := Chapter8.AbsConvergent.mk _fvar.12541 _fvar.12542g':ℕ → _fvar.12538 :=
@Exists.choose (ℕ → _fvar.12538)
(fun g =>
Function.Bijective g ∧
{ m := 0, seq := fun n => if n ≥ 0 then (_fvar.12539 ∘ g) n.toNat else 0, vanish := ⋯ }.absConverges)
_fvar.12561hbij: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:Function.Bijective (_fvar.30992 ∘ _fvar.12540) :=
Function.Bijective.comp ⟨Function.RightInverse.injective _fvar.31004, Function.LeftInverse.surjective _fvar.31000⟩
_fvar.12541n:ℤ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:Chapter8.AbsConvergent _fvar.12539 := Chapter8.AbsConvergent.mk _fvar.12541 _fvar.12542g':ℕ → _fvar.12538 :=
@Exists.choose (ℕ → _fvar.12538)
(fun g =>
Function.Bijective g ∧
{ m := 0, seq := fun n => if n ≥ 0 then (_fvar.12539 ∘ g) n.toNat else 0, vanish := ⋯ }.absConverges)
_fvar.12561hbij: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:Function.Bijective (_fvar.30992 ∘ _fvar.12540) :=
Function.Bijective.comp ⟨Function.RightInverse.injective _fvar.31004, Function.LeftInverse.surjective _fvar.31000⟩
_fvar.12541n:ℤ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:Chapter8.AbsConvergent _fvar.12539 := Chapter8.AbsConvergent.mk _fvar.12541 _fvar.12542g':ℕ → _fvar.12538 :=
@Exists.choose (ℕ → _fvar.12538)
(fun g =>
Function.Bijective g ∧
{ m := 0, seq := fun n => if n ≥ 0 then (_fvar.12539 ∘ g) n.toNat else 0, vanish := ⋯ }.absConverges)
_fvar.12561hbij: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:Function.Bijective (_fvar.30992 ∘ _fvar.12540) :=
Function.Bijective.comp ⟨Function.RightInverse.injective _fvar.31004, Function.LeftInverse.surjective _fvar.31000⟩
_fvar.12541n:ℤ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 g⊢ AbsConvergent (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 := ⋯ }.absConverges⊢ AbsConvergent (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 g⊢ AbsConvergent (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':Function.Bijective (_fvar.37554 ∘ _fvar.37523) :=
Function.Bijective.comp ⟨Function.RightInverse.injective _fvar.37566, Function.LeftInverse.surjective _fvar.37562⟩
_fvar.37532⊢ 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 g⊢ AbsConvergent (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':Function.Bijective (_fvar.37554 ∘ _fvar.37523) :=
Function.Bijective.comp ⟨Function.RightInverse.injective _fvar.37566, Function.LeftInverse.surjective _fvar.37562⟩
_fvar.37532n:ℕ⊢ ((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':Function.Bijective (@Function.comp ℕ _fvar.37515 _fvar.37516 _fvar.37554 _fvar.37523) :=
Function.Bijective.comp ⟨Function.RightInverse.injective _fvar.37566, Function.LeftInverse.surjective _fvar.37562⟩
_fvar.37532hident:(_fvar.37517 ∘ _fvar.37519) ∘ @Function.comp ℕ _fvar.37515 _fvar.37516 _fvar.37554 _fvar.37523 =
_fvar.37517 ∘ _fvar.37523 :=
funext fun n =>
of_eq_true
(Eq.trans (congrArg (fun x => @_fvar.37517 x = @_fvar.37517 (@_fvar.37523 n)) (@_fvar.37566 (@_fvar.37523 n)))
(eq_self (@_fvar.37517 (@_fvar.37523 n))))⊢ { 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':Function.Bijective (@Function.comp ℕ _fvar.37515 _fvar.37516 _fvar.37554 _fvar.37523) :=
Function.Bijective.comp ⟨Function.RightInverse.injective _fvar.37566, Function.LeftInverse.surjective _fvar.37562⟩
_fvar.37532hident:(_fvar.37517 ∘ _fvar.37519) ∘ @Function.comp ℕ _fvar.37515 _fvar.37516 _fvar.37554 _fvar.37523 =
_fvar.37517 ∘ _fvar.37523 :=
funext fun n =>
of_eq_true
(Eq.trans (congrArg (fun x => @_fvar.37517 x = @_fvar.37517 (@_fvar.37523 n)) (@_fvar.37566 (@_fvar.37523 n)))
(eq_self (@_fvar.37517 (@_fvar.37523 n))))⊢ { 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':Function.Bijective (_fvar.37554 ∘ _fvar.37523) :=
Function.Bijective.comp ⟨Function.RightInverse.injective _fvar.37566, Function.LeftInverse.surjective _fvar.37562⟩
_fvar.37532hident:(_fvar.37517 ∘ _fvar.37519) ∘ _fvar.37554 ∘ _fvar.37523 = _fvar.37517 ∘ _fvar.37523 := ?_mvar.37730h:{ 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 ≤ ↑N⊢ n ≤ N ∧ ↑n = ↑n; All goals completed! 🐙
N:ℕw✝:ℕleft✝:w✝ ≤ N⊢ 0 ≤ ↑w✝ ∧ ↑w✝ ≤ ↑N; All goals completed! 🐙theorem Finset.Icc_empty {N:ℤ} (h: ¬ N ≥ 0) : Icc 0 N = ∅ := N:ℤh:¬N ≥ 0⊢ Icc 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✝¹ ≤ N⊢ N ≥ 0; All goals completed! 🐙Theorem 8.2.2, preliminary version. The arguments here are rearranged slightly from the text.
theorem 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:ℝ := Chapter8.Sum _fvar.59574⊢ (∀ (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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xn:ℕM:ℕ⊢ ∑ x ∈ Icc 0 M, f (n, x) ≤ L
f:ℕ × ℕ → ℝhf:AbsConvergent fhpos:∀ (n m : ℕ), 0 ≤ f (n, m)L:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xn:ℕ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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xn:ℕM:ℕ⊢ ∑ x ∈ Finset.map (Embedding.sectR n ℕ) (Icc 0 M), f x ≤ L
f:ℕ × ℕ → ℝhf:AbsConvergent fhpos:∀ (n m : ℕ), 0 ≤ f (n, m)L:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xn:ℕ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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mn:ℕ⊢ ∀ (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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mn:ℕm:ℤ⊢ 0 ≤ if 0 ≤ m then f (n, m.toNat) else 0; f:ℕ × ℕ → ℝhf:AbsConvergent fhpos:∀ (n m : ℕ), 0 ≤ f (n, m)L:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mn:ℕm:ℤh✝:0 ≤ m⊢ 0 ≤ f (n, m.toNat)f:ℕ × ℕ → ℝhf:AbsConvergent fhpos:∀ (n m : ℕ), 0 ≤ f (n, m)L:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mn:ℕm:ℤh✝:¬0 ≤ m⊢ 0 ≤ 0 f:ℕ × ℕ → ℝhf:AbsConvergent fhpos:∀ (n m : ℕ), 0 ≤ f (n, m)L:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mn:ℕm:ℤh✝:0 ≤ m⊢ 0 ≤ f (n, m.toNat)f:ℕ × ℕ → ℝhf:AbsConvergent fhpos:∀ (n m : ℕ), 0 ≤ f (n, m)L:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mn:ℕm:ℤh✝:¬0 ≤ m⊢ 0 ≤ 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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nn:ℕ⊢ ∃ M, ∀ (N : ℤ), (a n).partial N ≤ M
f:ℕ × ℕ → ℝhf:AbsConvergent fhpos:∀ (n m : ℕ), 0 ≤ f (n, m)L:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nn:ℕ⊢ ∀ (N : ℤ), (a n).partial N ≤ L; f:ℕ × ℕ → ℝhf:AbsConvergent fhpos:∀ (n m : ℕ), 0 ≤ f (n, m)L:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nn:ℕN:ℤ⊢ (a n).partial N ≤ L; f:ℕ × ℕ → ℝhf:AbsConvergent fhpos:∀ (n m : ℕ), 0 ≤ f (n, m)L:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nn:ℕN:ℤh:N ≥ 0⊢ (a n).partial N ≤ Lf:ℕ × ℕ → ℝhf:AbsConvergent fhpos:∀ (n m : ℕ), 0 ≤ f (n, m)L:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nn:ℕN:ℤh:¬N ≥ 0⊢ (a n).partial N ≤ L
f:ℕ × ℕ → ℝhf:AbsConvergent fhpos:∀ (n m : ℕ), 0 ≤ f (n, m)L:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nn:ℕN:ℤh:N ≥ 0⊢ (a n).partial N ≤ L f:ℕ × ℕ → ℝhf:AbsConvergent fhpos:∀ (n m : ℕ), 0 ≤ f (n, m)L:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nn:ℕN:ℕ⊢ (a n).partial ↑N ≤ L; All goals completed! 🐙
f:ℕ × ℕ → ℝhf:AbsConvergent fhpos:∀ (n m : ℕ), 0 ≤ f (n, m)L:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nn:ℕN:ℤh:¬N ≥ 0⊢ 0 ≤ 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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nN:ℤM:ℤhN:N ≥ 0⊢ ∑ n ∈ Icc 0 N, (a n.toNat).partial M ≤ Lf:ℕ × ℕ → ℝhf:AbsConvergent fhpos:∀ (n m : ℕ), 0 ≤ f (n, m)L:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nN:ℤ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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nN:ℤM:ℤhN:¬N ≥ 0⊢ ∑ n ∈ Icc 0 N, (a n.toNat).partial M ≤ Lf:ℕ × ℕ → ℝhf:AbsConvergent fhpos:∀ (n m : ℕ), 0 ≤ f (n, m)L:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nN:ℤ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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nN:ℤ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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nM:ℤN:ℕ⊢ ∑ n ∈ Icc 0 ↑N, (a n.toNat).partial M ≤ L
f:ℕ × ℕ → ℝhf:AbsConvergent fhpos:∀ (n m : ℕ), 0 ≤ f (n, m)L:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nM:ℤN:ℕhM:M ≥ 0⊢ ∑ n ∈ Icc 0 ↑N, (a n.toNat).partial M ≤ Lf:ℕ × ℕ → ℝhf:AbsConvergent fhpos:∀ (n m : ℕ), 0 ≤ f (n, m)L:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nM:ℤ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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nM:ℤN:ℕhM:¬M ≥ 0⊢ ∑ n ∈ Icc 0 ↑N, (a n.toNat).partial M ≤ Lf:ℕ × ℕ → ℝhf:AbsConvergent fhpos:∀ (n m : ℕ), 0 ≤ f (n, m)L:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nM:ℤ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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nM:ℤ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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nM:ℤ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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nM:ℤ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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nM:ℤN:ℕhM:¬M ≥ 0⊢ ∀ x ∈ Icc 0 ↑N, ∑ n ∈ Icc (a x.toNat).m M, (a x.toNat).seq n = 0; f:ℕ × ℕ → ℝhf:AbsConvergent fhpos:∀ (n m : ℕ), 0 ≤ f (n, m)L:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nM:ℤ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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nN:ℕM:ℕ⊢ ∑ n ∈ Icc 0 ↑N, (a n.toNat).partial ↑M ≤ L
f:ℕ × ℕ → ℝhf:AbsConvergent fhpos:∀ (n m : ℕ), 0 ≤ f (n, m)L:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nN:ℕ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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nN:ℕM:ℕ⊢ ∑ x ∈ Icc 0 N ×ˢ Icc 0 M, f x ≤ L
f:ℕ × ℕ → ℝhf:AbsConvergent fhpos:∀ (n m : ℕ), 0 ≤ f (n, m)L:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nN:ℕ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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nthis:∀ (N M : ℤ), ∑ n ∈ Finset.Icc 0 N, Chapter7.Series.partial (@_fvar.59781 n.toNat) M ≤ _fvar.59585 := fun N M => @?_mvar.102473 N MN:ℤ⊢ ∀ 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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nthis:∀ (N : ℤ), ∑ n ∈ Finset.Icc 0 N, Chapter7.Series.sum (@_fvar.59781 n.toNat) ≤ _fvar.59585 := fun N => @?_mvar.118395 NN:ℤ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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nthis:∀ (N : ℤ),
{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.partial
N ≤
_fvar.59585 :=
fun N => @?_mvar.120947 Nn:ℤ⊢ { 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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nthis:∀ (N : ℤ),
{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.partial
N ≤
_fvar.59585 :=
fun N => @?_mvar.120947 Nn:ℤ⊢ 0 ≤ if 0 ≤ n then (a n.toNat).sum else 0; f:ℕ × ℕ → ℝhf:AbsConvergent fhpos:∀ (n m : ℕ), 0 ≤ f (n, m)L:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nthis:∀ (N : ℤ),
{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.partial
N ≤
_fvar.59585 :=
fun N => @?_mvar.120947 Nn:ℤh✝:0 ≤ n⊢ 0 ≤ (a n.toNat).sumf:ℕ × ℕ → ℝhf:AbsConvergent fhpos:∀ (n m : ℕ), 0 ≤ f (n, m)L:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nthis:∀ (N : ℤ),
{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.partial
N ≤
_fvar.59585 :=
fun N => @?_mvar.120947 Nn:ℤh✝:¬0 ≤ n⊢ 0 ≤ 0
f:ℕ × ℕ → ℝhf:AbsConvergent fhpos:∀ (n m : ℕ), 0 ≤ f (n, m)L:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nthis:∀ (N : ℤ),
{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.partial
N ≤
_fvar.59585 :=
fun N => @?_mvar.120947 Nn:ℤh✝:0 ≤ n⊢ 0 ≤ (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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nthis:∀ (N : ℤ),
{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.partial
N ≤
_fvar.59585 :=
fun N => @?_mvar.120947 Nhnon':{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.nonneg :=
?_mvar.132169⊢ ∃ 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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nhnon':{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.nonneg :=
?_mvar.132169hconv':{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.converges :=
?_mvar.135140this:{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.sum ≤
_fvar.59585 :=
le_of_tendsto' (Chapter7.Series.convergesTo_sum _fvar.135141) _fvar.120948⊢ (∀ (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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nhnon':{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.nonneg :=
?_mvar.132169hconv':{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.converges :=
?_mvar.135140this:{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.sum ≤
_fvar.59585 :=
le_of_tendsto' (Chapter7.Series.convergesTo_sum _fvar.135141) _fvar.120948⊢ ∀ ε > 0, L - ε ≤ { m := 0, seq := fun n => if n ≥ 0 then (fun n => (a n).sum) n.toNat else 0, vanish := ⋯ }.sum; f:ℕ × ℕ → ℝhf:AbsConvergent fhpos:∀ (n m : ℕ), 0 ≤ f (n, m)L:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nhnon':{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.nonneg :=
?_mvar.132169hconv':{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.converges :=
?_mvar.135140this:{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.sum ≤
_fvar.59585 :=
le_of_tendsto' (Chapter7.Series.convergesTo_sum _fvar.135141) _fvar.120948ε:ℝhε:ε > 0⊢ L - ε ≤ { 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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nhnon':{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.nonneg :=
?_mvar.132169hconv':{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.converges :=
?_mvar.135140ε:ℝhε:ε > 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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 := ?_mvar.59914hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => @?_mvar.84999 Xhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 := fun n M => @?_mvar.85053 n Mhnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) := fun n => @?_mvar.92368 nhconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) := fun n => @?_mvar.97784 nhnon':{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.nonneg :=
?_mvar.132169hconv':{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.converges :=
?_mvar.135140ε:ℝhε:ε > 0X:Finset (ℕ × ℕ)hX:∑ p ∈ X, f p ≥ L - εN:ℕM:ℕhX':X ⊆ Icc 0 N ×ˢ Icc 0 M⊢ L - ε ≤ { 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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 :=
Eq.mpr
(id
(congrArg (LE.le 0)
(Eq.trans (dite_cond_eq_true (eq_true _fvar.59575))
(congrArg Chapter7.Series.sum
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) (Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0)
(fun n => if n ≥ 0 then (_fvar.59574 ∘ Exists.choose (of_eq_true (eq_true _fvar.59575))) n.toNat else 0)
(fun n =>
if 0 ≤ n then
@_fvar.59574
(((funext fun g =>
congrArg (fun x => Function.Bijective g ∧ x.absConverges)
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq)
(Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0) (fun n => if n ≥ 0 then (_fvar.59574 ∘ g) n.toNat else 0)
(fun n => if 0 ≤ n then @_fvar.59574 (g n.toNat) else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (g n.toNat))) fun a =>
Eq.refl 0)
(Chapter8.AbsConvergent._proof_1 _fvar.59574 g))) ▸
of_eq_true (eq_true _fvar.59575)).choose
n.toNat)
else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1
(fun a =>
congrArg (fun x => (_fvar.59574 ∘ x) n.toNat)
(Exists.choose.congr_simp
(funext fun g =>
congrArg (fun x => Function.Bijective g ∧ x.absConverges)
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq)
(Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0) (fun n => if n ≥ 0 then (_fvar.59574 ∘ g) n.toNat else 0)
(fun n => if 0 ≤ n then @_fvar.59574 (g n.toNat) else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (g n.toNat))) fun a =>
Eq.refl 0)
(Chapter8.AbsConvergent._proof_1 _fvar.59574 g)))
(of_eq_true (eq_true _fvar.59575))))
fun a => Eq.refl 0)
(Chapter8.Sum._proof_1 _fvar.59574 (of_eq_true (eq_true _fvar.59575))))))))
(Chapter7.Series.sum_of_nonneg fun n =>
if h : n ≥ 0 then
Eq.mpr
(id
(Eq.trans
(congrArg (fun x => x ≥ 0)
(ite_cond_eq_true
(@_fvar.59574
(((funext fun g =>
congrArg (fun x => Function.Bijective g ∧ x.absConverges)
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq)
(Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0) (fun n => if n ≥ 0 then (_fvar.59574 ∘ g) n.toNat else 0)
(fun n => if 0 ≤ n then @_fvar.59574 (g n.toNat) else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (g n.toNat))) fun a =>
Eq.refl 0)
(Chapter8.AbsConvergent._proof_1 _fvar.59574 g))) ▸
of_eq_true (eq_true _fvar.59575)).choose
n.toNat))
0 (eq_true h)))
ge_iff_le._simp_1))
(Chapter8.sum_of_sum_of_AbsConvergent_nonneg._proof_4 _fvar.59575 _fvar.59576 n h)
else
of_eq_true
(Eq.trans
(Eq.trans
(congrArg (fun x => x ≥ 0)
(ite_cond_eq_false
(@_fvar.59574
(((funext fun g =>
congrArg (fun x => Function.Bijective g ∧ x.absConverges)
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq)
(Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0) (fun n => if n ≥ 0 then (_fvar.59574 ∘ g) n.toNat else 0)
(fun n => if 0 ≤ n then @_fvar.59574 (g n.toNat) else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (g n.toNat))) fun a =>
Eq.refl 0)
(Chapter8.AbsConvergent._proof_1 _fvar.59574 g))) ▸
of_eq_true (eq_true _fvar.59575)).choose
n.toNat))
0 (eq_false h)))
ge_iff_le._simp_1)
(le_refl._simp_1 0)))hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => sorryhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 :=
fun n M =>
Eq.mpr
(id
(congrArg (fun x => x ≤ _fvar.59585)
(Eq.trans
(Eq.trans
(Finset.sum_congr (Chapter8.Finset.Icc_eq_cast M) fun x a =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (n, x.toNat))) fun a => Eq.refl 0)
(Finset.sum_map (Finset.Icc 0 M) Nat.castEmbedding fun x => if 0 ≤ x then @_fvar.59574 (n, x.toNat) else 0))
(Finset.sum_congr (Eq.refl (Finset.Icc 0 M)) fun x a =>
ite_cond_eq_true (@_fvar.59574 (n, (Nat.castEmbedding x).toNat)) 0 (Nat.cast_nonneg._simp_1 x)))))
(Eq.mpr
(eq_of_heq
((fun α self a a' e'_3 a_1 =>
Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a ≤ a_1) ≍ (a' ≤ a_1)) e'_3
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_3 : a = a'), e_3 ≍ Eq.refl a → (a ≤ a_1) ≍ (a' ≤ a_1))
(fun e_3 h => HEq.refl (a ≤ a_1)) (Eq.symm h) e'_3)
(Eq.refl a') (HEq.refl e'_3))
ℝ Real.instLE (∑ x ∈ Finset.Icc 0 M, @_fvar.59574 (n, x))
(∑ x ∈ Finset.map (Function.Embedding.sectR n ℕ) (Finset.Icc 0 M), @_fvar.59574 x)
(of_eq_true
(Eq.trans
(congrArg (Eq (∑ x ∈ Finset.Icc 0 M, @_fvar.59574 (n, x)))
(Eq.trans (Finset.sum_map (Finset.Icc 0 M) (Function.Embedding.sectR n ℕ) _fvar.59574)
(Finset.sum_congr (Eq.refl (Finset.Icc 0 M)) fun x a => Eq.refl (@_fvar.59574 (n, x)))))
(eq_self (∑ x ∈ Finset.Icc 0 M, @_fvar.59574 (n, x)))))
_fvar.59585))
(id (@_fvar.85000 (Finset.map (Function.Embedding.sectR n ℕ) (Finset.Icc 0 M)))))hnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) :=
fun n =>
Eq.mpr
(id
(forall_congr fun n_1 =>
Eq.trans
(congrArg (fun x => x ≥ 0)
(ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (n, n_1.toNat))) fun a => Eq.refl 0))
ge_iff_le._simp_1))
fun m =>
if h : 0 ≤ m then
Eq.mpr (id (congrArg (LE.le 0) (if_pos h))) (of_eq_true ((fun n m => eq_true (@_fvar.59576 n m)) n m.toNat))
else Eq.mpr (id (congrArg (LE.le 0) (if_neg h))) (of_eq_true (le_refl._simp_1 0))hconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) :=
fun n =>
Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter7.Series.converges_of_nonneg_iff (@_fvar.92369 n)))))
(Exists.intro _fvar.59585 fun N =>
if h : N ≥ 0 then
Exists.casesOn (CanLift.prf N h) fun N_1 h_1 =>
Eq.ndrec (motive := fun N => N ≥ 0 → Chapter7.Series.partial (@_fvar.59781 n) N ≤ _fvar.59585)
(fun h => @_fvar.85054 n N_1) h_1 h
else
Eq.mpr
(id
(congrArg (fun _a => _a ≤ _fvar.59585)
(Chapter7.Series.partial_of_lt
(id
(lt_of_not_ge fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
(Eq.refl (Int.negOfNat 1)))))
Mathlib.Tactic.Ring.neg_zero))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf N)
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
(Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
(Mathlib.Tactic.Ring.add_pf_add_zero (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))
(Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
(Mathlib.Tactic.Ring.add_pf_add_zero
(Nat.rawCast 1 + (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
(Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_zero_add (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))
(Mathlib.Tactic.Ring.atom_pf N)
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul N (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt
(Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_zero_add
(N ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero N (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0)))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
(Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
(Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
(neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
(Mathlib.Tactic.Linarith.sub_nonpos_of_le (Int.add_one_le_iff.mpr (lt_of_not_ge h))))
(Mathlib.Tactic.Linarith.sub_nonpos_of_le a))))))))
_fvar.59915)hnon':{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.nonneg :=
fun n =>
Eq.mpr
(id
(Eq.trans
(congrArg (fun x => x ≥ 0)
(ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (Chapter7.Series.sum (@_fvar.59781 n.toNat))) fun a =>
Eq.refl 0))
ge_iff_le._simp_1))
(if h : 0 ≤ n then
Eq.mpr (id (congrArg (LE.le 0) (if_pos h))) (Chapter7.Series.sum_of_nonneg (@_fvar.92369 n.toNat))
else Eq.mpr (id (congrArg (LE.le 0) (if_neg h))) (of_eq_true (le_refl._simp_1 0)))hconv':{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.converges :=
Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter7.Series.converges_of_nonneg_iff _fvar.132170))))
(Exists.intro _fvar.59585 _fvar.120948)ε:ℝhε:ε > 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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 :=
Eq.mpr
(id
(congrArg (LE.le 0)
(Eq.trans (dite_cond_eq_true (eq_true _fvar.59575))
(congrArg Chapter7.Series.sum
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) (Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0)
(fun n => if n ≥ 0 then (_fvar.59574 ∘ Exists.choose (of_eq_true (eq_true _fvar.59575))) n.toNat else 0)
(fun n =>
if 0 ≤ n then
@_fvar.59574
(((funext fun g =>
congrArg (fun x => Function.Bijective g ∧ x.absConverges)
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq)
(Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0) (fun n => if n ≥ 0 then (_fvar.59574 ∘ g) n.toNat else 0)
(fun n => if 0 ≤ n then @_fvar.59574 (g n.toNat) else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (g n.toNat))) fun a =>
Eq.refl 0)
(Chapter8.AbsConvergent._proof_1 _fvar.59574 g))) ▸
of_eq_true (eq_true _fvar.59575)).choose
n.toNat)
else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1
(fun a =>
congrArg (fun x => (_fvar.59574 ∘ x) n.toNat)
(Exists.choose.congr_simp
(funext fun g =>
congrArg (fun x => Function.Bijective g ∧ x.absConverges)
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq)
(Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0) (fun n => if n ≥ 0 then (_fvar.59574 ∘ g) n.toNat else 0)
(fun n => if 0 ≤ n then @_fvar.59574 (g n.toNat) else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (g n.toNat))) fun a =>
Eq.refl 0)
(Chapter8.AbsConvergent._proof_1 _fvar.59574 g)))
(of_eq_true (eq_true _fvar.59575))))
fun a => Eq.refl 0)
(Chapter8.Sum._proof_1 _fvar.59574 (of_eq_true (eq_true _fvar.59575))))))))
(Chapter7.Series.sum_of_nonneg fun n =>
if h : n ≥ 0 then
Eq.mpr
(id
(Eq.trans
(congrArg (fun x => x ≥ 0)
(ite_cond_eq_true
(@_fvar.59574
(((funext fun g =>
congrArg (fun x => Function.Bijective g ∧ x.absConverges)
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq)
(Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0) (fun n => if n ≥ 0 then (_fvar.59574 ∘ g) n.toNat else 0)
(fun n => if 0 ≤ n then @_fvar.59574 (g n.toNat) else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (g n.toNat))) fun a =>
Eq.refl 0)
(Chapter8.AbsConvergent._proof_1 _fvar.59574 g))) ▸
of_eq_true (eq_true _fvar.59575)).choose
n.toNat))
0 (eq_true h)))
ge_iff_le._simp_1))
(Chapter8.sum_of_sum_of_AbsConvergent_nonneg._proof_4 _fvar.59575 _fvar.59576 n h)
else
of_eq_true
(Eq.trans
(Eq.trans
(congrArg (fun x => x ≥ 0)
(ite_cond_eq_false
(@_fvar.59574
(((funext fun g =>
congrArg (fun x => Function.Bijective g ∧ x.absConverges)
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq)
(Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0) (fun n => if n ≥ 0 then (_fvar.59574 ∘ g) n.toNat else 0)
(fun n => if 0 ≤ n then @_fvar.59574 (g n.toNat) else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (g n.toNat))) fun a =>
Eq.refl 0)
(Chapter8.AbsConvergent._proof_1 _fvar.59574 g))) ▸
of_eq_true (eq_true _fvar.59575)).choose
n.toNat))
0 (eq_false h)))
ge_iff_le._simp_1)
(le_refl._simp_1 0)))hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => sorryhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 :=
fun n M =>
Eq.mpr
(id
(congrArg (fun x => x ≤ _fvar.59585)
(Eq.trans
(Eq.trans
(Finset.sum_congr (Chapter8.Finset.Icc_eq_cast M) fun x a =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (n, x.toNat))) fun a => Eq.refl 0)
(Finset.sum_map (Finset.Icc 0 M) Nat.castEmbedding fun x => if 0 ≤ x then @_fvar.59574 (n, x.toNat) else 0))
(Finset.sum_congr (Eq.refl (Finset.Icc 0 M)) fun x a =>
ite_cond_eq_true (@_fvar.59574 (n, (Nat.castEmbedding x).toNat)) 0 (Nat.cast_nonneg._simp_1 x)))))
(Eq.mpr
(eq_of_heq
((fun α self a a' e'_3 a_1 =>
Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a ≤ a_1) ≍ (a' ≤ a_1)) e'_3
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_3 : a = a'), e_3 ≍ Eq.refl a → (a ≤ a_1) ≍ (a' ≤ a_1))
(fun e_3 h => HEq.refl (a ≤ a_1)) (Eq.symm h) e'_3)
(Eq.refl a') (HEq.refl e'_3))
ℝ Real.instLE (∑ x ∈ Finset.Icc 0 M, @_fvar.59574 (n, x))
(∑ x ∈ Finset.map (Function.Embedding.sectR n ℕ) (Finset.Icc 0 M), @_fvar.59574 x)
(of_eq_true
(Eq.trans
(congrArg (Eq (∑ x ∈ Finset.Icc 0 M, @_fvar.59574 (n, x)))
(Eq.trans (Finset.sum_map (Finset.Icc 0 M) (Function.Embedding.sectR n ℕ) _fvar.59574)
(Finset.sum_congr (Eq.refl (Finset.Icc 0 M)) fun x a => Eq.refl (@_fvar.59574 (n, x)))))
(eq_self (∑ x ∈ Finset.Icc 0 M, @_fvar.59574 (n, x)))))
_fvar.59585))
(id (@_fvar.85000 (Finset.map (Function.Embedding.sectR n ℕ) (Finset.Icc 0 M)))))hnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) :=
fun n =>
Eq.mpr
(id
(forall_congr fun n_1 =>
Eq.trans
(congrArg (fun x => x ≥ 0)
(ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (n, n_1.toNat))) fun a => Eq.refl 0))
ge_iff_le._simp_1))
fun m =>
if h : 0 ≤ m then
Eq.mpr (id (congrArg (LE.le 0) (if_pos h))) (of_eq_true ((fun n m => eq_true (@_fvar.59576 n m)) n m.toNat))
else Eq.mpr (id (congrArg (LE.le 0) (if_neg h))) (of_eq_true (le_refl._simp_1 0))hconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) :=
fun n =>
Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter7.Series.converges_of_nonneg_iff (@_fvar.92369 n)))))
(Exists.intro _fvar.59585 fun N =>
if h : N ≥ 0 then
Exists.casesOn (CanLift.prf N h) fun N_1 h_1 =>
Eq.ndrec (motive := fun N => N ≥ 0 → Chapter7.Series.partial (@_fvar.59781 n) N ≤ _fvar.59585)
(fun h => @_fvar.85054 n N_1) h_1 h
else
Eq.mpr
(id
(congrArg (fun _a => _a ≤ _fvar.59585)
(Chapter7.Series.partial_of_lt
(id
(lt_of_not_ge fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
(Eq.refl (Int.negOfNat 1)))))
Mathlib.Tactic.Ring.neg_zero))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf N)
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
(Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
(Mathlib.Tactic.Ring.add_pf_add_zero (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))
(Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
(Mathlib.Tactic.Ring.add_pf_add_zero
(Nat.rawCast 1 + (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
(Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_zero_add (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))
(Mathlib.Tactic.Ring.atom_pf N)
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul N (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt
(Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_zero_add
(N ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero N (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0)))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
(Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
(Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
(neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
(Mathlib.Tactic.Linarith.sub_nonpos_of_le (Int.add_one_le_iff.mpr (lt_of_not_ge h))))
(Mathlib.Tactic.Linarith.sub_nonpos_of_le a))))))))
_fvar.59915)hnon':{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.nonneg :=
fun n =>
Eq.mpr
(id
(Eq.trans
(congrArg (fun x => x ≥ 0)
(ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (Chapter7.Series.sum (@_fvar.59781 n.toNat))) fun a =>
Eq.refl 0))
ge_iff_le._simp_1))
(if h : 0 ≤ n then
Eq.mpr (id (congrArg (LE.le 0) (if_pos h))) (Chapter7.Series.sum_of_nonneg (@_fvar.92369 n.toNat))
else Eq.mpr (id (congrArg (LE.le 0) (if_neg h))) (of_eq_true (le_refl._simp_1 0)))hconv':{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.converges :=
Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter7.Series.converges_of_nonneg_iff _fvar.132170))))
(Exists.intro _fvar.59585 _fvar.120948)ε:ℝhε:ε > 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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 :=
Eq.mpr
(id
(congrArg (LE.le 0)
(Eq.trans (dite_cond_eq_true (eq_true _fvar.59575))
(congrArg Chapter7.Series.sum
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) (Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0)
(fun n => if n ≥ 0 then (_fvar.59574 ∘ Exists.choose (of_eq_true (eq_true _fvar.59575))) n.toNat else 0)
(fun n =>
if 0 ≤ n then
@_fvar.59574
(((funext fun g =>
congrArg (fun x => Function.Bijective g ∧ x.absConverges)
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq)
(Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0) (fun n => if n ≥ 0 then (_fvar.59574 ∘ g) n.toNat else 0)
(fun n => if 0 ≤ n then @_fvar.59574 (g n.toNat) else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (g n.toNat))) fun a =>
Eq.refl 0)
(Chapter8.AbsConvergent._proof_1 _fvar.59574 g))) ▸
of_eq_true (eq_true _fvar.59575)).choose
n.toNat)
else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1
(fun a =>
congrArg (fun x => (_fvar.59574 ∘ x) n.toNat)
(Exists.choose.congr_simp
(funext fun g =>
congrArg (fun x => Function.Bijective g ∧ x.absConverges)
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq)
(Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0) (fun n => if n ≥ 0 then (_fvar.59574 ∘ g) n.toNat else 0)
(fun n => if 0 ≤ n then @_fvar.59574 (g n.toNat) else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (g n.toNat))) fun a =>
Eq.refl 0)
(Chapter8.AbsConvergent._proof_1 _fvar.59574 g)))
(of_eq_true (eq_true _fvar.59575))))
fun a => Eq.refl 0)
(Chapter8.Sum._proof_1 _fvar.59574 (of_eq_true (eq_true _fvar.59575))))))))
(Chapter7.Series.sum_of_nonneg fun n =>
if h : n ≥ 0 then
Eq.mpr
(id
(Eq.trans
(congrArg (fun x => x ≥ 0)
(ite_cond_eq_true
(@_fvar.59574
(((funext fun g =>
congrArg (fun x => Function.Bijective g ∧ x.absConverges)
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq)
(Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0) (fun n => if n ≥ 0 then (_fvar.59574 ∘ g) n.toNat else 0)
(fun n => if 0 ≤ n then @_fvar.59574 (g n.toNat) else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (g n.toNat))) fun a =>
Eq.refl 0)
(Chapter8.AbsConvergent._proof_1 _fvar.59574 g))) ▸
of_eq_true (eq_true _fvar.59575)).choose
n.toNat))
0 (eq_true h)))
ge_iff_le._simp_1))
(Chapter8.sum_of_sum_of_AbsConvergent_nonneg._proof_4 _fvar.59575 _fvar.59576 n h)
else
of_eq_true
(Eq.trans
(Eq.trans
(congrArg (fun x => x ≥ 0)
(ite_cond_eq_false
(@_fvar.59574
(((funext fun g =>
congrArg (fun x => Function.Bijective g ∧ x.absConverges)
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq)
(Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0) (fun n => if n ≥ 0 then (_fvar.59574 ∘ g) n.toNat else 0)
(fun n => if 0 ≤ n then @_fvar.59574 (g n.toNat) else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (g n.toNat))) fun a =>
Eq.refl 0)
(Chapter8.AbsConvergent._proof_1 _fvar.59574 g))) ▸
of_eq_true (eq_true _fvar.59575)).choose
n.toNat))
0 (eq_false h)))
ge_iff_le._simp_1)
(le_refl._simp_1 0)))hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => sorryhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 :=
fun n M =>
Eq.mpr
(id
(congrArg (fun x => x ≤ _fvar.59585)
(Eq.trans
(Eq.trans
(Finset.sum_congr (Chapter8.Finset.Icc_eq_cast M) fun x a =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (n, x.toNat))) fun a => Eq.refl 0)
(Finset.sum_map (Finset.Icc 0 M) Nat.castEmbedding fun x => if 0 ≤ x then @_fvar.59574 (n, x.toNat) else 0))
(Finset.sum_congr (Eq.refl (Finset.Icc 0 M)) fun x a =>
ite_cond_eq_true (@_fvar.59574 (n, (Nat.castEmbedding x).toNat)) 0 (Nat.cast_nonneg._simp_1 x)))))
(Eq.mpr
(eq_of_heq
((fun α self a a' e'_3 a_1 =>
Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a ≤ a_1) ≍ (a' ≤ a_1)) e'_3
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_3 : a = a'), e_3 ≍ Eq.refl a → (a ≤ a_1) ≍ (a' ≤ a_1))
(fun e_3 h => HEq.refl (a ≤ a_1)) (Eq.symm h) e'_3)
(Eq.refl a') (HEq.refl e'_3))
ℝ Real.instLE (∑ x ∈ Finset.Icc 0 M, @_fvar.59574 (n, x))
(∑ x ∈ Finset.map (Function.Embedding.sectR n ℕ) (Finset.Icc 0 M), @_fvar.59574 x)
(of_eq_true
(Eq.trans
(congrArg (Eq (∑ x ∈ Finset.Icc 0 M, @_fvar.59574 (n, x)))
(Eq.trans (Finset.sum_map (Finset.Icc 0 M) (Function.Embedding.sectR n ℕ) _fvar.59574)
(Finset.sum_congr (Eq.refl (Finset.Icc 0 M)) fun x a => Eq.refl (@_fvar.59574 (n, x)))))
(eq_self (∑ x ∈ Finset.Icc 0 M, @_fvar.59574 (n, x)))))
_fvar.59585))
(id (@_fvar.85000 (Finset.map (Function.Embedding.sectR n ℕ) (Finset.Icc 0 M)))))hnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) :=
fun n =>
Eq.mpr
(id
(forall_congr fun n_1 =>
Eq.trans
(congrArg (fun x => x ≥ 0)
(ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (n, n_1.toNat))) fun a => Eq.refl 0))
ge_iff_le._simp_1))
fun m =>
if h : 0 ≤ m then
Eq.mpr (id (congrArg (LE.le 0) (if_pos h))) (of_eq_true ((fun n m => eq_true (@_fvar.59576 n m)) n m.toNat))
else Eq.mpr (id (congrArg (LE.le 0) (if_neg h))) (of_eq_true (le_refl._simp_1 0))hconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) :=
fun n =>
Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter7.Series.converges_of_nonneg_iff (@_fvar.92369 n)))))
(Exists.intro _fvar.59585 fun N =>
if h : N ≥ 0 then
Exists.casesOn (CanLift.prf N h) fun N_1 h_1 =>
Eq.ndrec (motive := fun N => N ≥ 0 → Chapter7.Series.partial (@_fvar.59781 n) N ≤ _fvar.59585)
(fun h => @_fvar.85054 n N_1) h_1 h
else
Eq.mpr
(id
(congrArg (fun _a => _a ≤ _fvar.59585)
(Chapter7.Series.partial_of_lt
(id
(lt_of_not_ge fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
(Eq.refl (Int.negOfNat 1)))))
Mathlib.Tactic.Ring.neg_zero))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf N)
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
(Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
(Mathlib.Tactic.Ring.add_pf_add_zero (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))
(Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
(Mathlib.Tactic.Ring.add_pf_add_zero
(Nat.rawCast 1 + (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
(Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_zero_add (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))
(Mathlib.Tactic.Ring.atom_pf N)
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul N (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt
(Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_zero_add
(N ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero N (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0)))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
(Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
(Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
(neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
(Mathlib.Tactic.Linarith.sub_nonpos_of_le (Int.add_one_le_iff.mpr (lt_of_not_ge h))))
(Mathlib.Tactic.Linarith.sub_nonpos_of_le a))))))))
_fvar.59915)hnon':{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.nonneg :=
fun n =>
Eq.mpr
(id
(Eq.trans
(congrArg (fun x => x ≥ 0)
(ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (Chapter7.Series.sum (@_fvar.59781 n.toNat))) fun a =>
Eq.refl 0))
ge_iff_le._simp_1))
(if h : 0 ≤ n then
Eq.mpr (id (congrArg (LE.le 0) (if_pos h))) (Chapter7.Series.sum_of_nonneg (@_fvar.92369 n.toNat))
else Eq.mpr (id (congrArg (LE.le 0) (if_neg h))) (of_eq_true (le_refl._simp_1 0)))hconv':{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.converges :=
Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter7.Series.converges_of_nonneg_iff _fvar.132170))))
(Exists.intro _fvar.59585 _fvar.120948)ε:ℝhε:ε > 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; f:ℕ × ℕ → ℝhf:AbsConvergent fhpos:∀ (n m : ℕ), 0 ≤ f (n, m)L:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 :=
Eq.mpr
(id
(congrArg (LE.le 0)
(Eq.trans (dite_cond_eq_true (eq_true _fvar.59575))
(congrArg Chapter7.Series.sum
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) (Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0)
(fun n => if n ≥ 0 then (_fvar.59574 ∘ Exists.choose (of_eq_true (eq_true _fvar.59575))) n.toNat else 0)
(fun n =>
if 0 ≤ n then
@_fvar.59574
(((funext fun g =>
congrArg (fun x => Function.Bijective g ∧ x.absConverges)
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq)
(Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0) (fun n => if n ≥ 0 then (_fvar.59574 ∘ g) n.toNat else 0)
(fun n => if 0 ≤ n then @_fvar.59574 (g n.toNat) else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (g n.toNat))) fun a =>
Eq.refl 0)
(Chapter8.AbsConvergent._proof_1 _fvar.59574 g))) ▸
of_eq_true (eq_true _fvar.59575)).choose
n.toNat)
else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1
(fun a =>
congrArg (fun x => (_fvar.59574 ∘ x) n.toNat)
(Exists.choose.congr_simp
(funext fun g =>
congrArg (fun x => Function.Bijective g ∧ x.absConverges)
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq)
(Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0) (fun n => if n ≥ 0 then (_fvar.59574 ∘ g) n.toNat else 0)
(fun n => if 0 ≤ n then @_fvar.59574 (g n.toNat) else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (g n.toNat))) fun a =>
Eq.refl 0)
(Chapter8.AbsConvergent._proof_1 _fvar.59574 g)))
(of_eq_true (eq_true _fvar.59575))))
fun a => Eq.refl 0)
(Chapter8.Sum._proof_1 _fvar.59574 (of_eq_true (eq_true _fvar.59575))))))))
(Chapter7.Series.sum_of_nonneg fun n =>
if h : n ≥ 0 then
Eq.mpr
(id
(Eq.trans
(congrArg (fun x => x ≥ 0)
(ite_cond_eq_true
(@_fvar.59574
(((funext fun g =>
congrArg (fun x => Function.Bijective g ∧ x.absConverges)
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq)
(Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0) (fun n => if n ≥ 0 then (_fvar.59574 ∘ g) n.toNat else 0)
(fun n => if 0 ≤ n then @_fvar.59574 (g n.toNat) else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (g n.toNat))) fun a =>
Eq.refl 0)
(Chapter8.AbsConvergent._proof_1 _fvar.59574 g))) ▸
of_eq_true (eq_true _fvar.59575)).choose
n.toNat))
0 (eq_true h)))
ge_iff_le._simp_1))
(Chapter8.sum_of_sum_of_AbsConvergent_nonneg._proof_4 _fvar.59575 _fvar.59576 n h)
else
of_eq_true
(Eq.trans
(Eq.trans
(congrArg (fun x => x ≥ 0)
(ite_cond_eq_false
(@_fvar.59574
(((funext fun g =>
congrArg (fun x => Function.Bijective g ∧ x.absConverges)
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq)
(Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0) (fun n => if n ≥ 0 then (_fvar.59574 ∘ g) n.toNat else 0)
(fun n => if 0 ≤ n then @_fvar.59574 (g n.toNat) else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (g n.toNat))) fun a =>
Eq.refl 0)
(Chapter8.AbsConvergent._proof_1 _fvar.59574 g))) ▸
of_eq_true (eq_true _fvar.59575)).choose
n.toNat))
0 (eq_false h)))
ge_iff_le._simp_1)
(le_refl._simp_1 0)))hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => sorryhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 :=
fun n M =>
Eq.mpr
(id
(congrArg (fun x => x ≤ _fvar.59585)
(Eq.trans
(Eq.trans
(Finset.sum_congr (Chapter8.Finset.Icc_eq_cast M) fun x a =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (n, x.toNat))) fun a => Eq.refl 0)
(Finset.sum_map (Finset.Icc 0 M) Nat.castEmbedding fun x => if 0 ≤ x then @_fvar.59574 (n, x.toNat) else 0))
(Finset.sum_congr (Eq.refl (Finset.Icc 0 M)) fun x a =>
ite_cond_eq_true (@_fvar.59574 (n, (Nat.castEmbedding x).toNat)) 0 (Nat.cast_nonneg._simp_1 x)))))
(Eq.mpr
(eq_of_heq
((fun α self a a' e'_3 a_1 =>
Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a ≤ a_1) ≍ (a' ≤ a_1)) e'_3
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_3 : a = a'), e_3 ≍ Eq.refl a → (a ≤ a_1) ≍ (a' ≤ a_1))
(fun e_3 h => HEq.refl (a ≤ a_1)) (Eq.symm h) e'_3)
(Eq.refl a') (HEq.refl e'_3))
ℝ Real.instLE (∑ x ∈ Finset.Icc 0 M, @_fvar.59574 (n, x))
(∑ x ∈ Finset.map (Function.Embedding.sectR n ℕ) (Finset.Icc 0 M), @_fvar.59574 x)
(of_eq_true
(Eq.trans
(congrArg (Eq (∑ x ∈ Finset.Icc 0 M, @_fvar.59574 (n, x)))
(Eq.trans (Finset.sum_map (Finset.Icc 0 M) (Function.Embedding.sectR n ℕ) _fvar.59574)
(Finset.sum_congr (Eq.refl (Finset.Icc 0 M)) fun x a => Eq.refl (@_fvar.59574 (n, x)))))
(eq_self (∑ x ∈ Finset.Icc 0 M, @_fvar.59574 (n, x)))))
_fvar.59585))
(id (@_fvar.85000 (Finset.map (Function.Embedding.sectR n ℕ) (Finset.Icc 0 M)))))hnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) :=
fun n =>
Eq.mpr
(id
(forall_congr fun n_1 =>
Eq.trans
(congrArg (fun x => x ≥ 0)
(ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (n, n_1.toNat))) fun a => Eq.refl 0))
ge_iff_le._simp_1))
fun m =>
if h : 0 ≤ m then
Eq.mpr (id (congrArg (LE.le 0) (if_pos h))) (of_eq_true ((fun n m => eq_true (@_fvar.59576 n m)) n m.toNat))
else Eq.mpr (id (congrArg (LE.le 0) (if_neg h))) (of_eq_true (le_refl._simp_1 0))hconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) :=
fun n =>
Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter7.Series.converges_of_nonneg_iff (@_fvar.92369 n)))))
(Exists.intro _fvar.59585 fun N =>
if h : N ≥ 0 then
Exists.casesOn (CanLift.prf N h) fun N_1 h_1 =>
Eq.ndrec (motive := fun N => N ≥ 0 → Chapter7.Series.partial (@_fvar.59781 n) N ≤ _fvar.59585)
(fun h => @_fvar.85054 n N_1) h_1 h
else
Eq.mpr
(id
(congrArg (fun _a => _a ≤ _fvar.59585)
(Chapter7.Series.partial_of_lt
(id
(lt_of_not_ge fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
(Eq.refl (Int.negOfNat 1)))))
Mathlib.Tactic.Ring.neg_zero))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf N)
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
(Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
(Mathlib.Tactic.Ring.add_pf_add_zero (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))
(Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
(Mathlib.Tactic.Ring.add_pf_add_zero
(Nat.rawCast 1 + (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
(Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_zero_add (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))
(Mathlib.Tactic.Ring.atom_pf N)
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul N (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt
(Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_zero_add
(N ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero N (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0)))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
(Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
(Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
(neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
(Mathlib.Tactic.Linarith.sub_nonpos_of_le (Int.add_one_le_iff.mpr (lt_of_not_ge h))))
(Mathlib.Tactic.Linarith.sub_nonpos_of_le a))))))))
_fvar.59915)hnon':{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.nonneg :=
fun n =>
Eq.mpr
(id
(Eq.trans
(congrArg (fun x => x ≥ 0)
(ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (Chapter7.Series.sum (@_fvar.59781 n.toNat))) fun a =>
Eq.refl 0))
ge_iff_le._simp_1))
(if h : 0 ≤ n then
Eq.mpr (id (congrArg (LE.le 0) (if_pos h))) (Chapter7.Series.sum_of_nonneg (@_fvar.92369 n.toNat))
else Eq.mpr (id (congrArg (LE.le 0) (if_neg h))) (of_eq_true (le_refl._simp_1 0)))hconv':{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.converges :=
Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter7.Series.converges_of_nonneg_iff _fvar.132170))))
(Exists.intro _fvar.59585 _fvar.120948)ε:ℝhε:ε > 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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 :=
Eq.mpr
(id
(congrArg (LE.le 0)
(Eq.trans (dite_cond_eq_true (eq_true _fvar.59575))
(congrArg Chapter7.Series.sum
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) (Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0)
(fun n => if n ≥ 0 then (_fvar.59574 ∘ Exists.choose (of_eq_true (eq_true _fvar.59575))) n.toNat else 0)
(fun n =>
if 0 ≤ n then
@_fvar.59574
(((funext fun g =>
congrArg (fun x => Function.Bijective g ∧ x.absConverges)
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq)
(Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0) (fun n => if n ≥ 0 then (_fvar.59574 ∘ g) n.toNat else 0)
(fun n => if 0 ≤ n then @_fvar.59574 (g n.toNat) else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (g n.toNat))) fun a =>
Eq.refl 0)
(Chapter8.AbsConvergent._proof_1 _fvar.59574 g))) ▸
of_eq_true (eq_true _fvar.59575)).choose
n.toNat)
else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1
(fun a =>
congrArg (fun x => (_fvar.59574 ∘ x) n.toNat)
(Exists.choose.congr_simp
(funext fun g =>
congrArg (fun x => Function.Bijective g ∧ x.absConverges)
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq)
(Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0) (fun n => if n ≥ 0 then (_fvar.59574 ∘ g) n.toNat else 0)
(fun n => if 0 ≤ n then @_fvar.59574 (g n.toNat) else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (g n.toNat))) fun a =>
Eq.refl 0)
(Chapter8.AbsConvergent._proof_1 _fvar.59574 g)))
(of_eq_true (eq_true _fvar.59575))))
fun a => Eq.refl 0)
(Chapter8.Sum._proof_1 _fvar.59574 (of_eq_true (eq_true _fvar.59575))))))))
(Chapter7.Series.sum_of_nonneg fun n =>
if h : n ≥ 0 then
Eq.mpr
(id
(Eq.trans
(congrArg (fun x => x ≥ 0)
(ite_cond_eq_true
(@_fvar.59574
(((funext fun g =>
congrArg (fun x => Function.Bijective g ∧ x.absConverges)
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq)
(Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0) (fun n => if n ≥ 0 then (_fvar.59574 ∘ g) n.toNat else 0)
(fun n => if 0 ≤ n then @_fvar.59574 (g n.toNat) else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (g n.toNat))) fun a =>
Eq.refl 0)
(Chapter8.AbsConvergent._proof_1 _fvar.59574 g))) ▸
of_eq_true (eq_true _fvar.59575)).choose
n.toNat))
0 (eq_true h)))
ge_iff_le._simp_1))
(Chapter8.sum_of_sum_of_AbsConvergent_nonneg._proof_4 _fvar.59575 _fvar.59576 n h)
else
of_eq_true
(Eq.trans
(Eq.trans
(congrArg (fun x => x ≥ 0)
(ite_cond_eq_false
(@_fvar.59574
(((funext fun g =>
congrArg (fun x => Function.Bijective g ∧ x.absConverges)
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq)
(Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0) (fun n => if n ≥ 0 then (_fvar.59574 ∘ g) n.toNat else 0)
(fun n => if 0 ≤ n then @_fvar.59574 (g n.toNat) else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (g n.toNat))) fun a =>
Eq.refl 0)
(Chapter8.AbsConvergent._proof_1 _fvar.59574 g))) ▸
of_eq_true (eq_true _fvar.59575)).choose
n.toNat))
0 (eq_false h)))
ge_iff_le._simp_1)
(le_refl._simp_1 0)))hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => sorryhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 :=
fun n M =>
Eq.mpr
(id
(congrArg (fun x => x ≤ _fvar.59585)
(Eq.trans
(Eq.trans
(Finset.sum_congr (Chapter8.Finset.Icc_eq_cast M) fun x a =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (n, x.toNat))) fun a => Eq.refl 0)
(Finset.sum_map (Finset.Icc 0 M) Nat.castEmbedding fun x => if 0 ≤ x then @_fvar.59574 (n, x.toNat) else 0))
(Finset.sum_congr (Eq.refl (Finset.Icc 0 M)) fun x a =>
ite_cond_eq_true (@_fvar.59574 (n, (Nat.castEmbedding x).toNat)) 0 (Nat.cast_nonneg._simp_1 x)))))
(Eq.mpr
(eq_of_heq
((fun α self a a' e'_3 a_1 =>
Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a ≤ a_1) ≍ (a' ≤ a_1)) e'_3
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_3 : a = a'), e_3 ≍ Eq.refl a → (a ≤ a_1) ≍ (a' ≤ a_1))
(fun e_3 h => HEq.refl (a ≤ a_1)) (Eq.symm h) e'_3)
(Eq.refl a') (HEq.refl e'_3))
ℝ Real.instLE (∑ x ∈ Finset.Icc 0 M, @_fvar.59574 (n, x))
(∑ x ∈ Finset.map (Function.Embedding.sectR n ℕ) (Finset.Icc 0 M), @_fvar.59574 x)
(of_eq_true
(Eq.trans
(congrArg (Eq (∑ x ∈ Finset.Icc 0 M, @_fvar.59574 (n, x)))
(Eq.trans (Finset.sum_map (Finset.Icc 0 M) (Function.Embedding.sectR n ℕ) _fvar.59574)
(Finset.sum_congr (Eq.refl (Finset.Icc 0 M)) fun x a => Eq.refl (@_fvar.59574 (n, x)))))
(eq_self (∑ x ∈ Finset.Icc 0 M, @_fvar.59574 (n, x)))))
_fvar.59585))
(id (@_fvar.85000 (Finset.map (Function.Embedding.sectR n ℕ) (Finset.Icc 0 M)))))hnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) :=
fun n =>
Eq.mpr
(id
(forall_congr fun n_1 =>
Eq.trans
(congrArg (fun x => x ≥ 0)
(ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (n, n_1.toNat))) fun a => Eq.refl 0))
ge_iff_le._simp_1))
fun m =>
if h : 0 ≤ m then
Eq.mpr (id (congrArg (LE.le 0) (if_pos h))) (of_eq_true ((fun n m => eq_true (@_fvar.59576 n m)) n m.toNat))
else Eq.mpr (id (congrArg (LE.le 0) (if_neg h))) (of_eq_true (le_refl._simp_1 0))hconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) :=
fun n =>
Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter7.Series.converges_of_nonneg_iff (@_fvar.92369 n)))))
(Exists.intro _fvar.59585 fun N =>
if h : N ≥ 0 then
Exists.casesOn (CanLift.prf N h) fun N_1 h_1 =>
Eq.ndrec (motive := fun N => N ≥ 0 → Chapter7.Series.partial (@_fvar.59781 n) N ≤ _fvar.59585)
(fun h => @_fvar.85054 n N_1) h_1 h
else
Eq.mpr
(id
(congrArg (fun _a => _a ≤ _fvar.59585)
(Chapter7.Series.partial_of_lt
(id
(lt_of_not_ge fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
(Eq.refl (Int.negOfNat 1)))))
Mathlib.Tactic.Ring.neg_zero))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf N)
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
(Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
(Mathlib.Tactic.Ring.add_pf_add_zero (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))
(Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
(Mathlib.Tactic.Ring.add_pf_add_zero
(Nat.rawCast 1 + (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
(Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_zero_add (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))
(Mathlib.Tactic.Ring.atom_pf N)
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul N (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt
(Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_zero_add
(N ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero N (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0)))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
(Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
(Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
(neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
(Mathlib.Tactic.Linarith.sub_nonpos_of_le (Int.add_one_le_iff.mpr (lt_of_not_ge h))))
(Mathlib.Tactic.Linarith.sub_nonpos_of_le a))))))))
_fvar.59915)hnon':{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.nonneg :=
fun n =>
Eq.mpr
(id
(Eq.trans
(congrArg (fun x => x ≥ 0)
(ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (Chapter7.Series.sum (@_fvar.59781 n.toNat))) fun a =>
Eq.refl 0))
ge_iff_le._simp_1))
(if h : 0 ≤ n then
Eq.mpr (id (congrArg (LE.le 0) (if_pos h))) (Chapter7.Series.sum_of_nonneg (@_fvar.92369 n.toNat))
else Eq.mpr (id (congrArg (LE.le 0) (if_neg h))) (of_eq_true (le_refl._simp_1 0)))hconv':{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.converges :=
Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter7.Series.converges_of_nonneg_iff _fvar.132170))))
(Exists.intro _fvar.59585 _fvar.120948)ε:ℝhε:ε > 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:ℝ := Chapter8.Sum _fvar.59574a:ℕ → Chapter7.Series := fun n => { m := 0, seq := fun n_1 => if n_1 ≥ 0 then (@fun m => @_fvar.59574 (n, m)) n_1.toNat else 0, vanish := ⋯ }hLpos:0 ≤ _fvar.59585 :=
Eq.mpr
(id
(congrArg (LE.le 0)
(Eq.trans (dite_cond_eq_true (eq_true _fvar.59575))
(congrArg Chapter7.Series.sum
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) (Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0)
(fun n => if n ≥ 0 then (_fvar.59574 ∘ Exists.choose (of_eq_true (eq_true _fvar.59575))) n.toNat else 0)
(fun n =>
if 0 ≤ n then
@_fvar.59574
(((funext fun g =>
congrArg (fun x => Function.Bijective g ∧ x.absConverges)
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq)
(Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0) (fun n => if n ≥ 0 then (_fvar.59574 ∘ g) n.toNat else 0)
(fun n => if 0 ≤ n then @_fvar.59574 (g n.toNat) else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (g n.toNat))) fun a =>
Eq.refl 0)
(Chapter8.AbsConvergent._proof_1 _fvar.59574 g))) ▸
of_eq_true (eq_true _fvar.59575)).choose
n.toNat)
else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1
(fun a =>
congrArg (fun x => (_fvar.59574 ∘ x) n.toNat)
(Exists.choose.congr_simp
(funext fun g =>
congrArg (fun x => Function.Bijective g ∧ x.absConverges)
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq)
(Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0) (fun n => if n ≥ 0 then (_fvar.59574 ∘ g) n.toNat else 0)
(fun n => if 0 ≤ n then @_fvar.59574 (g n.toNat) else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (g n.toNat))) fun a =>
Eq.refl 0)
(Chapter8.AbsConvergent._proof_1 _fvar.59574 g)))
(of_eq_true (eq_true _fvar.59575))))
fun a => Eq.refl 0)
(Chapter8.Sum._proof_1 _fvar.59574 (of_eq_true (eq_true _fvar.59575))))))))
(Chapter7.Series.sum_of_nonneg fun n =>
if h : n ≥ 0 then
Eq.mpr
(id
(Eq.trans
(congrArg (fun x => x ≥ 0)
(ite_cond_eq_true
(@_fvar.59574
(((funext fun g =>
congrArg (fun x => Function.Bijective g ∧ x.absConverges)
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq)
(Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0) (fun n => if n ≥ 0 then (_fvar.59574 ∘ g) n.toNat else 0)
(fun n => if 0 ≤ n then @_fvar.59574 (g n.toNat) else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (g n.toNat))) fun a =>
Eq.refl 0)
(Chapter8.AbsConvergent._proof_1 _fvar.59574 g))) ▸
of_eq_true (eq_true _fvar.59575)).choose
n.toNat))
0 (eq_true h)))
ge_iff_le._simp_1))
(Chapter8.sum_of_sum_of_AbsConvergent_nonneg._proof_4 _fvar.59575 _fvar.59576 n h)
else
of_eq_true
(Eq.trans
(Eq.trans
(congrArg (fun x => x ≥ 0)
(ite_cond_eq_false
(@_fvar.59574
(((funext fun g =>
congrArg (fun x => Function.Bijective g ∧ x.absConverges)
((fun m m_1 e_m =>
Eq.rec (motive := fun m_2 e_m =>
∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m_2, seq := seq_1,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m })
(fun seq seq_1 e_seq =>
Eq.rec (motive := fun seq_2 e_seq =>
∀ (vanish : ∀ n < m, seq n = 0),
{ m := m, seq := seq, vanish := vanish } =
{ m := m, seq := seq_2,
vanish :=
Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0)
(Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq)
(Eq.refl m) })
(fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq)
e_m)
0 0 (Eq.refl 0) (fun n => if n ≥ 0 then (_fvar.59574 ∘ g) n.toNat else 0)
(fun n => if 0 ≤ n then @_fvar.59574 (g n.toNat) else 0)
(funext fun n =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (g n.toNat))) fun a =>
Eq.refl 0)
(Chapter8.AbsConvergent._proof_1 _fvar.59574 g))) ▸
of_eq_true (eq_true _fvar.59575)).choose
n.toNat))
0 (eq_false h)))
ge_iff_le._simp_1)
(le_refl._simp_1 0)))hfinsum:∀ (X : Finset (ℕ × ℕ)), ∑ p ∈ X, @_fvar.59574 p ≤ _fvar.59585 := fun X => sorryhfinsum':∀ (n M : ℕ), Chapter7.Series.partial (@_fvar.59781 n) ↑M ≤ _fvar.59585 :=
fun n M =>
Eq.mpr
(id
(congrArg (fun x => x ≤ _fvar.59585)
(Eq.trans
(Eq.trans
(Finset.sum_congr (Chapter8.Finset.Icc_eq_cast M) fun x a =>
ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (n, x.toNat))) fun a => Eq.refl 0)
(Finset.sum_map (Finset.Icc 0 M) Nat.castEmbedding fun x => if 0 ≤ x then @_fvar.59574 (n, x.toNat) else 0))
(Finset.sum_congr (Eq.refl (Finset.Icc 0 M)) fun x a =>
ite_cond_eq_true (@_fvar.59574 (n, (Nat.castEmbedding x).toNat)) 0 (Nat.cast_nonneg._simp_1 x)))))
(Eq.mpr
(eq_of_heq
((fun α self a a' e'_3 a_1 =>
Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a ≤ a_1) ≍ (a' ≤ a_1)) e'_3
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_3 : a = a'), e_3 ≍ Eq.refl a → (a ≤ a_1) ≍ (a' ≤ a_1))
(fun e_3 h => HEq.refl (a ≤ a_1)) (Eq.symm h) e'_3)
(Eq.refl a') (HEq.refl e'_3))
ℝ Real.instLE (∑ x ∈ Finset.Icc 0 M, @_fvar.59574 (n, x))
(∑ x ∈ Finset.map (Function.Embedding.sectR n ℕ) (Finset.Icc 0 M), @_fvar.59574 x)
(of_eq_true
(Eq.trans
(congrArg (Eq (∑ x ∈ Finset.Icc 0 M, @_fvar.59574 (n, x)))
(Eq.trans (Finset.sum_map (Finset.Icc 0 M) (Function.Embedding.sectR n ℕ) _fvar.59574)
(Finset.sum_congr (Eq.refl (Finset.Icc 0 M)) fun x a => Eq.refl (@_fvar.59574 (n, x)))))
(eq_self (∑ x ∈ Finset.Icc 0 M, @_fvar.59574 (n, x)))))
_fvar.59585))
(id (@_fvar.85000 (Finset.map (Function.Embedding.sectR n ℕ) (Finset.Icc 0 M)))))hnon:∀ (n : ℕ), Chapter7.Series.nonneg (@_fvar.59781 n) :=
fun n =>
Eq.mpr
(id
(forall_congr fun n_1 =>
Eq.trans
(congrArg (fun x => x ≥ 0)
(ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.59574 (n, n_1.toNat))) fun a => Eq.refl 0))
ge_iff_le._simp_1))
fun m =>
if h : 0 ≤ m then
Eq.mpr (id (congrArg (LE.le 0) (if_pos h))) (of_eq_true ((fun n m => eq_true (@_fvar.59576 n m)) n m.toNat))
else Eq.mpr (id (congrArg (LE.le 0) (if_neg h))) (of_eq_true (le_refl._simp_1 0))hconv:∀ (n : ℕ), Chapter7.Series.converges (@_fvar.59781 n) :=
fun n =>
Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter7.Series.converges_of_nonneg_iff (@_fvar.92369 n)))))
(Exists.intro _fvar.59585 fun N =>
if h : N ≥ 0 then
Exists.casesOn (CanLift.prf N h) fun N_1 h_1 =>
Eq.ndrec (motive := fun N => N ≥ 0 → Chapter7.Series.partial (@_fvar.59781 n) N ≤ _fvar.59585)
(fun h => @_fvar.85054 n N_1) h_1 h
else
Eq.mpr
(id
(congrArg (fun _a => _a ≤ _fvar.59585)
(Chapter7.Series.partial_of_lt
(id
(lt_of_not_ge fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
(Eq.refl (Int.negOfNat 1)))))
Mathlib.Tactic.Ring.neg_zero))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf N)
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
(Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
(Mathlib.Tactic.Ring.add_pf_add_zero (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))
(Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
(Mathlib.Tactic.Ring.add_pf_add_zero
(Nat.rawCast 1 + (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
(Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_zero_add (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))
(Mathlib.Tactic.Ring.atom_pf N)
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul N (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt
(Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_zero_add
(N ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero N (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0)))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
(Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
(Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
(neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
(Mathlib.Tactic.Linarith.sub_nonpos_of_le (Int.add_one_le_iff.mpr (lt_of_not_ge h))))
(Mathlib.Tactic.Linarith.sub_nonpos_of_le a))))))))
_fvar.59915)hnon':{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.nonneg :=
fun n =>
Eq.mpr
(id
(Eq.trans
(congrArg (fun x => x ≥ 0)
(ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (Chapter7.Series.sum (@_fvar.59781 n.toNat))) fun a =>
Eq.refl 0))
ge_iff_le._simp_1))
(if h : 0 ≤ n then
Eq.mpr (id (congrArg (LE.le 0) (if_pos h))) (Chapter7.Series.sum_of_nonneg (@_fvar.92369 n.toNat))
else Eq.mpr (id (congrArg (LE.le 0) (if_neg h))) (of_eq_true (le_refl._simp_1 0)))hconv':{ m := 0, seq := fun n => if n ≥ 0 then (fun n => Chapter7.Series.sum (@_fvar.59781 n)) n.toNat else 0,
vanish := ⋯ }.converges :=
Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter7.Series.converges_of_nonneg_iff _fvar.132170))))
(Exists.intro _fvar.59585 _fvar.120948)ε:ℝhε:ε > 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 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:ℕ × ℕ → ℝ := _fvar.168246 ⊔ 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:ℕ × ℕ → ℝ := _fvar.168246 ⊔ 0fminus:ℕ × ℕ → ℝ := -_fvar.168246 ⊔ 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) f:ℕ × ℕ → ℝhf:AbsConvergent ffplus:ℕ × ℕ → ℝ := _fvar.168246 ⊔ 0fminus:ℕ × ℕ → ℝ := -_fvar.168246 ⊔ 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) f:ℕ × ℕ → ℝhf:AbsConvergent ffplus:ℕ × ℕ → ℝ := _fvar.168246 ⊔ 0fminus:ℕ × ℕ → ℝ := -_fvar.168246 ⊔ 0hfplus_nonneg:∀ (n m : ℕ), 0 ≤ @_fvar.168330 (n, m) := ?_mvar.168541n:ℕ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:ℕ × ℕ → ℝ := _fvar.168246 ⊔ 0fminus:ℕ × ℕ → ℝ := -_fvar.168246 ⊔ 0hfplus_nonneg:∀ (n m : ℕ), 0 ≤ @_fvar.168330 (n, m) := ?_mvar.168541hfminus_nonneg:∀ (n m : ℕ), 0 ≤ @_fvar.168422 (n, m) := ?_mvar.182542hdiff:_fvar.168246 = _fvar.168330 - _fvar.168422 := ?_mvar.196505hfplus_conv:Chapter8.AbsConvergent _fvar.168330 := ?_mvar.196519hfminus_conv:Chapter8.AbsConvergent _fvar.168422 := ?_mvar.196530hfplus_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:ℕ × ℕ → ℝ := _fvar.168246 ⊔ 0fminus:ℕ × ℕ → ℝ := -_fvar.168246 ⊔ 0hfplus_nonneg:∀ (n m : ℕ), 0 ≤ @_fvar.168330 (n, m) := ?_mvar.168541hfminus_nonneg:∀ (n m : ℕ), 0 ≤ @_fvar.168422 (n, m) := ?_mvar.182542hdiff:_fvar.168246 = _fvar.168330 - _fvar.168422 := ?_mvar.196505hfplus_conv:Chapter8.AbsConvergent _fvar.168330 := ?_mvar.196519hfminus_conv:Chapter8.AbsConvergent _fvar.168422 := ?_mvar.196530hfplus_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:ℕ × ℕ → ℝ := _fvar.168246 ⊔ 0fminus:ℕ × ℕ → ℝ := -_fvar.168246 ⊔ 0hfplus_nonneg:∀ (n m : ℕ), 0 ≤ @_fvar.168330 (n, m) := ?_mvar.168541hfminus_nonneg:∀ (n m : ℕ), 0 ≤ @_fvar.168422 (n, m) := ?_mvar.182542hdiff:_fvar.168246 = _fvar.168330 - _fvar.168422 := ?_mvar.196505hfplus_conv:Chapter8.AbsConvergent _fvar.168330 := ?_mvar.196519hfminus_conv:Chapter8.AbsConvergent _fvar.168422 := ?_mvar.196530hfplus_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:ℕ × ℕ → ℝ := _fvar.168246 ⊔ 0fminus:ℕ × ℕ → ℝ := -_fvar.168246 ⊔ 0hfplus_nonneg:∀ (n m : ℕ), 0 ≤ @_fvar.168330 (n, m) := ?_mvar.168541hfminus_nonneg:∀ (n m : ℕ), 0 ≤ @_fvar.168422 (n, m) := ?_mvar.182542hdiff:_fvar.168246 = _fvar.168330 - _fvar.168422 := ?_mvar.196505hfplus_conv:Chapter8.AbsConvergent _fvar.168330 := ?_mvar.196519hfminus_conv:Chapter8.AbsConvergent _fvar.168422 := ?_mvar.196530hfplus_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:ℕ × ℕ → ℝ := _fvar.168246 ⊔ 0fminus:ℕ × ℕ → ℝ := -_fvar.168246 ⊔ 0hfplus_nonneg:∀ (n m : ℕ), 0 ≤ @_fvar.168330 (n, m) := ?_mvar.168541hfminus_nonneg:∀ (n m : ℕ), 0 ≤ @_fvar.168422 (n, m) := ?_mvar.182542hdiff:_fvar.168246 = _fvar.168330 - _fvar.168422 := ?_mvar.196505hfplus_conv:Chapter8.AbsConvergent _fvar.168330 := ?_mvar.196519hfminus_conv:Chapter8.AbsConvergent _fvar.168422 := ?_mvar.196530hfplus_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:ℕ × ℕ → ℝ := _fvar.168246 ⊔ 0fminus:ℕ × ℕ → ℝ := -_fvar.168246 ⊔ 0hfplus_nonneg:∀ (n m : ℕ), 0 ≤ @_fvar.168330 (n, m) := ?_mvar.168541hfminus_nonneg:∀ (n m : ℕ), 0 ≤ @_fvar.168422 (n, m) := ?_mvar.182542hdiff:_fvar.168246 = _fvar.168330 - _fvar.168422 := ?_mvar.196505hfplus_conv:Chapter8.AbsConvergent _fvar.168330 := ?_mvar.196519hfminus_conv:Chapter8.AbsConvergent _fvar.168422 := ?_mvar.196530hfplus_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:ℕ × ℕ → ℝ := _fvar.168246 ⊔ 0fminus:ℕ × ℕ → ℝ := -_fvar.168246 ⊔ 0hfplus_nonneg:∀ (n m : ℕ), 0 ≤ @_fvar.168330 (n, m) := ?_mvar.168541hfminus_nonneg:∀ (n m : ℕ), 0 ≤ @_fvar.168422 (n, m) := ?_mvar.182542hdiff:_fvar.168246 = _fvar.168330 - _fvar.168422 := ?_mvar.196505hfplus_conv:Chapter8.AbsConvergent _fvar.168330 := ?_mvar.196519hfminus_conv:Chapter8.AbsConvergent _fvar.168422 := ?_mvar.196530hfplus_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:ℕ × ℕ → ℝ := _fvar.168246 ⊔ 0fminus:ℕ × ℕ → ℝ := -_fvar.168246 ⊔ 0hfplus_nonneg:∀ (n m : ℕ), 0 ≤ @_fvar.168330 (n, m) := ?_mvar.168541hfminus_nonneg:∀ (n m : ℕ), 0 ≤ @_fvar.168422 (n, m) := ?_mvar.182542hdiff:_fvar.168246 = _fvar.168330 - _fvar.168422 := ?_mvar.196505hfplus_conv:Chapter8.AbsConvergent _fvar.168330 := ?_mvar.196519hfminus_conv:Chapter8.AbsConvergent _fvar.168422 := ?_mvar.196530hfplus_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:ℕ × ℕ → ℝ := _fvar.168246 ⊔ 0fminus:ℕ × ℕ → ℝ := -_fvar.168246 ⊔ 0hfplus_nonneg:∀ (n m : ℕ), 0 ≤ @_fvar.168330 (n, m) := ?_mvar.168541hfminus_nonneg:∀ (n m : ℕ), 0 ≤ @_fvar.168422 (n, m) := ?_mvar.182542hdiff:_fvar.168246 = _fvar.168330 - _fvar.168422 := ?_mvar.196505hfplus_conv:Chapter8.AbsConvergent _fvar.168330 := ?_mvar.196519hfminus_conv:Chapter8.AbsConvergent _fvar.168422 := ?_mvar.196530hfplus_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:ℕ × ℕ → ℝ := _fvar.168246 ⊔ 0fminus:ℕ × ℕ → ℝ := -_fvar.168246 ⊔ 0hfplus_nonneg:∀ (n m : ℕ), 0 ≤ @_fvar.168330 (n, m) := ?_mvar.168541hfminus_nonneg:∀ (n m : ℕ), 0 ≤ @_fvar.168422 (n, m) := ?_mvar.182542hdiff:_fvar.168246 = _fvar.168330 - _fvar.168422 := ?_mvar.196505hfplus_conv:Chapter8.AbsConvergent _fvar.168330 := ?_mvar.196519hfminus_conv:Chapter8.AbsConvergent _fvar.168422 := ?_mvar.196530hfplus_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:ℕ × ℕ → ℝ := _fvar.168246 ⊔ 0fminus:ℕ × ℕ → ℝ := -_fvar.168246 ⊔ 0hfplus_nonneg:∀ (n m : ℕ), 0 ≤ @_fvar.168330 (n, m) := ?_mvar.168541hfminus_nonneg:∀ (n m : ℕ), 0 ≤ @_fvar.168422 (n, m) := ?_mvar.182542hdiff:_fvar.168246 = _fvar.168330 - _fvar.168422 := ?_mvar.196505hfplus_conv:Chapter8.AbsConvergent _fvar.168330 := ?_mvar.196519hfminus_conv:Chapter8.AbsConvergent _fvar.168422 := ?_mvar.196530hfplus_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 =>