Аналіз I, Глава 7.3

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:

namespace Chapter7abbrev 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 := s:Seriesh:s.nonneg⊢ Monotone s.partial All goals completed! 🐙

Твердження 7.3.1

theorem Series.converges_of_nonneg_iff {s : Series} (h : s.nonneg) : s.converges ↔ ∃ M, ∀ N, s.partial N ≤ M := s: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. s:Seriesh:s.nonneg⊢ s.converges → ∃ M, ∀ (N : ℤ), s.partial N ≤ Ms:Seriesh:s.nonneg⊢ (∃ M, ∀ (N : ℤ), s.partial N ≤ M) → s.converges s:Seriesh:s.nonneg⊢ s.converges → ∃ M, ∀ (N : ℤ), s.partial N ≤ M s:Seriesh:s.nonneghconv:s.converges⊢ ∃ M, ∀ (N : ℤ), s.partial N ≤ M set S : Chapter6.Sequence := ⟨ s.m, s.partial, s:Seriesh:s.nonneghconv:s.converges⊢ ∀ n < s.m, s.partial n = 0 s:Seriesh:s.nonneghconv:s.convergesn:ℤhn:n < s.m⊢ s.partial n = 0; All goals completed! 🐙 ⟩ have : S.isBounded := s:Seriesh:s.nonneg⊢ s.converges ↔ ∃ M, ∀ (N : ℤ), s.partial N ≤ M s:Seriesh:s.nonneghconv:s.convergesS:Chapter6.Sequence := { m := s.m, seq := s.partial, vanish := ⋯ }⊢ S.convergent s:Seriesh:s.nonneghconv:s.convergesS:Chapter6.Sequence := { m := s.m, seq := s.partial, vanish := ⋯ }⊢ ∃ L, Filter.Tendsto S.seq Filter.atTop (nhds L) All goals completed! 🐙 s: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 s: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; s:Seriesh:s.nonneghconv:s.convergesS:Chapter6.Sequence := { m := s.m, seq := s.partial, vanish := ⋯ }M:ℝhpos:M ≥ 0hM:S.BoundedBy MN:ℤ⊢ s.partial N ≤ M; s:Seriesh:s.nonneghconv:s.convergesS:Chapter6.Sequence := { m := s.m, seq := s.partial, vanish := ⋯ }M:ℝhpos:M ≥ 0N:ℤhM:|S.seq N| ≤ M⊢ s.partial N ≤ M All goals completed! 🐙 s:Seriesh:s.nonneghbound:∃ M, ∀ (N : ℤ), s.partial N ≤ M⊢ s.converges s:Seriesh:s.nonneghbound:∃ M, ∀ (N : ℤ), s.partial N ≤ Mhinfin:Filter.Tendsto s.partial Filter.atTop Filter.atTop⊢ s.convergess:Seriesh:s.nonneghbound:∃ M, ∀ (N : ℤ), s.partial N ≤ Mhfin:∃ l, Filter.Tendsto s.partial Filter.atTop (nhds l)⊢ s.converges s:Seriesh:s.nonneghbound:∃ M, ∀ (N : ℤ), s.partial N ≤ Mhinfin:Filter.Tendsto s.partial Filter.atTop Filter.atTop⊢ s.converges s:Seriesh:s.nonneghinfin:Filter.Tendsto s.partial Filter.atTop Filter.atTopM:ℝhM:∀ (N : ℤ), s.partial N ≤ M⊢ s.converges s:Seriesh:s.nonneghinfin:Filter.Tendsto s.partial Filter.atTop Filter.atTopM:ℝhM:∀ (N : ℤ), s.partial N ≤ MN:ℤhN:M < s.partial N⊢ s.converges s:Seriesh:s.nonneghinfin:Filter.Tendsto s.partial Filter.atTop Filter.atTopM:ℝN:ℤhN:M < s.partial NhM:s.partial N ≤ M⊢ s.converges All goals completed! 🐙 All goals completed! 🐙

Наслідок 7.3.2 (Comparison test) / Вправа 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 := s: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 All 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 := s:Seriest:Serieshm:s.m = t.mhcomp:∀ n ≥ s.m, |s.seq n| ≤ t.seq nhdiv:¬s.absConverges⊢ t.diverges All goals completed! 🐙

