Analysis
7.3. Sums of non-negative numbers

Imports

import Mathlib.Tactic
import Mathlib.Algebra.Field.Power
import Mathlib.NumberTheory.LSeries.RiemannZeta
import Mathlib.NumberTheory.LSeries.HurwitzZetaValues
import Analysis.Section_6_1
import Analysis.Section_6_epilogue
import Analysis.Section_7_2

Analysis I, Section 7.3: Sums of non-negative numbers

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:

Equivalent characterizations of convergence of nonnegative series.
Cauchy condensation test.

              namespace Chapter7open Realabbrev Series.nonneg (s: Series) : Prop := ∀ n, s.seq n ≥ 0abbrev declaration uses `sorry`Series.partial_of_nonneg {s: Series} (h: s.nonneg) : Monotone s.partial := bys:Seriesh:s.nonneg⊢ Monotone s.partial sorryAll goals completed! 🐙

Proposition 7.3.1

theorem Series.converges_of_nonneg_iff {s: Series} (h: s.nonneg) : s.converges ↔ ∃ M, ∀ N, s.partial N ≤ M := bys:Seriesh:s.nonneg⊢ s.converges ↔ ∃ M, ∀ (N : ℤ), s.partial N ≤ M
  -- This broadly follows the argument in the text, though for one direction I choose to use Mathlib routines rather than Chapter6 results.
  constructormps:Seriesh:s.nonneg⊢ s.converges → ∃ M, ∀ (N : ℤ), s.partial N ≤ Mmprs:Seriesh:s.nonneg⊢ (∃ M, ∀ (N : ℤ), s.partial N ≤ M) → s.converges
  .mps:Seriesh:s.nonneg⊢ s.converges → ∃ M, ∀ (N : ℤ), s.partial N ≤ M intro hconvmps:Seriesh:s.nonneghconv:s.converges⊢ ∃ M, ∀ (N : ℤ), s.partial N ≤ M
    set S : Chapter6.Sequence := ⟨ s.m, s.partial, bys:Seriesh:s.nonneghconv:s.converges⊢ ∀ n < s.m, s.partial n = 0 intro n hns:Seriesh:s.nonneghconv:s.convergesn:ℤhn:n < s.m⊢ s.partial n = 0; simp [Series.partial, hn]All goals completed! 🐙 ⟩
    have : S.IsBounded := bys:Seriesh:s.nonneg⊢ s.converges ↔ ∃ M, ∀ (N : ℤ), s.partial N ≤ M
      apply S.bounded_of_convergents:Seriesh:s.nonneghconv:s.convergesS:Chapter6.Sequence := { m := s.m, seq := s.partial, vanish := ⋯ }⊢ S.Convergent
      rw [Chapter6.Sequence.converges_iff_Tendsto']s:Seriesh:s.nonneghconv:s.convergesS:Chapter6.Sequence := { m := s.m, seq := s.partial, vanish := ⋯ }⊢ ∃ L, Filter.Tendsto S.seq Filter.atTop (nhds L)
      grindAll goals completed! 🐙
    choose M hpos hM using thismps:Seriesh:s.nonneghconv:s.convergesS:Chapter6.Sequence := { m := s.m, seq := s.partial, vanish := ⋯ }M:ℝhpos:M ≥ 0hM:S.BoundedBy M⊢ ∃ M, ∀ (N : ℤ), s.partial N ≤ M
    use Mhs:Seriesh:s.nonneghconv:s.convergesS:Chapter6.Sequence := { m := s.m, seq := s.partial, vanish := ⋯ }M:ℝhpos:M ≥ 0hM:S.BoundedBy M⊢ ∀ (N : ℤ), s.partial N ≤ M; peel hM with N hMh.hs:Seriesh:s.nonneghconv:s.convergesS:Chapter6.Sequence := { m := s.m, seq := s.partial, vanish := ⋯ }M:ℝhpos:M ≥ 0hM✝:S.BoundedBy MN:ℤhM:|S.seq N| ≤ M⊢ s.partial N ≤ M
    exact (le_abs_self _).trans hMAll goals completed! 🐙
  intro hboundmprs:Seriesh:s.nonneghbound:∃ M, ∀ (N : ℤ), s.partial N ≤ M⊢ s.converges
  obtain hinfin | hfin := tendsto_atTop_of_monotone (partial_of_nonneg h)mpr.inls:Seriesh:s.nonneghbound:∃ M, ∀ (N : ℤ), s.partial N ≤ Mhinfin:Filter.Tendsto s.partial Filter.atTop Filter.atTop⊢ s.convergesmpr.inrs:Seriesh:s.nonneghbound:∃ M, ∀ (N : ℤ), s.partial N ≤ Mhfin:∃ l, Filter.Tendsto s.partial Filter.atTop (nhds l)⊢ s.converges
  .mpr.inls:Seriesh:s.nonneghbound:∃ M, ∀ (N : ℤ), s.partial N ≤ Mhinfin:Filter.Tendsto s.partial Filter.atTop Filter.atTop⊢ s.converges choose M hM using hboundmpr.inls:Seriesh:s.nonneghinfin:Filter.Tendsto s.partial Filter.atTop Filter.atTopM:ℝhM:∀ (N : ℤ), s.partial N ≤ M⊢ s.converges
    choose N hN using (hinfin.eventually_gt_atTop M).existsmpr.inls:Seriesh:s.nonneghinfin:Filter.Tendsto s.partial Filter.atTop Filter.atTopM:ℝhM:∀ (N : ℤ), s.partial N ≤ MN:ℤhN:M < s.partial N⊢ s.converges
    grindAll goals completed! 🐙
  assumptionAll goals completed! 🐙

theorem Series.sum_of_nonneg_lt {s: Series} (h: s.nonneg) {M:ℝ} (hM: ∀ N, s.partial N ≤ M) : s.sum ≤ M := bys:Seriesh:s.nonnegM:ℝhM:∀ (N : ℤ), s.partial N ≤ M⊢ s.sum ≤ M
  have : ∃ M, ∀ N, s.partial N ≤ M  := bys:Seriesh:s.nonnegM:ℝhM:∀ (N : ℤ), s.partial N ≤ M⊢ s.sum ≤ M use MAll goals completed! 🐙
  rw [←converges_of_nonneg_iff h] at thiss:Seriesh:s.nonnegM:ℝhM:∀ (N : ℤ), s.partial N ≤ Mthis:s.converges⊢ s.sum ≤ M; simp [sum, this]s:Seriesh:s.nonnegM:ℝhM:∀ (N : ℤ), s.partial N ≤ Mthis:s.converges⊢ Exists.choose ⋯ ≤ M
  have hconv := this.choose_specs:Seriesh:s.nonnegM:ℝhM:∀ (N : ℤ), s.partial N ≤ Mthis:s.convergeshconv:s.convergesTo (Exists.choose this)⊢ Exists.choose ⋯ ≤ M; simp [convergesTo] at hconvs:Seriesh:s.nonnegM:ℝhM:∀ (N : ℤ), s.partial N ≤ Mthis:s.convergeshconv:Filter.Tendsto s.partial Filter.atTop (nhds (Exists.choose this))⊢ Exists.choose ⋯ ≤ M; exact le_of_tendsto' hconv hMAll goals completed! 🐙

theorem Series.partial_le_sum_of_nonneg {s: Series} (hnon: s.nonneg) (hconv: s.converges) (N : ℤ) :
  s.partial N ≤ s.sum := bys:Serieshnon:s.nonneghconv:s.convergesN:ℤ⊢ s.partial N ≤ s.sum
  apply (partial_of_nonneg hnon).ge_of_tendstohas:Serieshnon:s.nonneghconv:s.convergesN:ℤ⊢ Filter.Tendsto s.partial Filter.atTop (nhds s.sum)
  simp [sum, hconv]has:Serieshnon:s.nonneghconv:s.convergesN:ℤ⊢ Filter.Tendsto s.partial Filter.atTop (nhds (Exists.choose ⋯)); exact hconv.choose_specAll goals completed! 🐙

Some useful nonnegativity lemmas for later applications.

theorem Series.partial_nonneg {s: Series} (hnon: s.nonneg) (N : ℤ) : 0 ≤ s.partial N := bys:Serieshnon:s.nonnegN:ℤ⊢ 0 ≤ s.partial N
  simp [Series.partial]s:Serieshnon:s.nonnegN:ℤ⊢ 0 ≤ ∑ n ∈ Finset.Icc s.m N, s.seq n; apply Finset.sum_nonneghs:Serieshnon:s.nonnegN:ℤ⊢ ∀ i ∈ Finset.Icc s.m N, 0 ≤ s.seq i; aesopAll goals completed! 🐙

theorem Series.sum_of_nonneg {s:Series} (hnon: s.nonneg) : 0 ≤ s.sum := bys:Serieshnon:s.nonneg⊢ 0 ≤ s.sum
  by_cases h: s.convergesposs:Serieshnon:s.nonnegh:s.converges⊢ 0 ≤ s.sumnegs:Serieshnon:s.nonnegh:¬s.converges⊢ 0 ≤ s.sum <;>poss:Serieshnon:s.nonnegh:s.converges⊢ 0 ≤ s.sumnegs:Serieshnon:s.nonnegh:¬s.converges⊢ 0 ≤ s.sum simp [Series.sum, h]All goals completed! 🐙
  exact ge_of_tendsto' h.choose_spec (partial_nonneg hnon)All goals completed! 🐙

Corollary 7.3.2 (Comparison test) / Exercise 7.3.1

theorem declaration uses `sorry`Series.converges_of_le {s t: Series} (hm: s.m = t.m) (hcomp: ∀ n ≥ s.m, |s.seq n| ≤ t.seq n) (hconv : t.converges) : s.absConverges ∧ |s.sum| ≤ s.abs.sum ∧ s.abs.sum ≤ t.sum := bys:Seriest:Serieshm:s.m = t.mhcomp:∀ n ≥ s.m, |s.seq n| ≤ t.seq nhconv:t.converges⊢ s.absConverges ∧ |s.sum| ≤ s.abs.sum ∧ s.abs.sum ≤ t.sum sorryAll goals completed! 🐙

theorem declaration uses `sorry`Series.diverges_of_ge {s t: Series} (hm: s.m = t.m) (hcomp: ∀ n ≥ s.m, |s.seq n| ≤ t.seq n) (hdiv: ¬ s.absConverges) : t.diverges := bys:Seriest:Serieshm:s.m = t.mhcomp:∀ n ≥ s.m, |s.seq n| ≤ t.seq nhdiv:¬s.absConverges⊢ t.diverges sorryAll goals completed! 🐙

Lemma 7.3.3 (Geometric series) / Exercise 7.3.2

theorem declaration uses `sorry`Series.converges_geom {x: ℝ} (hx: |x| < 1) : (fun n ↦ x ^ n : Series).convergesTo (1 / (1 - x)) := byx:ℝhx:|x| < 1⊢ { m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ x ^ n) n.toNat else 0, vanish := ⋯ }.convergesTo (1 / (1 - x)) sorryAll goals completed! 🐙

              theorem declaration uses `sorry`Series.absConverges_geom {x: ℝ} (hx: |x| < 1) : (fun n ↦ x ^ n : Series).absConverges := byx:ℝhx:|x| < 1⊢ { m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ x ^ n) n.toNat else 0, vanish := ⋯ }.absConverges sorryAll goals completed! 🐙theorem declaration uses `sorry`Series.diverges_geom {x: ℝ} (hx: |x| ≥ 1) : (fun n ↦ x ^ n : Series).diverges := byx:ℝhx:|x| ≥ 1⊢ { m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ x ^ n) n.toNat else 0, vanish := ⋯ }.diverges sorryAll goals completed! 🐙theorem declaration uses `sorry`Series.converges_geom_iff (x: ℝ) : (fun n ↦ x ^ n : Series).converges ↔ |x| < 1 := byx:ℝ⊢ { m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ x ^ n) n.toNat else 0, vanish := ⋯ }.converges ↔ |x| < 1 sorryAll goals completed! 🐙