Лема 7.3.3 (Geometric series) / Вправа 7.3.2

theorem declaration uses 'sorry'Series.converges_geom {x : ℝ} (hx : |x| < 1) : (fun n ↦ x ^ n : Series).convergesTo (1 / (1 - x)) := x:ℝ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)) All goals completed! 🐙
theorem declaration uses 'sorry'Series.absConverges_geom {x : ℝ} (hx : |x| < 1) : (fun n ↦ x ^ n : Series).absConverges := x:ℝhx:|x| < 1⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }.absConverges All goals completed! 🐙theorem declaration uses 'sorry'Series.diverges_geom {x : ℝ} (hx : |x| ≥ 1) : (fun n ↦ x ^ n : Series).diverges := x:ℝhx:|x| ≥ 1⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }.diverges All goals completed! 🐙theorem declaration uses 'sorry'Series.converges_geom_iff (x : ℝ) : (fun n ↦ x ^ n : Series).converges ↔ |x| < 1 := x:ℝ⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }.converges ↔ |x| < 1 All goals completed! 🐙

Твердження 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 := s: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 -- цей доказ написан так, щоб співпадати із структурою орігінального тексту. 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 := s: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 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 := ⋯ }n:ℤ⊢ t.seq n ≥ 0 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 := ⋯ }n:ℤh:n ≥ 0⊢ t.seq n ≥ 0s: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 all_goals All goals completed! 🐙 All goals completed! 🐙 have hmono' : ∀ n ≥ 1, ∀ m ≥ n, s.seq m ≤ s.seq n := s: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 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.nonnegn:ℤhn:n ≥ 1m:ℤhm:m ≥ n⊢ s.seq m ≤ s.seq n 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.nonnegn:ℤhn:n ≥ 1k:ℕhm:n + ↑k ≥ n⊢ s.seq (n + ↑k) ≤ s.seq n 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.nonnegn:ℤhn:n ≥ 1k:ℕ⊢ s.seq (n + ↑k) ≤ s.seq n 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.nonnegn:ℤhn:n ≥ 1⊢ s.seq (n + ↑0) ≤ s.seq 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 := ⋯ }ht:t.nonnegn:ℤhn:n ≥ 1k:ℕhk:s.seq (n + ↑k) ≤ s.seq n⊢ s.seq (n + ↑(k + 1)) ≤ s.seq n 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.nonnegn:ℤhn:n ≥ 1⊢ s.seq (n + ↑0) ≤ s.seq n All goals completed! 🐙 convert (hmono (n+k) (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.nonnegn:ℤhn:n ≥ 1k:ℕhk:s.seq (n + ↑k) ≤ s.seq n⊢ n + ↑k ≥ 1 All goals completed! 🐙)).trans hk using 2 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.nonnegn:ℤhn:n ≥ 1k:ℕhk:s.seq (n + ↑k) ≤ s.seq n⊢ n + (↑k + 1) = n + ↑k + 1; All goals completed! 🐙 have htm : t.m = 0 := s: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 All goals completed! 🐙 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 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.partial⊢ (∃ M, ∀ (N : ℤ), S N ≤ M) ↔ ∃ M, ∀ (N : ℤ), t.partial N ≤ M 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.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) := s: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 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.partial⊢ S (2 ^ (0 + 1) - 1) ≤ T ↑0 ∧ T ↑0 ≤ 2 * S (2 ^ 0)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:ℕ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)) 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.partial⊢ S (2 ^ (0 + 1) - 1) ≤ T ↑0 ∧ T ↑0 ≤ 2 * S (2 ^ 0) 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.partial⊢ s.seq 1 ≤ 2 * s.seq 1 All goals completed! 🐙 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:ℕ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)) 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:ℕ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)) 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)⊢ 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)) := s: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 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)⊢ ↑K ≥ t.m - 1 All goals completed! 🐙 have claim2a : S (2^(K+1)) ≥ S (2^K) + 2^K * s.seq (2^(K+1)) := calc _ = S (2^K) + ∑ n ∈ Finset.Ioc (2^K) (2^(K+1)), s.seq n := 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))⊢ 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))) := 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))⊢ S (2 ^ (K + 1)) = S (2 ^ K) + ∑ n ∈ Finset.Ioc (2 ^ K) (2 ^ (K + 1)), s.seq n 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 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))x:ℤhx:x ∈ Finset.Icc s.m (2 ^ K)y:ℤhy:y ∈ Finset.Ioc (2 ^ K) (2 ^ (K + 1))⊢ x ≠ y 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))x:ℤy:ℤhx:s.m ≤ x ∧ x ≤ 2 ^ Khy:2 ^ K < y ∧ y ≤ 2 ^ (K + 1)⊢ x ≠ y; All goals completed! 🐙 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))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)) 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))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)); 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))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) 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))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)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))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) 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))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) 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))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) All goals completed! 🐙 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))this:Disjoint (Finset.Icc s.m (2 ^ K)) (Finset.Ioc (2 ^ K) (2 ^ (K + 1)))x:ℤh:s.m ≤ x ∧ x ≤ 2 ^ K ∨ 2 ^ K < x ∧ x ≤ 2 ^ (K + 1)⊢ s.m ≤ x ∧ x ≤ 2 ^ (K + 1) 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))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)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))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) 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))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) 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))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; All goals completed! 🐙 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))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; All goals completed! 🐙 _ ≥ S (2^K) + ∑ n ∈ Finset.Ioc ((2:ℤ)^K) (2^(K+1)), s.seq (2^(K+1)) := 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))⊢ 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)) 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))n:ℤhn:n ∈ Finset.Ioc (2 ^ K) (2 ^ (K + 1))⊢ s.seq (2 ^ (K + 1)) ≤ s.seq n 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))n:ℤhn:2 ^ K < n ∧ n ≤ 2 ^ (K + 1)⊢ s.seq (2 ^ (K + 1)) ≤ s.seq n exact hmono' _ (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))n:ℤhn:2 ^ K < n ∧ n ≤ 2 ^ (K + 1)⊢ n ≥ 1 All goals completed! 🐙) _ hn.2 _ = _ := 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))⊢ 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)) 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; 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: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 All goals completed! 🐙 have claim2 : 2 * S (2^(K+1)) ≥ 2 * S (2^K) + 2^(K+1) * s.seq (2^(K+1)) := s: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 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)); All 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 ∈ Finset.Icc (2^(K+1)) (2^(K+1+1)-1), s.seq n := 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))⊢ 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)) := 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))⊢ 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 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 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))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 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))x:ℤy:ℤhx:s.m ≤ x ∧ x ≤ 2 ^ (K + 1) - 1hy:2 ^ (K + 1) ≤ y ∧ y ≤ 2 ^ (K + 1 + 1) - 1⊢ x ≠ y; All goals completed! 🐙 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))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) 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))this:Disjoint (Finset.Icc s.m (2 ^ (K + 1) - 1)) (Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1))x:ℤ⊢ x ∈ Finset.Icc s.m (2 ^ (K + 1 + 1) - 1) ↔ x ∈ Finset.Icc s.m (2 ^ (K + 1) - 1) ∪ Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1); 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))this:Disjoint (Finset.Icc s.m (2 ^ (K + 1) - 1)) (Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1))x:ℤ⊢ s.m ≤ x ∧ x ≤ 2 ^ (K + 1 + 1) - 1 ↔ s.m ≤ x ∧ x ≤ 2 ^ (K + 1) - 1 ∨ 2 ^ (K + 1) ≤ x ∧ x ≤ 2 ^ (K + 1 + 1) - 1 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))this:Disjoint (Finset.Icc s.m (2 ^ (K + 1) - 1)) (Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1))x:ℤ⊢ s.m ≤ x ∧ x ≤ 2 ^ (K + 1 + 1) - 1 → s.m ≤ x ∧ x ≤ 2 ^ (K + 1) - 1 ∨ 2 ^ (K + 1) ≤ x ∧ x ≤ 2 ^ (K + 1 + 1) - 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))this:Disjoint (Finset.Icc s.m (2 ^ (K + 1) - 1)) (Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1))x:ℤ⊢ s.m ≤ x ∧ x ≤ 2 ^ (K + 1) - 1 ∨ 2 ^ (K + 1) ≤ x ∧ x ≤ 2 ^ (K + 1 + 1) - 1 → s.m ≤ x ∧ x ≤ 2 ^ (K + 1 + 1) - 1 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))this:Disjoint (Finset.Icc s.m (2 ^ (K + 1) - 1)) (Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1))x:ℤ⊢ s.m ≤ x ∧ x ≤ 2 ^ (K + 1 + 1) - 1 → s.m ≤ x ∧ x ≤ 2 ^ (K + 1) - 1 ∨ 2 ^ (K + 1) ≤ x ∧ x ≤ 2 ^ (K + 1 + 1) - 1 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))this:Disjoint (Finset.Icc s.m (2 ^ (K + 1) - 1)) (Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1))x:ℤh1:s.m ≤ xh2:x ≤ 2 ^ (K + 1 + 1) - 1⊢ s.m ≤ x ∧ x ≤ 2 ^ (K + 1) - 1 ∨ 2 ^ (K + 1) ≤ x ∧ x ≤ 2 ^ (K + 1 + 1) - 1 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))this:Disjoint (Finset.Icc s.m (2 ^ (K + 1) - 1)) (Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1))x:ℤh1:s.m ≤ xh2:x ≤ 2 ^ (K + 1 + 1) - 1⊢ x ≤ 2 ^ (K + 1) - 1 ∨ 2 ^ (K + 1) ≤ x; All goals completed! 🐙 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))this:Disjoint (Finset.Icc s.m (2 ^ (K + 1) - 1)) (Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1))x:ℤh:s.m ≤ x ∧ x ≤ 2 ^ (K + 1) - 1 ∨ 2 ^ (K + 1) ≤ x ∧ x ≤ 2 ^ (K + 1 + 1) - 1⊢ s.m ≤ x ∧ x ≤ 2 ^ (K + 1 + 1) - 1 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))this:Disjoint (Finset.Icc s.m (2 ^ (K + 1) - 1)) (Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1))x:ℤh1:s.m ≤ xh2:x ≤ 2 ^ (K + 1) - 1⊢ s.m ≤ x ∧ x ≤ 2 ^ (K + 1 + 1) - 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))this:Disjoint (Finset.Icc s.m (2 ^ (K + 1) - 1)) (Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1))x:ℤh1:2 ^ (K + 1) ≤ xh2:x ≤ 2 ^ (K + 1 + 1) - 1⊢ s.m ≤ x ∧ x ≤ 2 ^ (K + 1 + 1) - 1 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))this:Disjoint (Finset.Icc s.m (2 ^ (K + 1) - 1)) (Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1))x:ℤh1:s.m ≤ xh2:x ≤ 2 ^ (K + 1) - 1⊢ s.m ≤ x ∧ x ≤ 2 ^ (K + 1 + 1) - 1 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))this:Disjoint (Finset.Icc s.m (2 ^ (K + 1) - 1)) (Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1))x:ℤh1:s.m ≤ xh2:x ≤ 2 ^ (K + 1) - 1⊢ x ≤ 2 * 2 ^ (K + 1) - 1; All goals completed! 🐙 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))this:Disjoint (Finset.Icc s.m (2 ^ (K + 1) - 1)) (Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1))x:ℤh1:2 ^ (K + 1) ≤ xh2:x ≤ 2 ^ (K + 1 + 1) - 1⊢ 1 ≤ x; All goals completed! 🐙 _ ≤ S (2^(K+1)-1) + ∑ n ∈ Finset.Icc ((2:ℤ)^(K+1)) (2^(K+1+1)-1), s.seq (2^(K+1)) := 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))⊢ 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)) 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))n:ℤhn:n ∈ Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1)⊢ s.seq n ≤ s.seq (2 ^ (K + 1)) 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))n:ℤhn:2 ^ (K + 1) ≤ n ∧ n ≤ 2 ^ (K + 1 + 1) - 1⊢ s.seq n ≤ s.seq (2 ^ (K + 1)) exact hmono' _ (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))n:ℤhn:2 ^ (K + 1) ≤ n ∧ n ≤ 2 ^ (K + 1 + 1) - 1⊢ 2 ^ (K + 1) ≥ 1 All goals completed! 🐙) _ hn.1 _ = _ := 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))⊢ 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)) 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; 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: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 All goals completed! 🐙 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))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)) 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))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)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))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)) 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))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)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))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)) All goals completed! 🐙 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, ∀ (N : ℤ), S N ≤ M) → ∃ M, ∀ (N : ℤ), T 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.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 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, ∀ (N : ℤ), S N ≤ M) → ∃ M, ∀ (N : ℤ), T N ≤ M 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)h:∃ M, ∀ (N : ℤ), S N ≤ M⊢ ∃ M, ∀ (N : ℤ), T N ≤ M 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 : ℤ), S N ≤ M⊢ ∃ M, ∀ (N : ℤ), T N ≤ M 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 : ℤ), S N ≤ M⊢ ∀ (N : ℤ), T N ≤ 2 * M 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 : ℤ), S N ≤ MN:ℤ⊢ T N ≤ 2 * M; 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 : ℤ), S N ≤ MN:ℤhN:N < 0⊢ T N ≤ 2 * 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.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 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 : ℤ), S N ≤ MN:ℤhN:N < 0⊢ T N ≤ 2 * M 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 : ℤ), S N ≤ MN:ℤhN:N < 0⊢ 0 ≤ M 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 : ℤ), S N ≤ MN:ℤhN:N < 0⊢ 0 = S 0 All goals completed! 🐙 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 : ℤ), S N ≤ MN:ℤhN:N ≥ 0⊢ T ↑N.toNat ≤ 2 * M 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 : ℤ), S N ≤ MN:ℤhN:N ≥ 0⊢ 2 * S (2 ^ N.toNat) ≤ 2 * M 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 : ℤ), S N ≤ MN:ℤhN:N ≥ 0⊢ S (2 ^ N.toNat) ≤ M All goals completed! 🐙 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)h:∃ M, ∀ (N : ℤ), T N ≤ M⊢ ∃ M, ∀ (N : ℤ), S N ≤ M 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 ≤ M⊢ ∃ M, ∀ (N : ℤ), S N ≤ M 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 ≤ M⊢ ∀ (N : ℤ), S N ≤ M 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':ℤ⊢ S K' ≤ M 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':K' < 1⊢ S K' ≤ 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.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 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':K' < 1⊢ S K' ≤ M 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':K' < 1⊢ 0 ≤ M All goals completed! 🐙 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':K' ≥ 1K:ℕ := (K' - 1).toNat⊢ S K' ≤ M have hK : K' = K + 1 := s: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 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':K' ≥ 1K:ℕ := (K' - 1).toNat⊢ K' = K' - 1 + 1 All goals completed! 🐙 calc _ ≤ S (2 ^ (K+1) - 1) := 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':K' ≥ 1K:ℕ := (K' - 1).toNathK:K' = ↑K + 1⊢ S K' ≤ S (2 ^ (K + 1) - 1) 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':K' ≥ 1K:ℕ := (K' - 1).toNathK:K' = ↑K + 1⊢ K' ≤ 2 ^ (K + 1) - 1 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':K' ≥ 1K:ℕ := (K' - 1).toNathK:K' = ↑K + 1⊢ ↑K + 1 ≤ 2 ^ (K + 1) - 1 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':K' ≥ 1K:ℕ := (K' - 1).toNathK:K' = ↑K + 1n:ℕ⊢ ↑n + 1 ≤ 2 ^ (n + 1) - 1 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':K' ≥ 1K:ℕ := (K' - 1).toNathK:K' = ↑K + 1⊢ ↑0 + 1 ≤ 2 ^ (0 + 1) - 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.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' ≥ 1K:ℕ := (K' - 1).toNathK:K' = ↑K + 1n:ℕhn:↑n + 1 ≤ 2 ^ (n + 1) - 1⊢ ↑(n + 1) + 1 ≤ 2 ^ (n + 1 + 1) - 1 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':K' ≥ 1K:ℕ := (K' - 1).toNathK:K' = ↑K + 1⊢ ↑0 + 1 ≤ 2 ^ (0 + 1) - 1 All goals completed! 🐙 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':K' ≥ 1K:ℕ := (K' - 1).toNathK:K' = ↑K + 1n:ℕhn:↑n + 1 ≤ 2 ^ n * 2 - 1⊢ ↑n + 1 + 1 ≤ 2 ^ n * 2 * 2 - 1 All goals completed! 🐙 _ ≤ T K := (Lemma_7_3_6 K).1 _ ≤ M := hM K

Наслідок 7.3.7

theorem Series.converges_qseries (q : ℝ) (hq : q > 0) : (mk' (m := 1) fun n ↦ 1 / (n:ℝ) ^ q : Series).converges ↔ (q>1) := q:ℝhq:q > 0⊢ (mk' fun n => 1 / ↑↑n ^ q).converges ↔ q > 1 -- цей доказ написан так, щоб співпадати із структурою орігінального тексту. q:ℝhq:q > 0s:Series := mk' fun n => 1 / ↑↑n ^ q⊢ s.converges ↔ q > 1 have hs : s.nonneg := q:ℝhq:q > 0⊢ (mk' fun n => 1 / ↑↑n ^ q).converges ↔ q > 1 q:ℝhq:q > 0s:Series := mk' fun n => 1 / ↑↑n ^ qn:ℤ⊢ s.seq n ≥ 0; q:ℝhq:q > 0s:Series := mk' fun n => 1 / ↑↑n ^ qn:ℤ⊢ 0 ≤ if 1 ≤ n then (↑n ^ q)⁻¹ else 0; q:ℝhq:q > 0s:Series := mk' fun n => 1 / ↑↑n ^ qn:ℤh:1 ≤ n⊢ 0 ≤ if 1 ≤ n then (↑n ^ q)⁻¹ else 0q:ℝhq:q > 0s:Series := mk' fun n => 1 / ↑↑n ^ qn:ℤh:¬1 ≤ n⊢ 0 ≤ if 1 ≤ n then (↑n ^ q)⁻¹ else 0 q:ℝhq:q > 0s:Series := mk' fun n => 1 / ↑↑n ^ qn:ℤh:1 ≤ n⊢ 0 ≤ if 1 ≤ n then (↑n ^ q)⁻¹ else 0q:ℝhq:q > 0s:Series := mk' fun n => 1 / ↑↑n ^ qn:ℤh:¬1 ≤ n⊢ 0 ≤ if 1 ≤ n then (↑n ^ q)⁻¹ else 0 All goals completed! 🐙; All goals completed! 🐙 have hmono : ∀ n ≥ 1, s.seq (n+1) ≤ s.seq n := q:ℝhq:q > 0⊢ (mk' fun n => 1 / ↑↑n ^ q).converges ↔ q > 1 q:ℝ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 := q:ℝhq:q > 0⊢ (mk' fun n => 1 / ↑↑n ^ q).converges ↔ q > 1 All goals completed! 🐙 have hn3 : n.toNat > 0 := q:ℝhq:q > 0⊢ (mk' fun n => 1 / ↑↑n ^ q).converges ↔ q > 1 All goals completed! 🐙 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 inv_anti₀ (q:ℝhq:q > 0s:Series := mk' fun n => 1 / ↑↑n ^ qhs:s.nonnegn:ℤhn:n ≥ 1hn1:n ≥ 0hn3:n.toNat > 0⊢ 0 < ↑n ^ q All goals completed! 🐙) exact Real.rpow_le_rpow (q:ℝhq:q > 0s:Series := mk' fun n => 1 / ↑↑n ^ qhs:s.nonnegn:ℤhn:n ≥ 1hn1:n ≥ 0hn3:n.toNat > 0⊢ 0 ≤ ↑n All goals completed! 🐙) (q:ℝhq:q > 0s:Series := mk' fun n => 1 / ↑↑n ^ qhs:s.nonnegn:ℤhn:n ≥ 1hn1:n ≥ 0hn3:n.toNat > 0⊢ ↑n ≤ ↑n + 1 All goals completed! 🐙) (q:ℝhq:q > 0s:Series := mk' fun n => 1 / ↑↑n ^ qhs:s.nonnegn:ℤhn:n ≥ 1hn1:n ≥ 0hn3:n.toNat > 0⊢ 0 ≤ q All goals completed! 🐙) 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 := q:ℝhq:q > 0⊢ (mk' fun n => 1 / ↑↑n ^ q).converges ↔ q > 1 have : 1 ≤ (2:ℤ)^n := q:ℝhq:q > 0⊢ (mk' fun n => 1 / ↑↑n ^ q).converges ↔ q > 1 q:ℝhq:q > 0s:Series := mk' fun n => 1 / ↑↑n ^ qhs:s.nonneghmono:∀ n ≥ 1, s.seq (n + 1) ≤ s.seq nn:ℕ⊢ 1 ≤ 2 ^ n; All goals completed! 🐙 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 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) 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⊢ -q + 1 = 1 - q; All goals completed! 🐙 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 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 < q All goals completed! 🐙

Ремарка 7.3.8

theorem Series.zeta_eq {q:ℝ} (hq: q > 1) : (mk' (m := 1) fun n ↦ 1 / (n:ℝ) ^ q : Series).sum = riemannZeta q := q:ℝ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. q:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ q⊢ ↑(mk' fun n => 1 / ↑↑n ^ q).sum = riemannZeta ↑q have hL : L = riemannZeta q := q:ℝhq:q > 1⊢ ↑(mk' fun n => 1 / ↑↑n ^ q).sum = riemannZeta ↑q q:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ q⊢ ↑L = ∑' (n : ℕ), 1 / (↑n + 1) ^ ↑q q:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ q⊢ ↑(∑' (n : ℕ), 1 / (↑n + 1) ^ q) = ∑' (n : ℕ), 1 / (↑n + 1) ^ ↑q q:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ qn:ℕ⊢ 1 / (↑n + 1) ^ ↑q = ↑(1 / (↑n + 1) ^ q) All goals completed! 🐙 q:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ qhL:↑L = riemannZeta ↑q⊢ ↑(mk' fun n => 1 / ↑↑n ^ q).sum = ↑L q:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ qhL:↑L = riemannZeta ↑q⊢ (mk' fun n => 1 / ↑↑n ^ q).sum = L q:ℝ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) := q:ℝhq:q > 1⊢ ↑(mk' fun n => 1 / ↑↑n ^ q).sum = riemannZeta ↑q q:ℝhq:q > 1L:ℝ := ∑' (n : ℕ), 1 / (↑n + 1) ^ qhL:↑L = riemannZeta ↑qn:ℕ⊢ ↑n + 1 = |↑n + 1| All goals completed! 🐙 have tail (a: ℤ → ℝ) (L:ℝ) : Filter.Tendsto a Filter.atTop (nhds L) ↔ Filter.Tendsto (fun n:ℕ ↦ a n) Filter.atTop (nhds L) := q:ℝhq:q > 1⊢ ↑(mk' fun n => 1 / ↑↑n ^ q).sum = riemannZeta ↑q q:ℝ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 All goals completed! 🐙 q:ℝ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) q:ℝ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) q:ℝ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 q:ℝ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' := q:ℝ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:ℕ⊢ Function.Injective fun n => ↑n + 1 q:ℝ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:ℕa:ℕb:ℕh:(fun n => ↑n + 1) a = (fun n => ↑n + 1) b⊢ a = b; q:ℝ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:ℕa:ℕb:ℕh:a = b⊢ a = b; All goals completed! 🐙 } q:ℝ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)q:ℝ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 q:ℝ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) q:ℝ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) q:ℝ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 q:ℝ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 = xq:ℝ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 q:ℝ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 q:ℝ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:ℤh1:1 ≤ xh2:x ≤ ↑n⊢ ∃ a < n, ↑a + 1 = x q:ℝ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:ℤh1:1 ≤ xh2:x ≤ ↑n⊢ (x - 1).toNat < n ∧ ↑(x - 1).toNat + 1 = x; All goals completed! 🐙 q:ℝ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:ℕhan:a < nhax:↑a + 1 = x⊢ 1 ≤ x ∧ x ≤ ↑n; All goals completed! 🐙 All goals completed! 🐙
theorem Series.Basel_problem : (mk' (m := 1) fun n ↦ 1 / (n:ℝ) ^ 2 : Series).sum = Real.pi ^ 2 / 6 := ⊢ (mk' fun n => 1 / ↑↑n ^ 2).sum = Real.pi ^ 2 / 6 have := zeta_eq (show 2 > 1 ⊢ (mk' fun n => 1 / ↑↑n ^ 2).sum = Real.pi ^ 2 / 6 All goals completed! 🐙) this:↑(mk' fun n => (↑↑n ^ 2)⁻¹).sum = ↑Real.pi ^ 2 / 6⊢ (mk' fun n => 1 / ↑↑n ^ 2).sum = Real.pi ^ 2 / 6 All goals completed! 🐙

Вправа 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 := a:ℕ → ℝ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 All goals completed! 🐙
end Chapter7