Proposition 7.3.4 (Cauchy criterion)

theorem Series.cauchy_criterion {s:Series} (hm: s.m = 1) (hs:s.nonneg) (hmono: ∀ n ≥ 1, s.seq (n+1) ≤ s.seq n) : s.converges ↔ (fun k ↦ 2^k * s.seq (2^k): Series).converges := bys:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq n⊢ s.converges ↔
  { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }.converges
  -- This proof is written to follow the structure of the original text.
  set t := (fun k ↦ 2^k * s.seq (2^k):Series)s:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }⊢ s.converges ↔ t.converges
  have ht: t.nonneg := bys:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq n⊢ s.converges ↔
  { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }.converges intro ns:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }n:ℤ⊢ t.seq n ≥ 0; by_cases h: n ≥ 0poss:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }n:ℤh:n ≥ 0⊢ t.seq n ≥ 0negs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }n:ℤh:¬n ≥ 0⊢ t.seq n ≥ 0 <;>poss:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }n:ℤh:n ≥ 0⊢ t.seq n ≥ 0negs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }n:ℤh:¬n ≥ 0⊢ t.seq n ≥ 0 simp [t,h]All goals completed! 🐙; grindAll goals completed! 🐙
  have hmono' : ∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq n := bys:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq n⊢ s.converges ↔
  { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }.converges
    intro n hns:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonnegn:ℤhn:n ≥ 1⊢ ∀ m ≥ n, s.seq m ≤ s.seq n ms:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonnegn:ℤhn:n ≥ 1m:ℤ⊢ m ≥ n → s.seq m ≤ s.seq n hms:Serieshm✝:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonnegn:ℤhn:n ≥ 1m:ℤhm:m ≥ n⊢ s.seq m ≤ s.seq n; obtain ⟨ k, rfl ⟩ := Int.le.dest hms:Serieshm✝:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonnegn:ℤhn:n ≥ 1k:ℕhm:n + ↑k ≥ n⊢ s.seq (n + ↑k) ≤ s.seq n; clear hms:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonnegn:ℤhn:n ≥ 1k:ℕ⊢ s.seq (n + ↑k) ≤ s.seq n
    induction' k with k hkzeros:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonnegn:ℤhn:n ≥ 1⊢ s.seq (n + ↑0) ≤ s.seq nsuccs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonnegn:ℤhn:n ≥ 1k:ℕhk:s.seq (n + ↑k) ≤ s.seq n⊢ s.seq (n + ↑(k + 1)) ≤ s.seq n; simpsuccs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonnegn:ℤhn:n ≥ 1k:ℕhk:s.seq (n + ↑k) ≤ s.seq n⊢ s.seq (n + ↑(k + 1)) ≤ s.seq n
    convert (hmono (n+k) (bys:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonnegn:ℤhn:n ≥ 1k:ℕhk:s.seq (n + ↑k) ≤ s.seq n⊢ n + ↑k ≥ 1 grindAll goals completed! 🐙)).trans hk using 2; grindAll goals completed! 🐙
  have htm : t.m = 0 := bys:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq n⊢ s.converges ↔
  { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }.converges simp [t]All goals completed! 🐙
  rw [converges_of_nonneg_iff hs, converges_of_nonneg_iff ht]s:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0⊢ (∃ M, ∀ (N : ℤ), s.partial N ≤ M) ↔ ∃ M, ∀ (N : ℤ), t.partial N ≤ M
  set S := s.partials:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partial⊢ (∃ M, ∀ (N : ℤ), S N ≤ M) ↔ ∃ M, ∀ (N : ℤ), t.partial N ≤ M
  set T := t.partials:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partial⊢ (∃ M, ∀ (N : ℤ), S N ≤ M) ↔ ∃ M, ∀ (N : ℤ), T N ≤ M
  have Lemma_7_3_6 (K:ℕ) : S (2^(K+1) - 1) ≤ T K ∧ T K ≤ 2 * S (2^K) := bys:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq n⊢ s.converges ↔
  { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }.converges
    induction' K with K hKzeros:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partial⊢ S (2 ^ (0 + 1) - 1) ≤ T ↑0 ∧ T ↑0 ≤ 2 * S (2 ^ 0)succs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕhK:S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)⊢ S (2 ^ (K + 1 + 1) - 1) ≤ T ↑(K + 1) ∧ T ↑(K + 1) ≤ 2 * S (2 ^ (K + 1))
    .zeros:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partial⊢ S (2 ^ (0 + 1) - 1) ≤ T ↑0 ∧ T ↑0 ≤ 2 * S (2 ^ 0) simp [S,T,Series.partial, hm, t]zeros:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partial⊢ s.seq 1 ≤ 2 * s.seq 1; grindAll goals completed! 🐙
    observe h2K : 1 ≤ 2^Ksuccs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕhK:S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)h2K:1 ≤ 2 ^ K⊢ S (2 ^ (K + 1 + 1) - 1) ≤ T ↑(K + 1) ∧ T ↑(K + 1) ≤ 2 * S (2 ^ (K + 1)); observe h2K' : 1 ≤ 2^(K+1)succs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕhK:S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)h2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)⊢ S (2 ^ (K + 1 + 1) - 1) ≤ T ↑(K + 1) ∧ T ↑(K + 1) ≤ 2 * S (2 ^ (K + 1))
    choose hK1 hK2 using hKsuccs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)⊢ S (2 ^ (K + 1 + 1) - 1) ≤ T ↑(K + 1) ∧ T ↑(K + 1) ≤ 2 * S (2 ^ (K + 1))
    have claim1 : T (K + 1) = T K + 2^(K+1) * s.seq (2^(K+1)) := bys:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq n⊢ s.converges ↔
  { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }.converges apply t.partial_succs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)⊢ ↑K ≥ t.m - 1; grindAll goals completed! 🐙
    have claim2a : S (2^(K+1)) ≥ S (2^K) + 2^K * s.seq (2^(K+1)) := calc
      _ = S (2^K) + ∑ n ∈ .Ioc (2^K) (2^(K+1)), s.seq n := bys:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))⊢ S (2 ^ (K + 1)) = S (2 ^ K) + ∑ n ∈ Finset.Ioc (2 ^ K) (2 ^ (K + 1)), s.seq n
        have : Disjoint (Finset.Icc s.m (2^K)) (Finset.Ioc (2^K) (2^(K+1))) := bys:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))⊢ S (2 ^ (K + 1)) = S (2 ^ K) + ∑ n ∈ Finset.Ioc (2 ^ K) (2 ^ (K + 1)), s.seq n
          rw [Finset.disjoint_iff_ne]s:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))⊢ ∀ a ∈ Finset.Icc s.m (2 ^ K), ∀ b ∈ Finset.Ioc (2 ^ K) (2 ^ (K + 1)), a ≠ b; intro x hxs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))x:ℤhx:x ∈ Finset.Icc s.m (2 ^ K)⊢ ∀ b ∈ Finset.Ioc (2 ^ K) (2 ^ (K + 1)), x ≠ b ys:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))x:ℤhx:x ∈ Finset.Icc s.m (2 ^ K)y:ℤ⊢ y ∈ Finset.Ioc (2 ^ K) (2 ^ (K + 1)) → x ≠ y hys:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))x:ℤhx:x ∈ Finset.Icc s.m (2 ^ K)y:ℤhy:y ∈ Finset.Ioc (2 ^ K) (2 ^ (K + 1))⊢ x ≠ y; simp at hx hys:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))x:ℤy:ℤhx:s.m ≤ x ∧ x ≤ 2 ^ Khy:2 ^ K < y ∧ y ≤ 2 ^ (K + 1)⊢ x ≠ y; linarithAll goals completed! 🐙
        convert Finset.sum_union thish.e'_2.hs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))this:Disjoint (Finset.Icc s.m (2 ^ K)) (Finset.Ioc (2 ^ K) (2 ^ (K + 1)))⊢ Finset.Icc s.m (2 ^ (K + 1)) = Finset.Icc s.m (2 ^ K) ∪ Finset.Ioc (2 ^ K) (2 ^ (K + 1))
        ext xh.e'_2.h.hs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))this:Disjoint (Finset.Icc s.m (2 ^ K)) (Finset.Ioc (2 ^ K) (2 ^ (K + 1)))x:ℤ⊢ x ∈ Finset.Icc s.m (2 ^ (K + 1)) ↔ x ∈ Finset.Icc s.m (2 ^ K) ∪ Finset.Ioc (2 ^ K) (2 ^ (K + 1)); simph.e'_2.h.hs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))this:Disjoint (Finset.Icc s.m (2 ^ K)) (Finset.Ioc (2 ^ K) (2 ^ (K + 1)))x:ℤ⊢ s.m ≤ x ∧ x ≤ 2 ^ (K + 1) ↔ s.m ≤ x ∧ x ≤ 2 ^ K ∨ 2 ^ K < x ∧ x ≤ 2 ^ (K + 1); constructorh.e'_2.h.h.mps:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))this:Disjoint (Finset.Icc s.m (2 ^ K)) (Finset.Ioc (2 ^ K) (2 ^ (K + 1)))x:ℤ⊢ s.m ≤ x ∧ x ≤ 2 ^ (K + 1) → s.m ≤ x ∧ x ≤ 2 ^ K ∨ 2 ^ K < x ∧ x ≤ 2 ^ (K + 1)h.e'_2.h.h.mprs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))this:Disjoint (Finset.Icc s.m (2 ^ K)) (Finset.Ioc (2 ^ K) (2 ^ (K + 1)))x:ℤ⊢ s.m ≤ x ∧ x ≤ 2 ^ K ∨ 2 ^ K < x ∧ x ≤ 2 ^ (K + 1) → s.m ≤ x ∧ x ≤ 2 ^ (K + 1)
        .h.e'_2.h.h.mps:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))this:Disjoint (Finset.Icc s.m (2 ^ K)) (Finset.Ioc (2 ^ K) (2 ^ (K + 1)))x:ℤ⊢ s.m ≤ x ∧ x ≤ 2 ^ (K + 1) → s.m ≤ x ∧ x ≤ 2 ^ K ∨ 2 ^ K < x ∧ x ≤ 2 ^ (K + 1) intro ⟨h1, h2⟩h.e'_2.h.h.mps:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))this:Disjoint (Finset.Icc s.m (2 ^ K)) (Finset.Ioc (2 ^ K) (2 ^ (K + 1)))x:ℤh1:s.m ≤ xh2:x ≤ 2 ^ (K + 1)⊢ s.m ≤ x ∧ x ≤ 2 ^ K ∨ 2 ^ K < x ∧ x ≤ 2 ^ (K + 1); simp [h1, h2, le_or_gt]All goals completed! 🐙
        rintro (⟨ h1, h2 ⟩ | ⟨ h1, h2 ⟩)h.e'_2.h.h.mpr.inls:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))this:Disjoint (Finset.Icc s.m (2 ^ K)) (Finset.Ioc (2 ^ K) (2 ^ (K + 1)))x:ℤh1:s.m ≤ xh2:x ≤ 2 ^ K⊢ s.m ≤ x ∧ x ≤ 2 ^ (K + 1)h.e'_2.h.h.mpr.inrs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))this:Disjoint (Finset.Icc s.m (2 ^ K)) (Finset.Ioc (2 ^ K) (2 ^ (K + 1)))x:ℤh1:2 ^ K < xh2:x ≤ 2 ^ (K + 1)⊢ s.m ≤ x ∧ x ≤ 2 ^ (K + 1)
        .h.e'_2.h.h.mpr.inls:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))this:Disjoint (Finset.Icc s.m (2 ^ K)) (Finset.Ioc (2 ^ K) (2 ^ (K + 1)))x:ℤh1:s.m ≤ xh2:x ≤ 2 ^ K⊢ s.m ≤ x ∧ x ≤ 2 ^ (K + 1) simp [h1,pow_succ']h.e'_2.h.h.mpr.inls:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))this:Disjoint (Finset.Icc s.m (2 ^ K)) (Finset.Ioc (2 ^ K) (2 ^ (K + 1)))x:ℤh1:s.m ≤ xh2:x ≤ 2 ^ K⊢ x ≤ 2 * 2 ^ K; linarithAll goals completed! 🐙
        simp [h2, hm]h.e'_2.h.h.mpr.inrs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))this:Disjoint (Finset.Icc s.m (2 ^ K)) (Finset.Ioc (2 ^ K) (2 ^ (K + 1)))x:ℤh1:2 ^ K < xh2:x ≤ 2 ^ (K + 1)⊢ 1 ≤ x; grindAll goals completed! 🐙
      _ ≥ S (2^K) + ∑ n ∈ .Ioc ((2:ℤ)^K) (2^(K+1)), s.seq (2^(K+1)) := bys:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))⊢ S (2 ^ K) + ∑ n ∈ Finset.Ioc (2 ^ K) (2 ^ (K + 1)), s.seq n ≥
  S (2 ^ K) + ∑ n ∈ Finset.Ioc (2 ^ K) (2 ^ (K + 1)), s.seq (2 ^ (K + 1))
        gcongr with n hnbc.hs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))n:ℤhn:n ∈ Finset.Ioc (2 ^ K) (2 ^ (K + 1))⊢ s.seq (2 ^ (K + 1)) ≤ s.seq n; simp at hnbc.hs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))n:ℤhn:2 ^ K < n ∧ n ≤ 2 ^ (K + 1)⊢ s.seq (2 ^ (K + 1)) ≤ s.seq n; exact hmono' _ (bys:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))n:ℤhn:2 ^ K < n ∧ n ≤ 2 ^ (K + 1)⊢ n ≥ 1 grindAll goals completed! 🐙) _ hn.2
      _ = _ := bys:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))⊢ S (2 ^ K) + ∑ n ∈ Finset.Ioc (2 ^ K) (2 ^ (K + 1)), s.seq (2 ^ (K + 1)) = S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1)) simp [pow_succ']s:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))⊢ ↑(2 * 2 ^ K - 2 ^ K).toNat = 2 ^ K ∨ s.seq (2 * 2 ^ K) = 0; lefths:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))⊢ ↑(2 * 2 ^ K - 2 ^ K).toNat = 2 ^ K; ring_nfhs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))⊢ ↑(2 ^ K).toNat = 2 ^ K; norm_castAll goals completed! 🐙
    have claim2 : 2 * S (2^(K+1)) ≥ 2 * S (2^K) + 2^(K+1) * s.seq (2^(K+1)) := bys:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq n⊢ s.converges ↔
  { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }.converges
      nth_rewrite 2 [pow_succ']s:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))⊢ 2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 * 2 ^ K * s.seq (2 ^ (K + 1)); grindAll goals completed! 🐙
    have claim3 : S (2^(K+1+1) - 1) ≤ S (2^(K+1)-1) + 2^(K+1) * s.seq (2^(K+1)) := calc
      _ = S (2^(K+1)-1) + ∑ n ∈ .Icc (2^(K+1)) (2^(K+1+1)-1), s.seq n := bys:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))⊢ S (2 ^ (K + 1 + 1) - 1) = S (2 ^ (K + 1) - 1) + ∑ n ∈ Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1), s.seq n
        have : Disjoint (Finset.Icc s.m (2^(K+1)-1)) (Finset.Icc (2^(K+1)) (2^(K+1+1)-1)) := bys:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))⊢ S (2 ^ (K + 1 + 1) - 1) = S (2 ^ (K + 1) - 1) + ∑ n ∈ Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1), s.seq n
          rw [Finset.disjoint_iff_ne]s:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))⊢ ∀ a ∈ Finset.Icc s.m (2 ^ (K + 1) - 1), ∀ b ∈ Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1), a ≠ b; intro x hxs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))x:ℤhx:x ∈ Finset.Icc s.m (2 ^ (K + 1) - 1)⊢ ∀ b ∈ Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1), x ≠ b ys:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))x:ℤhx:x ∈ Finset.Icc s.m (2 ^ (K + 1) - 1)y:ℤ⊢ y ∈ Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1) → x ≠ y hys:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))x:ℤhx:x ∈ Finset.Icc s.m (2 ^ (K + 1) - 1)y:ℤhy:y ∈ Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1)⊢ x ≠ y; simp at hx hys:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))x:ℤy:ℤhx:s.m ≤ x ∧ x < 2 ^ (K + 1)hy:2 ^ (K + 1) ≤ y ∧ y < 2 ^ (K + 1 + 1)⊢ x ≠ y; linarithAll goals completed! 🐙
        convert Finset.sum_union thish.e'_2.hs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))this:Disjoint (Finset.Icc s.m (2 ^ (K + 1) - 1)) (Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1))⊢ Finset.Icc s.m (2 ^ (K + 1 + 1) - 1) = Finset.Icc s.m (2 ^ (K + 1) - 1) ∪ Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1)
        exth.e'_2.h.hs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))this:Disjoint (Finset.Icc s.m (2 ^ (K + 1) - 1)) (Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1))a✝:ℤ⊢ a✝ ∈ Finset.Icc s.m (2 ^ (K + 1 + 1) - 1) ↔
  a✝ ∈ Finset.Icc s.m (2 ^ (K + 1) - 1) ∪ Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1); simph.e'_2.h.hs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))this:Disjoint (Finset.Icc s.m (2 ^ (K + 1) - 1)) (Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1))a✝:ℤ⊢ s.m ≤ a✝ ∧ a✝ < 2 ^ (K + 1 + 1) ↔ s.m ≤ a✝ ∧ a✝ < 2 ^ (K + 1) ∨ 2 ^ (K + 1) ≤ a✝ ∧ a✝ < 2 ^ (K + 1 + 1); constructorh.e'_2.h.h.mps:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))this:Disjoint (Finset.Icc s.m (2 ^ (K + 1) - 1)) (Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1))a✝:ℤ⊢ s.m ≤ a✝ ∧ a✝ < 2 ^ (K + 1 + 1) → s.m ≤ a✝ ∧ a✝ < 2 ^ (K + 1) ∨ 2 ^ (K + 1) ≤ a✝ ∧ a✝ < 2 ^ (K + 1 + 1)h.e'_2.h.h.mprs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))this:Disjoint (Finset.Icc s.m (2 ^ (K + 1) - 1)) (Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1))a✝:ℤ⊢ s.m ≤ a✝ ∧ a✝ < 2 ^ (K + 1) ∨ 2 ^ (K + 1) ≤ a✝ ∧ a✝ < 2 ^ (K + 1 + 1) → s.m ≤ a✝ ∧ a✝ < 2 ^ (K + 1 + 1)
        .h.e'_2.h.h.mps:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))this:Disjoint (Finset.Icc s.m (2 ^ (K + 1) - 1)) (Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1))a✝:ℤ⊢ s.m ≤ a✝ ∧ a✝ < 2 ^ (K + 1 + 1) → s.m ≤ a✝ ∧ a✝ < 2 ^ (K + 1) ∨ 2 ^ (K + 1) ≤ a✝ ∧ a✝ < 2 ^ (K + 1 + 1) intro ⟨h1, h2⟩h.e'_2.h.h.mps:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))this:Disjoint (Finset.Icc s.m (2 ^ (K + 1) - 1)) (Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1))a✝:ℤh1:s.m ≤ a✝h2:a✝ < 2 ^ (K + 1 + 1)⊢ s.m ≤ a✝ ∧ a✝ < 2 ^ (K + 1) ∨ 2 ^ (K + 1) ≤ a✝ ∧ a✝ < 2 ^ (K + 1 + 1); simp [h1, h2]h.e'_2.h.h.mps:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))this:Disjoint (Finset.Icc s.m (2 ^ (K + 1) - 1)) (Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1))a✝:ℤh1:s.m ≤ a✝h2:a✝ < 2 ^ (K + 1 + 1)⊢ a✝ < 2 ^ (K + 1) ∨ 2 ^ (K + 1) ≤ a✝; omegaAll goals completed! 🐙
        rintro (⟨ h1, h2 ⟩ | ⟨ h1, h2 ⟩)h.e'_2.h.h.mpr.inls:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))this:Disjoint (Finset.Icc s.m (2 ^ (K + 1) - 1)) (Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1))a✝:ℤh1:s.m ≤ a✝h2:a✝ < 2 ^ (K + 1)⊢ s.m ≤ a✝ ∧ a✝ < 2 ^ (K + 1 + 1)h.e'_2.h.h.mpr.inrs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))this:Disjoint (Finset.Icc s.m (2 ^ (K + 1) - 1)) (Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1))a✝:ℤh1:2 ^ (K + 1) ≤ a✝h2:a✝ < 2 ^ (K + 1 + 1)⊢ s.m ≤ a✝ ∧ a✝ < 2 ^ (K + 1 + 1)
        .h.e'_2.h.h.mpr.inls:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))this:Disjoint (Finset.Icc s.m (2 ^ (K + 1) - 1)) (Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1))a✝:ℤh1:s.m ≤ a✝h2:a✝ < 2 ^ (K + 1)⊢ s.m ≤ a✝ ∧ a✝ < 2 ^ (K + 1 + 1) simp [h1, pow_succ' _ (K+1)]h.e'_2.h.h.mpr.inls:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))this:Disjoint (Finset.Icc s.m (2 ^ (K + 1) - 1)) (Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1))a✝:ℤh1:s.m ≤ a✝h2:a✝ < 2 ^ (K + 1)⊢ a✝ < 2 * 2 ^ (K + 1); linarithAll goals completed! 🐙
        simp [h2, hm]h.e'_2.h.h.mpr.inrs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))this:Disjoint (Finset.Icc s.m (2 ^ (K + 1) - 1)) (Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1))a✝:ℤh1:2 ^ (K + 1) ≤ a✝h2:a✝ < 2 ^ (K + 1 + 1)⊢ 1 ≤ a✝; linarithAll goals completed! 🐙
      _ ≤ S (2^(K+1)-1) + ∑ n ∈ .Icc ((2:ℤ)^(K+1)) (2^(K+1+1)-1), s.seq (2^(K+1)) := bys:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))⊢ S (2 ^ (K + 1) - 1) + ∑ n ∈ Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1), s.seq n ≤
  S (2 ^ (K + 1) - 1) + ∑ n ∈ Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1), s.seq (2 ^ (K + 1))
        gcongr with n hnbc.hs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))n:ℤhn:n ∈ Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1)⊢ s.seq n ≤ s.seq (2 ^ (K + 1)); simp at hnbc.hs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))n:ℤhn:2 ^ (K + 1) ≤ n ∧ n < 2 ^ (K + 1 + 1)⊢ s.seq n ≤ s.seq (2 ^ (K + 1)); apply hmono' _ _ _ hn.1s:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))n:ℤhn:2 ^ (K + 1) ≤ n ∧ n < 2 ^ (K + 1 + 1)⊢ 2 ^ (K + 1) ≥ 1; linarithAll goals completed! 🐙
      _ = _ := bys:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))⊢ S (2 ^ (K + 1) - 1) + ∑ n ∈ Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1), s.seq (2 ^ (K + 1)) =
  S (2 ^ (K + 1) - 1) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1)) simp [pow_succ']s:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))⊢ ↑(2 * (2 * 2 ^ K) - 2 * 2 ^ K).toNat = 2 * 2 ^ K ∨ s.seq (2 * 2 ^ K) = 0; lefths:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))⊢ ↑(2 * (2 * 2 ^ K) - 2 * 2 ^ K).toNat = 2 * 2 ^ K; ring_nfhs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))⊢ ↑(2 ^ K * 2).toNat = 2 ^ K * 2; norm_castAll goals completed! 🐙
    simpsuccs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim3:S (2 ^ (K + 1 + 1) - 1) ≤ S (2 ^ (K + 1) - 1) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))⊢ S (2 ^ (K + 1 + 1) - 1) ≤ T (↑K + 1) ∧ T (↑K + 1) ≤ 2 * S (2 ^ (K + 1)); constructorsucc.lefts:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim3:S (2 ^ (K + 1 + 1) - 1) ≤ S (2 ^ (K + 1) - 1) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))⊢ S (2 ^ (K + 1 + 1) - 1) ≤ T (↑K + 1)succ.rights:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim3:S (2 ^ (K + 1 + 1) - 1) ≤ S (2 ^ (K + 1) - 1) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))⊢ T (↑K + 1) ≤ 2 * S (2 ^ (K + 1)) <;>succ.lefts:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim3:S (2 ^ (K + 1 + 1) - 1) ≤ S (2 ^ (K + 1) - 1) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))⊢ S (2 ^ (K + 1 + 1) - 1) ≤ T (↑K + 1)succ.rights:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialK:ℕh2K:1 ≤ 2 ^ Kh2K':1 ≤ 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) ≤ T ↑KhK2:T ↑K ≤ 2 * S (2 ^ K)claim1:T (↑K + 1) = T ↑K + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim2a:S (2 ^ (K + 1)) ≥ S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1))claim2:2 * S (2 ^ (K + 1)) ≥ 2 * S (2 ^ K) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))claim3:S (2 ^ (K + 1 + 1) - 1) ≤ S (2 ^ (K + 1) - 1) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1))⊢ T (↑K + 1) ≤ 2 * S (2 ^ (K + 1)) grindAll goals completed! 🐙
  constructormps:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)⊢ (∃ M, ∀ (N : ℤ), S N ≤ M) → ∃ M, ∀ (N : ℤ), T N ≤ Mmprs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)⊢ (∃ M, ∀ (N : ℤ), T N ≤ M) → ∃ M, ∀ (N : ℤ), S N ≤ M
  .mps:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)⊢ (∃ M, ∀ (N : ℤ), S N ≤ M) → ∃ M, ∀ (N : ℤ), T N ≤ M intro ⟨ M, hM ⟩mps:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)M:ℝhM:∀ (N : ℤ), S N ≤ M⊢ ∃ M, ∀ (N : ℤ), T N ≤ M; use 2*Mhs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)M:ℝhM:∀ (N : ℤ), S N ≤ M⊢ ∀ (N : ℤ), T N ≤ 2 * M; intro Nhs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)M:ℝhM:∀ (N : ℤ), S N ≤ MN:ℤ⊢ T N ≤ 2 * M; obtain hN | hN := lt_or_ge N 0h.inls:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)M:ℝhM:∀ (N : ℤ), S N ≤ MN:ℤhN:N < 0⊢ T N ≤ 2 * Mh.inrs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)M:ℝhM:∀ (N : ℤ), S N ≤ MN:ℤhN:0 ≤ N⊢ T N ≤ 2 * M
    .h.inls:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)M:ℝhM:∀ (N : ℤ), S N ≤ MN:ℤhN:N < 0⊢ T N ≤ 2 * M simp [T, Series.partial, htm, hN]h.inls:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)M:ℝhM:∀ (N : ℤ), S N ≤ MN:ℤhN:N < 0⊢ 0 ≤ M; convert hM 0h.e'_3s:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)M:ℝhM:∀ (N : ℤ), S N ≤ MN:ℤhN:N < 0⊢ 0 = S 0; simp [S, Series.partial, hm]All goals completed! 🐙
    rw [Int.eq_natCast_toNat.mpr hN]h.inrs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)M:ℝhM:∀ (N : ℤ), S N ≤ MN:ℤhN:0 ≤ N⊢ T ↑N.toNat ≤ 2 * M; apply (Lemma_7_3_6 N.toNat).2.transh.inrs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)M:ℝhM:∀ (N : ℤ), S N ≤ MN:ℤhN:0 ≤ N⊢ 2 * S (2 ^ N.toNat) ≤ 2 * M; grindAll goals completed! 🐙
  intro ⟨ M, hM ⟩mprs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)M:ℝhM:∀ (N : ℤ), T N ≤ M⊢ ∃ M, ∀ (N : ℤ), S N ≤ M; use Mhs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)M:ℝhM:∀ (N : ℤ), T N ≤ M⊢ ∀ (N : ℤ), S N ≤ M; intro K'hs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)M:ℝhM:∀ (N : ℤ), T N ≤ MK':ℤ⊢ S K' ≤ M; obtain hK' | hK' := lt_or_ge K' 1h.inls:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)M:ℝhM:∀ (N : ℤ), T N ≤ MK':ℤhK':K' < 1⊢ S K' ≤ Mh.inrs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)M:ℝhM:∀ (N : ℤ), T N ≤ MK':ℤhK':1 ≤ K'⊢ S K' ≤ M
  .h.inls:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)M:ℝhM:∀ (N : ℤ), T N ≤ MK':ℤhK':K' < 1⊢ S K' ≤ M simp [S, Series.partial, hm, hK']h.inls:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)M:ℝhM:∀ (N : ℤ), T N ≤ MK':ℤhK':K' < 1⊢ 0 ≤ M; convert hM (-1)All goals completed! 🐙
  set K := (K'-1).toNath.inrs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)M:ℝhM:∀ (N : ℤ), T N ≤ MK':ℤhK':1 ≤ K'K:ℕ := (K' - 1).toNat⊢ S K' ≤ M; have hK : K' = K + 1 := bys:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq n⊢ s.converges ↔
  { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }.converges rw [Int.toNat_of_nonneg (by linarith)]s:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)M:ℝhM:∀ (N : ℤ), T N ≤ MK':ℤhK':1 ≤ K'K:ℕ := (K' - 1).toNat⊢ K' = K' - 1 + 1; abelAll goals completed! 🐙
  calc
    _ ≤ S (2 ^ (K+1) - 1) := bys:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)M:ℝhM:∀ (N : ℤ), T N ≤ MK':ℤhK':1 ≤ K'K:ℕ := (K' - 1).toNathK:K' = ↑K + 1⊢ S K' ≤ S (2 ^ (K + 1) - 1)
      apply partial_of_nonneg hsas:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)M:ℝhM:∀ (N : ℤ), T N ≤ MK':ℤhK':1 ≤ K'K:ℕ := (K' - 1).toNathK:K' = ↑K + 1⊢ K' ≤ 2 ^ (K + 1) - 1; rw [hK]as:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)M:ℝhM:∀ (N : ℤ), T N ≤ MK':ℤhK':1 ≤ K'K:ℕ := (K' - 1).toNathK:K' = ↑K + 1⊢ ↑K + 1 ≤ 2 ^ (K + 1) - 1
      generalize K = nas:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)M:ℝhM:∀ (N : ℤ), T N ≤ MK':ℤhK':1 ≤ K'K:ℕ := (K' - 1).toNathK:K' = ↑K + 1n:ℕ⊢ ↑n + 1 ≤ 2 ^ (n + 1) - 1; induction' n with n hna.zeros:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)M:ℝhM:∀ (N : ℤ), T N ≤ MK':ℤhK':1 ≤ K'K:ℕ := (K' - 1).toNathK:K' = ↑K + 1⊢ ↑0 + 1 ≤ 2 ^ (0 + 1) - 1a.succs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)M:ℝhM:∀ (N : ℤ), T N ≤ MK':ℤhK':1 ≤ K'K:ℕ := (K' - 1).toNathK:K' = ↑K + 1n:ℕhn:↑n + 1 ≤ 2 ^ (n + 1) - 1⊢ ↑(n + 1) + 1 ≤ 2 ^ (n + 1 + 1) - 1; simpa.succs:Serieshm:s.m = 1hs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghmono':∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq nhtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialLemma_7_3_6:∀ (K : ℕ), S (2 ^ (K + 1) - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)M:ℝhM:∀ (N : ℤ), T N ≤ MK':ℤhK':1 ≤ K'K:ℕ := (K' - 1).toNathK:K' = ↑K + 1n:ℕhn:↑n + 1 ≤ 2 ^ (n + 1) - 1⊢ ↑(n + 1) + 1 ≤ 2 ^ (n + 1 + 1) - 1
      simp [pow_succ] at *a.succs:Serieshm:s.m = 1hs:s.nonnegt:Series := { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }ht:t.nonneghtm:t.m = 0S:ℤ → ℝ := s.partialT:ℤ → ℝ := t.partialM:ℝhM:∀ (N : ℤ), T N ≤ MK':ℤhK':1 ≤ K'K:ℕ := (K' - 1).toNathK:K' = ↑K + 1n:ℕhmono:∀ (n : ℤ), 1 ≤ n → s.seq (n + 1) ≤ s.seq nhmono':∀ (n : ℤ), 1 ≤ n → ∀ (m : ℤ), n ≤ m → s.seq m ≤ s.seq nLemma_7_3_6:∀ (K : ℕ), S (2 ^ K * 2 - 1) ≤ T ↑K ∧ T ↑K ≤ 2 * S (2 ^ K)hn:↑n + 1 < 2 ^ n * 2⊢ ↑n + 1 + 1 < 2 ^ n * 2 * 2; linarithAll goals completed! 🐙
    _ ≤ T K := (Lemma_7_3_6 K).1
    _ ≤ M := hM K

Corollary 7.3.7

theorem Series.converges_qseries (q: ℝ) (hq: q > 0) : (mk' (m := 1) fun n ↦ 1 / (n:ℝ) ^ q : Series).converges ↔ (q>1) := byq:ℝhq:q > 0⊢ (mk' fun n ↦ 1 / ↑↑n ^ q).converges ↔ q > 1
  -- This proof is written to follow the structure of the original text.
  set s := (mk' (m := 1) fun n ↦ 1 / (n:ℝ) ^ q : Series)q:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ q⊢ s.converges ↔ q > 1
  have hs : s.nonneg := byq:ℝhq:q > 0⊢ (mk' fun n ↦ 1 / ↑↑n ^ q).converges ↔ q > 1 intro nq:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qn:ℤ⊢ s.seq n ≥ 0; simp [s]q:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qn:ℤ⊢ 0 ≤ if 1 ≤ n then (↑n ^ q)⁻¹ else 0; by_cases h : 1 ≤ nposq:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qn:ℤh:1 ≤ n⊢ 0 ≤ if 1 ≤ n then (↑n ^ q)⁻¹ else 0negq:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qn:ℤh:¬1 ≤ n⊢ 0 ≤ if 1 ≤ n then (↑n ^ q)⁻¹ else 0 <;>posq:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qn:ℤh:1 ≤ n⊢ 0 ≤ if 1 ≤ n then (↑n ^ q)⁻¹ else 0negq:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qn:ℤh:¬1 ≤ n⊢ 0 ≤ if 1 ≤ n then (↑n ^ q)⁻¹ else 0 simp [h]All goals completed! 🐙; positivityAll goals completed! 🐙
  have hmono : ∀ n ≥ 1, s.seq (n+1) ≤ s.seq n := byq:ℝhq:q > 0⊢ (mk' fun n ↦ 1 / ↑↑n ^ q).converges ↔ q > 1
    intro n hnq:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonnegn:ℤhn:n ≥ 1⊢ s.seq (n + 1) ≤ s.seq n
    have hn1 : n ≥ 0 := byq:ℝhq:q > 0⊢ (mk' fun n ↦ 1 / ↑↑n ^ q).converges ↔ q > 1 positivityAll goals completed! 🐙
    have hn3 : n.toNat > 0 := byq:ℝhq:q > 0⊢ (mk' fun n ↦ 1 / ↑↑n ^ q).converges ↔ q > 1 omegaAll goals completed! 🐙
    simp [s, hn, hn1]q:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonnegn:ℤhn:n ≥ 1hn1:n ≥ 0hn3:n.toNat > 0⊢ ((↑n + 1) ^ q)⁻¹ ≤ (↑n ^ q)⁻¹
    apply_rules [inv_anti₀, rpow_le_rpow]hbq:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonnegn:ℤhn:n ≥ 1hn1:n ≥ 0hn3:n.toNat > 0⊢ 0 < ↑n ^ qhba.hq:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonnegn:ℤhn:n ≥ 1hn1:n ≥ 0hn3:n.toNat > 0⊢ 0 ≤ ↑nhba.h₁q:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonnegn:ℤhn:n ≥ 1hn1:n ≥ 0hn3:n.toNat > 0⊢ ↑n ≤ ↑n + 1hba.h₂q:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonnegn:ℤhn:n ≥ 1hn1:n ≥ 0hn3:n.toNat > 0⊢ 0 ≤ q <;>hbq:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonnegn:ℤhn:n ≥ 1hn1:n ≥ 0hn3:n.toNat > 0⊢ 0 < ↑n ^ qhba.hq:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonnegn:ℤhn:n ≥ 1hn1:n ≥ 0hn3:n.toNat > 0⊢ 0 ≤ ↑nhba.h₁q:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonnegn:ℤhn:n ≥ 1hn1:n ≥ 0hn3:n.toNat > 0⊢ ↑n ≤ ↑n + 1hba.h₂q:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonnegn:ℤhn:n ≥ 1hn1:n ≥ 0hn3:n.toNat > 0⊢ 0 ≤ q try positivityAll goals completed! 🐙
    simpAll goals completed! 🐙
  rw [cauchy_criterion (by simp [s]) hs hmono]q:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq n⊢ { m := 0, seq := fun n ↦ if n ≥ 0 then (fun k ↦ 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }.converges ↔ q > 1
  have (n:ℕ) : 2^n * s.seq (2^n) = (2^(1-q))^n := byq:ℝhq:q > 0⊢ (mk' fun n ↦ 1 / ↑↑n ^ q).converges ↔ q > 1
    have : 1 ≤ (2:ℤ)^n := byq:ℝhq:q > 0⊢ (mk' fun n ↦ 1 / ↑↑n ^ q).converges ↔ q > 1 norm_castq:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nn:ℕ⊢ 1 ≤ 2 ^ n; exact Nat.one_le_two_powAll goals completed! 🐙
    simp [s, this]q:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nn:ℕthis:1 ≤ 2 ^ n⊢ 2 ^ n * ((2 ^ n) ^ q)⁻¹ = (2 ^ (1 - q)) ^ n
    rw [←rpow_neg, mul_comm, ←rpow_add_one, rpow_pow_comm]q:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nn:ℕthis:1 ≤ 2 ^ n⊢ (2 ^ n) ^ (-q + 1) = (2 ^ n) ^ (1 - q)hxq:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nn:ℕthis:1 ≤ 2 ^ n⊢ 0 ≤ 2hxq:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nn:ℕthis:1 ≤ 2 ^ n⊢ 2 ^ n ≠ 0hxq:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nn:ℕthis:1 ≤ 2 ^ n⊢ 0 ≤ 2 ^ n <;>q:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nn:ℕthis:1 ≤ 2 ^ n⊢ (2 ^ n) ^ (-q + 1) = (2 ^ n) ^ (1 - q)hxq:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nn:ℕthis:1 ≤ 2 ^ n⊢ 0 ≤ 2hxq:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nn:ℕthis:1 ≤ 2 ^ n⊢ 2 ^ n ≠ 0hxq:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nn:ℕthis:1 ≤ 2 ^ n⊢ 0 ≤ 2 ^ n (try positivityAll goals completed! 🐙); grindAll goals completed! 🐙
  simp [this, converges_geom_iff]q:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nthis:∀ (n : ℕ), 2 ^ n * s.seq (2 ^ n) = (2 ^ (1 - q)) ^ n⊢ |2 ^ (1 - q)| < 1 ↔ 1 < q
  rw [abs_of_nonneg, rpow_lt_one_iff_of_pos]q:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nthis:∀ (n : ℕ), 2 ^ n * s.seq (2 ^ n) = (2 ^ (1 - q)) ^ n⊢ 1 < 2 ∧ 1 - q < 0 ∨ 2 < 1 ∧ 0 < 1 - q ↔ 1 < qq:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nthis:∀ (n : ℕ), 2 ^ n * s.seq (2 ^ n) = (2 ^ (1 - q)) ^ n⊢ 0 < 2q:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nthis:∀ (n : ℕ), 2 ^ n * s.seq (2 ^ n) = (2 ^ (1 - q)) ^ n⊢ 0 ≤ 2 ^ (1 - q) <;>q:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nthis:∀ (n : ℕ), 2 ^ n * s.seq (2 ^ n) = (2 ^ (1 - q)) ^ n⊢ 1 < 2 ∧ 1 - q < 0 ∨ 2 < 1 ∧ 0 < 1 - q ↔ 1 < qq:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nthis:∀ (n : ℕ), 2 ^ n * s.seq (2 ^ n) = (2 ^ (1 - q)) ^ n⊢ 0 < 2q:ℝhq:q > 0s:Series := mk' fun n ↦ 1 / ↑↑n ^ qhs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nthis:∀ (n : ℕ), 2 ^ n * s.seq (2 ^ n) = (2 ^ (1 - q)) ^ n⊢ 0 ≤ 2 ^ (1 - q) try positivityAll goals completed! 🐙
  simpAll goals completed! 🐙

Remark 7.3.8

theorem Series.zeta_eq {q:ℝ} (hq: q > 1) : (mk' (m := 1) fun n ↦ 1 / (n:ℝ) ^ q : Series).sum = riemannZeta q := byq:ℝhq:q > 1⊢ ↑(mk' fun n ↦ 1 / ↑↑n ^ q).sum = riemannZeta ↑q
  -- `riemannZeta` is defined over the complex numbers, so some preliminary work is needed to specialize to the reals.
  set L := ∑' n:ℕ, 1 / (n+1:ℝ)^qq:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ q⊢ ↑(mk' fun n ↦ 1 / ↑↑n ^ q).sum = riemannZeta ↑q
  have hL : L = riemannZeta q := byq:ℝhq:q > 1⊢ ↑(mk' fun n ↦ 1 / ↑↑n ^ q).sum = riemannZeta ↑q
    rw [zeta_eq_tsum_one_div_nat_add_one_cpow (by norm_cast)]q:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ q⊢ ↑L = ∑' (n : ℕ), 1 / (↑n + 1) ^ ↑q
    convert Complex.ofReal_tsum _ with nh.e'_3.h.e'_5.hq:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ qn:ℕ⊢ 1 / (↑n + 1) ^ ↑q = ↑(1 / (↑n + 1) ^ q)
    simp [Complex.ofReal_cpow (x := n+1) (by positivity) _]All goals completed! 🐙
  rw [←hL]q:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ qhL:↑L = riemannZeta ↑q⊢ ↑(mk' fun n ↦ 1 / ↑↑n ^ q).sum = ↑L
  norm_castq:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ qhL:↑L = riemannZeta ↑q⊢ (mk' fun n ↦ 1 / ↑↑n ^ q).sum = L; apply sum_of_convergeshq:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ qhL:↑L = riemannZeta ↑q⊢ (mk' fun n ↦ 1 / ↑↑n ^ q).convergesTo L
  have : Summable (fun (n : ℕ)↦ 1 / (n+1:ℝ) ^ q) := byq:ℝhq:q > 1⊢ ↑(mk' fun n ↦ 1 / ↑↑n ^ q).sum = riemannZeta ↑q
    convert (summable_one_div_nat_add_rpow 1 q).mpr hq using 4 with nh.e'_5.h.h.e'_6.h.e'_5q:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ qhL:↑L = riemannZeta ↑qn:ℕ⊢ ↑n + 1 = |↑n + 1|
    rw [abs_of_nonneg]h.e'_5.h.h.e'_6.h.e'_5q:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ qhL:↑L = riemannZeta ↑qn:ℕ⊢ 0 ≤ ↑n + 1; positivityAll goals completed! 🐙
  have tail (a: ℤ → ℝ) (L:ℝ) : Filter.atTop.Tendsto a (nhds L) ↔ Filter.atTop.Tendsto (fun n:ℕ ↦ a n) (nhds L) := byq:ℝhq:q > 1⊢ ↑(mk' fun n ↦ 1 / ↑↑n ^ q).sum = riemannZeta ↑q
    convert Filter.tendsto_map'_iff (g:= fun n:ℕ ↦ (n:ℤ) )h.e'_1.h.e'_4q:ℝhq:q > 1L✝:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ qhL:↑L = riemannZeta ↑qthis:Summable fun n ↦ 1 / (↑n + 1) ^ qa:ℤ → ℝL:ℝ⊢ Filter.atTop = Filter.map (fun n ↦ ↑n) Filter.atTop
    simpAll goals completed! 🐙
  unfold convergesTohq:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ qhL:↑L = riemannZeta ↑qthis:Summable fun n ↦ 1 / (↑n + 1) ^ qtail:∀ (a : ℤ → ℝ) (L : ℝ), Filter.Tendsto a Filter.atTop (nhds L) ↔ Filter.Tendsto (fun n ↦ a ↑n) Filter.atTop (nhds L)⊢ Filter.Tendsto (mk' fun n ↦ 1 / ↑↑n ^ q).partial Filter.atTop (nhds L)
  rw [tail _ L]hq:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ qhL:↑L = riemannZeta ↑qthis:Summable fun n ↦ 1 / (↑n + 1) ^ qtail:∀ (a : ℤ → ℝ) (L : ℝ), Filter.Tendsto a Filter.atTop (nhds L) ↔ Filter.Tendsto (fun n ↦ a ↑n) Filter.atTop (nhds L)⊢ Filter.Tendsto (fun n ↦ (mk' fun n ↦ 1 / ↑↑n ^ q).partial ↑n) Filter.atTop (nhds L)
  convert Summable.tendsto_sum_tsum_nat this with nh.e'_3.hq:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ qhL:↑L = riemannZeta ↑qthis:Summable fun n ↦ 1 / (↑n + 1) ^ qtail:∀ (a : ℤ → ℝ) (L : ℝ), Filter.Tendsto a Filter.atTop (nhds L) ↔ Filter.Tendsto (fun n ↦ a ↑n) Filter.atTop (nhds L)n:ℕ⊢ (mk' fun n ↦ 1 / ↑↑n ^ q).partial ↑n = ∑ i ∈ Finset.range n, 1 / (↑i + 1) ^ q
  simp [Series.partial]h.e'_3.hq:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ qhL:↑L = riemannZeta ↑qthis:Summable fun n ↦ 1 / (↑n + 1) ^ qtail:∀ (a : ℤ → ℝ) (L : ℝ), Filter.Tendsto a Filter.atTop (nhds L) ↔ Filter.Tendsto (fun n ↦ a ↑n) Filter.atTop (nhds L)n:ℕ⊢ (∑ x ∈ Finset.Icc 1 ↑n, if 1 ≤ x then (↑x ^ q)⁻¹ else 0) = ∑ x ∈ Finset.range n, ((↑x + 1) ^ q)⁻¹
  set e : ℕ ↪ ℤ := {
    toFun n := n+1
    inj' _ _ _ := byq:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ qhL:↑L = riemannZeta ↑qthis:Summable fun n ↦ 1 / (↑n + 1) ^ qtail:∀ (a : ℤ → ℝ) (L : ℝ), Filter.Tendsto a Filter.atTop (nhds L) ↔ Filter.Tendsto (fun n ↦ a ↑n) Filter.atTop (nhds L)n:ℕx✝²:ℕx✝¹:ℕx✝:(fun n ↦ ↑n + 1) x✝² = (fun n ↦ ↑n + 1) x✝¹⊢ x✝² = x✝¹ grindAll goals completed! 🐙
  }
  convert Finset.sum_map _ e _ using 2 with n _ m hmh.e'_2.hq:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ qhL:↑L = riemannZeta ↑qthis:Summable fun n ↦ 1 / (↑n + 1) ^ qtail:∀ (a : ℤ → ℝ) (L : ℝ), Filter.Tendsto a Filter.atTop (nhds L) ↔ Filter.Tendsto (fun n ↦ a ↑n) Filter.atTop (nhds L)n:ℕe:ℕ ↪ ℤ := { toFun := fun n ↦ ↑n + 1, inj' := ⋯ }⊢ Finset.Icc 1 ↑n = Finset.map e (Finset.range n)h.e'_3.aq:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ qhL:↑L = riemannZeta ↑qthis:Summable fun n ↦ 1 / (↑n + 1) ^ qtail:∀ (a : ℤ → ℝ) (L : ℝ), Filter.Tendsto a Filter.atTop (nhds L) ↔ Filter.Tendsto (fun n ↦ a ↑n) Filter.atTop (nhds L)n:ℕe:ℕ ↪ ℤ := { toFun := fun n ↦ ↑n + 1, inj' := ⋯ }m:ℕhm:m ∈ Finset.range n⊢ ((↑m + 1) ^ q)⁻¹ = if 1 ≤ e m then (↑(e m) ^ q)⁻¹ else 0
  .h.e'_2.hq:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ qhL:↑L = riemannZeta ↑qthis:Summable fun n ↦ 1 / (↑n + 1) ^ qtail:∀ (a : ℤ → ℝ) (L : ℝ), Filter.Tendsto a Filter.atTop (nhds L) ↔ Filter.Tendsto (fun n ↦ a ↑n) Filter.atTop (nhds L)n:ℕe:ℕ ↪ ℤ := { toFun := fun n ↦ ↑n + 1, inj' := ⋯ }⊢ Finset.Icc 1 ↑n = Finset.map e (Finset.range n) ext xh.e'_2.h.hq:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ qhL:↑L = riemannZeta ↑qthis:Summable fun n ↦ 1 / (↑n + 1) ^ qtail:∀ (a : ℤ → ℝ) (L : ℝ), Filter.Tendsto a Filter.atTop (nhds L) ↔ Filter.Tendsto (fun n ↦ a ↑n) Filter.atTop (nhds L)n:ℕe:ℕ ↪ ℤ := { toFun := fun n ↦ ↑n + 1, inj' := ⋯ }x:ℤ⊢ x ∈ Finset.Icc 1 ↑n ↔ x ∈ Finset.map e (Finset.range n); simp [e]h.e'_2.h.hq:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ qhL:↑L = riemannZeta ↑qthis:Summable fun n ↦ 1 / (↑n + 1) ^ qtail:∀ (a : ℤ → ℝ) (L : ℝ), Filter.Tendsto a Filter.atTop (nhds L) ↔ Filter.Tendsto (fun n ↦ a ↑n) Filter.atTop (nhds L)n:ℕe:ℕ ↪ ℤ := { toFun := fun n ↦ ↑n + 1, inj' := ⋯ }x:ℤ⊢ 1 ≤ x ∧ x ≤ ↑n ↔ ∃ a < n, ↑a + 1 = x; constructorh.e'_2.h.h.mpq:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ qhL:↑L = riemannZeta ↑qthis:Summable fun n ↦ 1 / (↑n + 1) ^ qtail:∀ (a : ℤ → ℝ) (L : ℝ), Filter.Tendsto a Filter.atTop (nhds L) ↔ Filter.Tendsto (fun n ↦ a ↑n) Filter.atTop (nhds L)n:ℕe:ℕ ↪ ℤ := { toFun := fun n ↦ ↑n + 1, inj' := ⋯ }x:ℤ⊢ 1 ≤ x ∧ x ≤ ↑n → ∃ a < n, ↑a + 1 = xh.e'_2.h.h.mprq:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ qhL:↑L = riemannZeta ↑qthis:Summable fun n ↦ 1 / (↑n + 1) ^ qtail:∀ (a : ℤ → ℝ) (L : ℝ), Filter.Tendsto a Filter.atTop (nhds L) ↔ Filter.Tendsto (fun n ↦ a ↑n) Filter.atTop (nhds L)n:ℕe:ℕ ↪ ℤ := { toFun := fun n ↦ ↑n + 1, inj' := ⋯ }x:ℤ⊢ (∃ a < n, ↑a + 1 = x) → 1 ≤ x ∧ x ≤ ↑n
    .h.e'_2.h.h.mpq:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ qhL:↑L = riemannZeta ↑qthis:Summable fun n ↦ 1 / (↑n + 1) ^ qtail:∀ (a : ℤ → ℝ) (L : ℝ), Filter.Tendsto a Filter.atTop (nhds L) ↔ Filter.Tendsto (fun n ↦ a ↑n) Filter.atTop (nhds L)n:ℕe:ℕ ↪ ℤ := { toFun := fun n ↦ ↑n + 1, inj' := ⋯ }x:ℤ⊢ 1 ≤ x ∧ x ≤ ↑n → ∃ a < n, ↑a + 1 = x intro ⟨ _, _ ⟩h.e'_2.h.h.mpq:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ qhL:↑L = riemannZeta ↑qthis:Summable fun n ↦ 1 / (↑n + 1) ^ qtail:∀ (a : ℤ → ℝ) (L : ℝ), Filter.Tendsto a Filter.atTop (nhds L) ↔ Filter.Tendsto (fun n ↦ a ↑n) Filter.atTop (nhds L)n:ℕe:ℕ ↪ ℤ := { toFun := fun n ↦ ↑n + 1, inj' := ⋯ }x:ℤleft✝:1 ≤ xright✝:x ≤ ↑n⊢ ∃ a < n, ↑a + 1 = x; use (x-1).toNathq:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ qhL:↑L = riemannZeta ↑qthis:Summable fun n ↦ 1 / (↑n + 1) ^ qtail:∀ (a : ℤ → ℝ) (L : ℝ), Filter.Tendsto a Filter.atTop (nhds L) ↔ Filter.Tendsto (fun n ↦ a ↑n) Filter.atTop (nhds L)n:ℕe:ℕ ↪ ℤ := { toFun := fun n ↦ ↑n + 1, inj' := ⋯ }x:ℤleft✝:1 ≤ xright✝:x ≤ ↑n⊢ (x - 1).toNat < n ∧ ↑(x - 1).toNat + 1 = x; omegaAll goals completed! 🐙
    grindAll goals completed! 🐙
  simp [e]All goals completed! 🐙

theorem Series.Basel_problem :  (mk' (m := 1) fun n ↦ 1 / (n:ℝ) ^ 2 : Series).sum = Real.pi ^ 2 / 6 := by⊢ (mk' fun n ↦ 1 / ↑↑n ^ 2).sum = π ^ 2 / 6
  have := zeta_eq (show 2 > 1 by⊢ (mk' fun n ↦ 1 / ↑↑n ^ 2).sum = π ^ 2 / 6 norm_numAll goals completed! 🐙)
  simp [Complex.ofReal_ofNat, riemannZeta_two] at thisthis:↑(mk' fun n ↦ (↑↑n ^ 2)⁻¹).sum = ↑π ^ 2 / 6⊢ (mk' fun n ↦ 1 / ↑↑n ^ 2).sum = π ^ 2 / 6
  simpa [←Complex.ofReal_inj]All goals completed! 🐙

Exercise 7.3.3

theorem declaration uses `sorry`Series.nonneg_sum_zero {a:ℕ → ℝ} (ha: (a:Series).nonneg) (hconv: (a:Series).converges) : (a:Series).sum = 0 ↔ ∀ n, a n = 0 := bya:ℕ → ℝha:{ m := 0, seq := fun n ↦ if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.nonneghconv:{ m := 0, seq := fun n ↦ if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.converges⊢ { m := 0, seq := fun n ↦ if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.sum = 0 ↔ ∀ (n : ℕ), a n = 0 sorryAll goals completed! 🐙

end Chapter7