Imports
import Mathlib.Tactic
import Analysis.Section_6_4
import Analysis.Section_7_4
import Mathlib.Topology.Instances.EReal.Lemmas
import Mathlib.Analysis.SpecialFunctions.Pow.ContinuityAnalysis I, Section 7.5: The root and ratio tests
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:
-
The root and ratio tests/
A point that is only implicitly stated in the text is that for the root and ratio tests, the lim inf and lim sup should be interpreted within the extended reals. The Lean formalizations below make this point more explicit.
namespace Chapter7open Filter Real ERealTheorem 7.5.1(a) (Root test). A technical condition is needed to ensure the limsup is finite.
theorem Series.root_test_pos {s : Series}
(h : atTop.limsup (fun n ↦ ((|s.seq n|^(1/(n:ℝ)):ℝ):EReal)) < 1) : s.absConverges := s:Seriesh:limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTop < 1⊢ s.absConverges
-- This proof is written to follow the structure of the original text.
s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atToph:α' < 1⊢ s.absConverges
have hpos : 0 ≤ α' := s:Seriesh:limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTop < 1⊢ s.absConverges
apply le_limsup_of_frequently_le (Frequently.of_forall _) (s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atToph:α' < 1⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ ↑(|s.seq n| ^ (1 / ↑n)) All goals completed! 🐙)
s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atToph:α' < 1x✝:ℤ⊢ 0 ≤ ↑(|s.seq x✝| ^ (1 / ↑x✝)); All goals completed! 🐙
s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atToph:α' < 1hpos:0 ≤ α'α:ℝ := α'.toReal⊢ s.absConverges
have hαα' : α' = α := s:Seriesh:limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTop < 1⊢ s.absConverges
s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atToph:α' < 1hpos:0 ≤ α'α:ℝ := α'.toReal⊢ ↑α = α'; s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atToph:α' < 1hpos:0 ≤ α'α:ℝ := α'.toReal⊢ α' ≠ ⊤s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atToph:α' < 1hpos:0 ≤ α'α:ℝ := α'.toReal⊢ α' ≠ ⊥
s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atToph:α' < 1hpos:0 ≤ α'α:ℝ := α'.toReal⊢ α' ≠ ⊤ s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTophpos:0 ≤ α'α:ℝ := α'.toRealh:α' = ⊤⊢ 1 ≤ α'; s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTophpos:0 ≤ α'α:ℝ := α'.toRealh:α' = ⊤⊢ 1 ≤ ⊤; All goals completed! 🐙
s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atToph:α' < 1α:ℝ := α'.toRealhpos:α' = ⊥⊢ α' < 0; All goals completed! 🐙
s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhpos:0 ≤ ↑αh:↑α < 1hαα':α' = ↑α⊢ s.absConverges; s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ α⊢ s.absConverges
s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2⊢ s.absConverges
have hε : 0 < ε := s:Seriesh:limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTop < 1⊢ s.absConverges s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2⊢ α < 1; All goals completed! 🐙
have hε' : α' < (α+ε:ℝ) := s:Seriesh:limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTop < 1⊢ s.absConverges s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < ε⊢ α < α + ε; All goals completed! 🐙
have hα : α + ε < 1 := s:Seriesh:limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTop < 1⊢ s.absConverges s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)⊢ α + (1 - α) / 2 < 1; All goals completed! 🐙
have hα' : 0 < α + ε := s:Seriesh:limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTop < 1⊢ s.absConverges All goals completed! 🐙
have := eventually_lt_of_limsup_lt hε' (s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + ε⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ ↑(|s.seq n| ^ (1 / ↑n)) All goals completed! 🐙)
s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εthis:∃ a, ∀ b ≥ a, ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)⊢ s.absConverges
s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)⊢ s.absConverges; s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)⊢ s.absConverges
have (n:ℤ) (hn: n ≥ N) : |s.seq n| ≤ (α + ε)^n := s:Seriesh:limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTop < 1⊢ s.absConverges
have : n ≥ N' := s:Seriesh:limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTop < 1⊢ s.absConverges All goals completed! 🐙
have npos : 0 < n := s:Seriesh:limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTop < 1⊢ s.absConverges All goals completed! 🐙
s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤN:ℤ := max N' (max s.m 1)n:ℤhn:n ≥ Nthis:n ≥ N'npos:0 < nhN:↑(|s.seq n| ^ (1 / ↑n)) < ↑(α + ε)⊢ |s.seq n| ≤ (α + ε) ^ n
s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤN:ℤ := max N' (max s.m 1)n:ℤhn:n ≥ Nthis:n ≥ N'npos:0 < nhN:|s.seq n| ^ (1 / ↑n) < α + ε⊢ |s.seq n| ≤ (α + ε) ^ n
calc
_ = (|s.seq n|^(1/(n:ℝ)))^n := s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤN:ℤ := max N' (max s.m 1)n:ℤhn:n ≥ Nthis:n ≥ N'npos:0 < nhN:|s.seq n| ^ (1 / ↑n) < α + ε⊢ |s.seq n| = (|s.seq n| ^ (1 / ↑n)) ^ n
s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤN:ℤ := max N' (max s.m 1)n:ℤhn:n ≥ Nthis:n ≥ N'npos:0 < nhN:|s.seq n| ^ (1 / ↑n) < α + ε⊢ |s.seq n| = |s.seq n| ^ (1 / ↑n * ↑n)
s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤN:ℤ := max N' (max s.m 1)n:ℤhn:n ≥ Nthis:n ≥ N'npos:0 < nhN:|s.seq n| ^ (1 / ↑n) < α + ε⊢ |s.seq n| ^ (1 / ↑n * ↑n) = |s.seq n|; s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤN:ℤ := max N' (max s.m 1)n:ℤhn:n ≥ Nthis:n ≥ N'npos:0 < nhN:|s.seq n| ^ (1 / ↑n) < α + ε⊢ 1 / ↑n * ↑n = 1; All goals completed! 🐙
_ ≤ _ := s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤN:ℤ := max N' (max s.m 1)n:ℤhn:n ≥ Nthis:n ≥ N'npos:0 < nhN:|s.seq n| ^ (1 / ↑n) < α + ε⊢ (|s.seq n| ^ (1 / ↑n)) ^ n ≤ (α + ε) ^ n
convert pow_le_pow_left₀ (s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤN:ℤ := max N' (max s.m 1)n:ℤhn:n ≥ Nthis:n ≥ N'npos:0 < nhN:|s.seq n| ^ (1 / ↑n) < α + ε⊢ 0 ≤ |s.seq n| ^ (1 / ↑n) All goals completed! 🐙) (le_of_lt hN) n.toNat
all_goals s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤN:ℤ := max N' (max s.m 1)n:ℤhn:n ≥ Nthis:n ≥ N'npos:0 < nhN:|s.seq n| ^ (1 / ↑n) < α + ε⊢ n = ↑n.toNat; All goals completed! 🐙
s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNat⊢ s.absConverges
have hNk : N = s.m + k := s:Seriesh:limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTop < 1⊢ s.absConverges All goals completed! 🐙
have hgeom : (fun n ↦ (α+ε) ^ n : Series).converges := s:Seriesh:limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTop < 1⊢ s.absConverges
All goals completed! 🐙
s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).converges⊢ s.absConverges
have : (s.from N).absConverges := s:Seriesh:limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTop < 1⊢ s.absConverges
s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).converges⊢ (s.from N).m =
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).ms:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).converges⊢ ∀ n ≥ (s.from N).m,
|(s.from N).seq n| ≤
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).seq
n
s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).converges⊢ (s.from N).m =
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).m s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).converges⊢ max s.m N = max N 0; All goals completed! 🐙
intro n s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).convergesn:ℤhn:n ≥ (s.from N).m⊢ |(s.from N).seq n| ≤
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).seq
n; s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).convergesn:ℤhn:s.m ≤ n ∧ N ≤ n⊢ |(s.from N).seq n| ≤
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).seq
n
have hn' : n ≥ 0 := s:Seriesh:limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTop < 1⊢ s.absConverges All goals completed! 🐙
s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).convergesn:ℤhn:s.m ≤ n ∧ N ≤ nhn':n ≥ 0⊢ |s.seq n| ≤ (α + ε) ^ n.toNat
s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).convergesn:ℤhn:s.m ≤ n ∧ N ≤ nhn':n ≥ 0⊢ (α + ε) ^ n.toNat = (α + ε) ^ n; s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).convergesn:ℤhn:s.m ≤ n ∧ N ≤ nhn':n ≥ 0⊢ (α + ε) ^ n = (α + ε) ^ n.toNat; s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).convergesn:ℤhn:s.m ≤ n ∧ N ≤ nhn':n ≥ 0⊢ n = ↑n.toNat; All goals completed! 🐙
s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this✝:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).convergesthis:(s.from N).abs.converges⊢ s.abs.converges
s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this✝:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).convergesthis:(s.from N).abs.converges⊢ (s.abs.from (s.abs.m + ↑k)).converges; s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this✝:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).convergesthis:(s.from N).abs.converges⊢ s.abs.from (s.abs.m + ↑k) = (s.from N).abs; s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this✝:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).convergesthis:(s.from N).abs.converges⊢ s.m + ↑k = max s.m N ∧
(fun n ↦ if s.m + ↑k ≤ n then if s.m ≤ n then |s.seq n| else 0 else 0) = fun n ↦
if s.m ≤ n ∧ N ≤ n then |if s.m ≤ n ∧ N ≤ n then s.seq n else 0| else 0; refine ⟨ s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this✝:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).convergesthis:(s.from N).abs.converges⊢ s.m + ↑k = max s.m N All goals completed! 🐙, ?_ ⟩
s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this✝:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).convergesthis:(s.from N).abs.convergesn:ℤ⊢ (if s.m + ↑k ≤ n then if s.m ≤ n then |s.seq n| else 0 else 0) =
if s.m ≤ n ∧ N ≤ n then |if s.m ≤ n ∧ N ≤ n then s.seq n else 0| else 0
s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this✝:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).convergesthis:(s.from N).abs.convergesn:ℤhnm:n ≥ s.m⊢ (if s.m + ↑k ≤ n then if s.m ≤ n then |s.seq n| else 0 else 0) =
if s.m ≤ n ∧ N ≤ n then |if s.m ≤ n ∧ N ≤ n then s.seq n else 0| else 0s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this✝:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).convergesthis:(s.from N).abs.convergesn:ℤhnm:¬n ≥ s.m⊢ (if s.m + ↑k ≤ n then if s.m ≤ n then |s.seq n| else 0 else 0) =
if s.m ≤ n ∧ N ≤ n then |if s.m ≤ n ∧ N ≤ n then s.seq n else 0| else 0 s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this✝:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).convergesthis:(s.from N).abs.convergesn:ℤhnm:n ≥ s.m⊢ (if s.m + ↑k ≤ n then if s.m ≤ n then |s.seq n| else 0 else 0) =
if s.m ≤ n ∧ N ≤ n then |if s.m ≤ n ∧ N ≤ n then s.seq n else 0| else 0s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this✝:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).convergesthis:(s.from N).abs.convergesn:ℤhnm:¬n ≥ s.m⊢ (if s.m + ↑k ≤ n then if s.m ≤ n then |s.seq n| else 0 else 0) =
if s.m ≤ n ∧ N ≤ n then |if s.m ≤ n ∧ N ≤ n then s.seq n else 0| else 0 All goals completed! 🐙
s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this✝:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).convergesthis:(s.from N).abs.convergesn:ℤhnm:n ≥ s.mhn:n ≥ N⊢ (if s.m + ↑k ≤ n then |s.seq n| else 0) = if N ≤ n then |if N ≤ n then s.seq n else 0| else 0s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this✝:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).convergesthis:(s.from N).abs.convergesn:ℤhnm:n ≥ s.mhn:¬n ≥ N⊢ (if s.m + ↑k ≤ n then |s.seq n| else 0) = if N ≤ n then |if N ≤ n then s.seq n else 0| else 0 s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this✝:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).convergesthis:(s.from N).abs.convergesn:ℤhnm:n ≥ s.mhn:n ≥ N⊢ (if s.m + ↑k ≤ n then |s.seq n| else 0) = if N ≤ n then |if N ≤ n then s.seq n else 0| else 0s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this✝:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).convergesthis:(s.from N).abs.convergesn:ℤhnm:n ≥ s.mhn:¬n ≥ N⊢ (if s.m + ↑k ≤ n then |s.seq n| else 0) = if N ≤ n then |if N ≤ n then s.seq n else 0| else 0 s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this✝:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).convergesthis:(s.from N).abs.convergesn:ℤhnm:n ≥ s.mhn:¬n ≥ N⊢ s.m + ↑k ≤ n → s.seq n = 0 s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this✝:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).convergesthis:(s.from N).abs.convergesn:ℤhnm:n ≥ s.mhn:n ≥ N⊢ n < s.m + ↑k → 0 = |s.seq n|s:Seriesα':EReal := limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + εN':ℤhN:∀ b ≥ N', ↑(|s.seq b| ^ (1 / ↑b)) < ↑(α + ε)N:ℤ := max N' (max s.m 1)this✝:∀ n ≥ N, |s.seq n| ≤ (α + ε) ^ nk:ℕ := (N - s.m).toNathNk:N = s.m + ↑khgeom:({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.from
({ m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ (α + ε) ^ n) n.toNat else 0, vanish := ⋯ }.m + ↑N.toNat)).convergesthis:(s.from N).abs.convergesn:ℤhnm:n ≥ s.mhn:¬n ≥ N⊢ s.m + ↑k ≤ n → s.seq n = 0 All goals completed! 🐙Theorem 7.5.1(b) (Root test)
theorem Series.root_test_neg {s : Series}
(h : atTop.limsup (fun n ↦ ((|s.seq n|^(1/(n:ℝ)):ℝ):EReal)) > 1) : s.diverges := s:Seriesh:limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTop > 1⊢ s.diverges
-- This proof is written to follow the structure of the original text.
apply frequently_lt_of_lt_limsup (s:Seriesh:limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTop > 1⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ ↑(|s.seq n| ^ (1 / ↑n)) All goals completed! 🐙) at h
s:Seriesh:∃ᶠ (x : ℤ) in atTop, 1 < ↑(|s.seq x| ^ (1 / ↑x))⊢ ¬Tendsto s.seq atTop (nhds 0)
s:Seriesh:∃ᶠ (x : ℤ) in atTop, 1 < ↑(|s.seq x| ^ (1 / ↑x))this:Tendsto s.seq atTop (nhds 0)⊢ False; s:Seriesh:∃ᶠ (x : ℤ) in atTop, 1 < ↑(|s.seq x| ^ (1 / ↑x))this:∀ ε > 0, ∀ᶠ (b : ℤ) in atTop, |s.seq b - 0| < ε⊢ False; specialize this 1 (s:Seriesh:∃ᶠ (x : ℤ) in atTop, 1 < ↑(|s.seq x| ^ (1 / ↑x))this:∀ ε > 0, ∀ᶠ (b : ℤ) in atTop, |s.seq b - 0| < ε⊢ 1 > 0 All goals completed! 🐙)
s:Seriesh:∃ᶠ (x : ℤ) in atTop, 1 < ↑(|s.seq x| ^ (1 / ↑x))this:∀ᶠ (b : ℤ) in atTop, |s.seq b - 0| < 1n:ℤhn:1 ≤ nhs:1 < ↑(|s.seq n| ^ (1 / ↑n))hs':|s.seq n - 0| < 1⊢ False
s:Seriesh:∃ᶠ (x : ℤ) in atTop, 1 < ↑(|s.seq x| ^ (1 / ↑x))this:∀ᶠ (b : ℤ) in atTop, |s.seq b - 0| < 1n:ℤhn:1 ≤ nhs:1 < ↑(|s.seq n| ^ (1 / ↑n))hs':|s.seq n| < 1⊢ False; s:Seriesh:∃ᶠ (x : ℤ) in atTop, 1 < ↑(|s.seq x| ^ (1 / ↑x))this:∀ᶠ (b : ℤ) in atTop, |s.seq b - 0| < 1n:ℤhn:1 ≤ nhs:1 < ↑(|s.seq n| ^ (1 / ↑n))hs':|s.seq n| ^ (1 / ↑n) < 1⊢ Falses:Seriesh:∃ᶠ (x : ℤ) in atTop, 1 < ↑(|s.seq x| ^ (1 / ↑x))this:∀ᶠ (b : ℤ) in atTop, |s.seq b - 0| < 1n:ℤhn:1 ≤ nhs:1 < ↑(|s.seq n| ^ (1 / ↑n))hs':|s.seq n| < 1⊢ 0 ≤ |s.seq n|s:Seriesh:∃ᶠ (x : ℤ) in atTop, 1 < ↑(|s.seq x| ^ (1 / ↑x))this:∀ᶠ (b : ℤ) in atTop, |s.seq b - 0| < 1n:ℤhn:1 ≤ nhs:1 < ↑(|s.seq n| ^ (1 / ↑n))hs':|s.seq n| < 1⊢ 0 < 1 / ↑n s:Seriesh:∃ᶠ (x : ℤ) in atTop, 1 < ↑(|s.seq x| ^ (1 / ↑x))this:∀ᶠ (b : ℤ) in atTop, |s.seq b - 0| < 1n:ℤhn:1 ≤ nhs:1 < ↑(|s.seq n| ^ (1 / ↑n))hs':|s.seq n| ^ (1 / ↑n) < 1⊢ Falses:Seriesh:∃ᶠ (x : ℤ) in atTop, 1 < ↑(|s.seq x| ^ (1 / ↑x))this:∀ᶠ (b : ℤ) in atTop, |s.seq b - 0| < 1n:ℤhn:1 ≤ nhs:1 < ↑(|s.seq n| ^ (1 / ↑n))hs':|s.seq n| < 1⊢ 0 ≤ |s.seq n|s:Seriesh:∃ᶠ (x : ℤ) in atTop, 1 < ↑(|s.seq x| ^ (1 / ↑x))this:∀ᶠ (b : ℤ) in atTop, |s.seq b - 0| < 1n:ℤhn:1 ≤ nhs:1 < ↑(|s.seq n| ^ (1 / ↑n))hs':|s.seq n| < 1⊢ 0 < 1 / ↑n try All goals completed! 🐙
s:Seriesh:∃ᶠ (x : ℤ) in atTop, 1 < ↑(|s.seq x| ^ (1 / ↑x))this:∀ᶠ (b : ℤ) in atTop, |s.seq b - 0| < 1n:ℤhn:1 ≤ nhs:1 < |s.seq n| ^ (1 / ↑n)hs':|s.seq n| ^ (1 / ↑n) < 1⊢ False
All goals completed! 🐙Theorem 7.5.1(c) (Root test) / Exercise 7.5.3
theorem Series.root_test_inconclusive: ∃ s:Series,
atTop.Tendsto (fun n ↦ |s.seq n|^(1/(n:ℝ))) (nhds 1) ∧ s.diverges := ⊢ ∃ s, Tendsto (fun n ↦ |s.seq n| ^ (1 / ↑n)) atTop (nhds 1) ∧ s.diverges
All goals completed! 🐙Theorem 7.5.1 (Root test) / Exercise 7.5.3
theorem Series.root_test_inconclusive' : ∃ s:Series,
atTop.Tendsto (fun n ↦ |s.seq n|^(1/(n:ℝ))) (nhds 1) ∧ s.absConverges := ⊢ ∃ s, Tendsto (fun n ↦ |s.seq n| ^ (1 / ↑n)) atTop (nhds 1) ∧ s.absConverges
All goals completed! 🐙Lemma 7.5.2 / Exercise 7.5.1
theorem Series.ratio_ineq {c:ℤ → ℝ} (m:ℤ) (hpos: ∀ n ≥ m, c n > 0) :
atTop.liminf (fun n ↦ ((c (n+1) / c n:ℝ):EReal)) ≤
atTop.liminf (fun n ↦ ↑((c n)^(1/(n:ℝ)):ℝ))
∧ atTop.liminf (fun n ↦ (((c n)^(1/(n:ℝ)):ℝ):EReal)) ≤
atTop.limsup (fun n ↦ ↑((c n)^(1/(n:ℝ)):ℝ))
∧ atTop.limsup (fun n ↦ (((c n)^(1/(n:ℝ)):ℝ):EReal)) ≤
atTop.limsup (fun n ↦ ↑(c (n+1) / c n:ℝ))
:= c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ liminf (fun n ↦ ↑(c (n + 1) / c n)) atTop ≤ liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c (n + 1) / c n)) atTop
-- This proof is written to follow the structure of the original text.
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ liminf (fun n ↦ ↑(c (n + 1) / c n)) atTop ≤ liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTopc:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ ↑(c n ^ (1 / ↑n))c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) atTop fun n ↦ ↑(c n ^ (1 / ↑n))c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c (n + 1) / c n)) atTop c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ liminf (fun n ↦ ↑(c (n + 1) / c n)) atTop ≤ liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTopc:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ ↑(c n ^ (1 / ↑n))c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) atTop fun n ↦ ↑(c n ^ (1 / ↑n))c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c (n + 1) / c n)) atTop try c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c (n + 1) / c n)) atTop
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ liminf (fun n ↦ ↑(c (n + 1) / c n)) atTop ≤ liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop All goals completed! 🐙
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTop⊢ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ L'
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:L' = ⊤⊢ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ L'c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤⊢ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ L'; c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:L' = ⊤⊢ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ L' c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:L' = ⊤⊢ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ ⊤; All goals completed! 🐙
have hL'pos : 0 ≤ L' := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ liminf (fun n ↦ ↑(c (n + 1) / c n)) atTop ≤ liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c (n + 1) / c n)) atTop
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤⊢ ∃ᶠ (a : ℤ) in atTop, 0 ≤ ↑(c (a + 1) / c a)
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤⊢ ∀ (a : ℤ), ∃ b ≥ a, 0 ≤ ↑(c (b + 1) / c b)
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤N:ℤ⊢ ∃ b ≥ N, 0 ≤ ↑(c (b + 1) / c b); use max N m, c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤N:ℤ⊢ max N m ≥ N All goals completed! 🐙
have hpos1 := hpos (max N m) (c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤N:ℤ⊢ max N m ≥ m All goals completed! 🐙)
have hpos2 := hpos ((max N m)+1) (c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤N:ℤhpos1:c (max N m) > 0⊢ max N m + 1 ≥ m All goals completed! 🐙)
All goals completed! 🐙
have why : L' ≠ ⊥ := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ liminf (fun n ↦ ↑(c (n + 1) / c n)) atTop ≤ liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c (n + 1) / c n)) atTop All goals completed! 🐙
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toReal⊢ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ L'
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑L⊢ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ L'
have hLpos : 0 ≤ L := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ liminf (fun n ↦ ↑(c (n + 1) / c n)) atTop ≤ liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c (n + 1) / c n)) atTop c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤why:L' ≠ ⊥L:ℝ := L'.toRealhL'pos:0 ≤ ↑LhL':L' = ↑L⊢ 0 ≤ L; All goals completed! 🐙
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ L⊢ ∀ (a : EReal), L' < a → limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ a
intro y c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L' < y⊢ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ y
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L' < yhy':y = ⊤⊢ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ yc:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L' < yhy':¬y = ⊤⊢ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ y; c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L' < yhy':y = ⊤⊢ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ y c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L' < yhy':y = ⊤⊢ limsup (fun n ↦ ↑(c n ^ (↑n)⁻¹)) atTop ≤ ⊤; All goals completed! 🐙
have : y = y.toReal := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ liminf (fun n ↦ ↑(c (n + 1) / c n)) atTop ≤ liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c (n + 1) / c n)) atTop c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L' < yhy':¬y = ⊤⊢ ↑y.toReal = y; c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L' < yhy':¬y = ⊤⊢ y ≠ ⊥; c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy':¬y = ⊤hy:y = ⊥⊢ y ≤ L'; All goals completed! 🐙
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤this:y = ↑y.toReal⊢ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ y
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤this:y = ↑y.toRealε:ℝ := y.toReal - L⊢ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ y
have hε : 0 < ε := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ liminf (fun n ↦ ↑(c (n + 1) / c n)) atTop ≤ liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c (n + 1) / c n)) atTop All goals completed! 🐙
replace this : y = (L+ε:ℝ) := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ liminf (fun n ↦ ↑(c (n + 1) / c n)) atTop ≤ liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c (n + 1) / c n)) atTop c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤this:y = ↑y.toRealε:ℝ := y.toReal - Lhε:0 < ε⊢ L + ε = y.toReal; All goals completed! 🐙
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis:y = ↑(L + ε)⊢ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ ↑(L + ε)
have hε' : L' < (L+ε:ℝ) := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ liminf (fun n ↦ ↑(c (n + 1) / c n)) atTop ≤ liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c (n + 1) / c n)) atTop c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis:y = ↑(L + ε)⊢ L < L + ε; All goals completed! 🐙
have := eventually_lt_of_limsup_lt hε' (c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis:y = ↑(L + ε)hε':L' < ↑(L + ε)⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ ↑(c (n + 1) / c n) All goals completed! 🐙)
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)this:∃ a, ∀ b ≥ a, ↑(c (b + 1) / c b) < ↑(L + ε)⊢ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ ↑(L + ε); c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)⊢ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ ↑(L + ε)
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)⊢ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ ↑(L + ε)
have (n:ℤ) (hn: n ≥ N) : c (n+1) / c n ≤ (L + ε) := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ liminf (fun n ↦ ↑(c (n + 1) / c n)) atTop ≤ liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c (n + 1) / c n)) atTop
have : n ≥ N' := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ liminf (fun n ↦ ↑(c (n + 1) / c n)) atTop ≤ liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c (n + 1) / c n)) atTop All goals completed! 🐙
have npos : 0 < n := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ liminf (fun n ↦ ↑(c (n + 1) / c n)) atTop ≤ liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c (n + 1) / c n)) atTop All goals completed! 🐙
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤN:ℤ := max N' (max m 1)n:ℤhn:n ≥ Nthis:n ≥ N'npos:0 < nhN:↑(c (n + 1) / c n) < ↑(L + ε)⊢ c (n + 1) / c n ≤ L + ε; c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤN:ℤ := max N' (max m 1)n:ℤhn:n ≥ Nthis:n ≥ N'npos:0 < nhN:c (n + 1) / c n < L + ε⊢ c (n + 1) / c n ≤ L + ε; All goals completed! 🐙
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)⊢ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ ↑(L + ε)
have hA : 0 < A := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ liminf (fun n ↦ ↑(c (n + 1) / c n)) atTop ≤ liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c (n + 1) / c n)) atTop specialize hpos N (c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)⊢ N ≥ m All goals completed! 🐙); All goals completed! 🐙
have why2 (n:ℤ) (hn: n ≥ N) : c n ≤ A * (L+ε)^n := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ liminf (fun n ↦ ↑(c (n + 1) / c n)) atTop ≤ liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c (n + 1) / c n)) atTop
All goals completed! 🐙
have why2_root (n:ℤ) (hn: n ≥ N) : (((c n)^(1/(n:ℝ)):ℝ):EReal) ≤ (A^(1/(n:ℝ)) * (L+ε):ℝ) := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ liminf (fun n ↦ ↑(c (n + 1) / c n)) atTop ≤ liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c (n + 1) / c n)) atTop
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nn:ℤhn:n ≥ N⊢ c n ^ (1 / ↑n) ≤ A ^ (1 / ↑n) * (L + ε)
have hn' : n > 0 := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ liminf (fun n ↦ ↑(c (n + 1) / c n)) atTop ≤ liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
liminf (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ∧
limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(c (n + 1) / c n)) atTop All goals completed! 🐙
calc
_ ≤ (A * (L+ε)^n)^(1/(n:ℝ)) := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nn:ℤhn:n ≥ Nhn':n > 0⊢ c n ^ (1 / ↑n) ≤ (A * (L + ε) ^ n) ^ (1 / ↑n)
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nn:ℤhn:n ≥ Nhn':n > 0⊢ n ≥ mc:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nn:ℤhn:n ≥ Nhn':n > 0⊢ 0 ≤ 1 / ↑n; c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nn:ℤhn:n ≥ Nhn':n > 0⊢ 0 ≤ 1 / ↑n; All goals completed! 🐙
_ = A^(1/(n:ℝ)) * ((L+ε)^n)^(1/(n:ℝ)) := mul_rpow (c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nn:ℤhn:n ≥ Nhn':n > 0⊢ 0 ≤ A All goals completed! 🐙) (c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nn:ℤhn:n ≥ Nhn':n > 0⊢ 0 ≤ (L + ε) ^ n All goals completed! 🐙)
_ = _ := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nn:ℤhn:n ≥ Nhn':n > 0⊢ A ^ (1 / ↑n) * ((L + ε) ^ n) ^ (1 / ↑n) = A ^ (1 / ↑n) * (L + ε)
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nn:ℤhn:n ≥ Nhn':n > 0⊢ ((L + ε) ^ n) ^ (1 / ↑n) = L + ε
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nn:ℤhn:n ≥ Nhn':n > 0⊢ (L + ε) ^ (↑n * (1 / ↑n)) = L + ε
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nn:ℤhn:n ≥ Nhn':n > 0⊢ ↑n * (1 / ↑n) = 1
All goals completed! 🐙
calc
_ ≤ atTop.limsup (fun n:ℤ ↦ ((A^(1/(n:ℝ)) * (L+ε):ℝ):EReal)) := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ limsup (fun n ↦ ↑(c n ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(A ^ (1 / ↑n) * (L + ε))) atTop
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ (fun n ↦ ↑(c n ^ (1 / ↑n))) ≤ᶠ[atTop] fun n ↦ ↑(A ^ (1 / ↑n) * (L + ε))c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ autoParam (IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ ↑(c n ^ (1 / ↑n))) limsup_le_limsup._auto_1c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ autoParam (IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ ↑(A ^ (1 / ↑n) * (L + ε))) limsup_le_limsup._auto_3 c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ (fun n ↦ ↑(c n ^ (1 / ↑n))) ≤ᶠ[atTop] fun n ↦ ↑(A ^ (1 / ↑n) * (L + ε))c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ autoParam (IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ ↑(c n ^ (1 / ↑n))) limsup_le_limsup._auto_1c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ autoParam (IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ ↑(A ^ (1 / ↑n) * (L + ε))) limsup_le_limsup._auto_3 try All goals completed! 🐙
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ ∀ᶠ (x : ℤ) in atTop, (fun n ↦ ↑(c n ^ (1 / ↑n))) x ≤ (fun n ↦ ↑(A ^ (1 / ↑n) * (L + ε))) x; c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ ∃ a, ∀ b ≥ a, (fun n ↦ ↑(c n ^ (1 / ↑n))) b ≤ (fun n ↦ ↑(A ^ (1 / ↑n) * (L + ε))) b
All goals completed! 🐙
_ ≤ (atTop.limsup (fun n:ℤ ↦ ((A^(1/(n:ℝ)):ℝ):EReal))) * (atTop.limsup (fun n:ℤ ↦ ((L+ε:ℝ):EReal))) := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ limsup (fun n ↦ ↑(A ^ (1 / ↑n) * (L + ε))) atTop ≤
limsup (fun n ↦ ↑(A ^ (1 / ↑n))) atTop * limsup (fun n ↦ ↑(L + ε)) atTop
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))n:ℤ⊢ ↑(A ^ (1 / ↑n) * (L + ε)) = ((fun n ↦ ↑(A ^ (1 / ↑n))) * fun n ↦ ↑(L + ε)) nc:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ ∃ᶠ (x : ℤ) in atTop, 0 ≤ ↑(A ^ (1 / ↑x))c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ 0 ≤ᶠ[atTop] fun n ↦ ↑(L + ε)c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ limsup (fun n ↦ ↑(A ^ (1 / ↑n))) atTop ≠ 0 ∨ limsup (fun n ↦ ↑(L + ε)) atTop ≠ ⊤c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ limsup (fun n ↦ ↑(A ^ (1 / ↑n))) atTop ≠ ⊤ ∨ limsup (fun n ↦ ↑(L + ε)) atTop ≠ 0
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))n:ℤ⊢ ↑(A ^ (1 / ↑n) * (L + ε)) = ((fun n ↦ ↑(A ^ (1 / ↑n))) * fun n ↦ ↑(L + ε)) n All goals completed! 🐙
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ ∃ᶠ (x : ℤ) in atTop, 0 ≤ ↑(A ^ (1 / ↑x)) c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ ∀ (x : ℤ), 0 ≤ ↑(A ^ (1 / ↑x)); c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))x✝:ℤ⊢ 0 ≤ ↑(A ^ (1 / ↑x✝)); All goals completed! 🐙
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ 0 ≤ᶠ[atTop] fun n ↦ ↑(L + ε) c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ ∀ (x : ℤ), 0 x ≤ (fun n ↦ ↑(L + ε)) x; c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ 0 ≤ ↑L + ↑ε; All goals completed! 🐙
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ limsup (fun n ↦ ↑(A ^ (1 / ↑n))) atTop ≠ 0 ∨ limsup (fun n ↦ ↑(L + ε)) atTop ≠ ⊤ All goals completed! 🐙
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ ¬limsup (fun n ↦ ↑(A ^ (↑n)⁻¹)) atTop = ⊤ ∨ ¬L + ε = 0; All goals completed! 🐙
_ = (L+ε:ℝ) := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ limsup (fun n ↦ ↑(A ^ (1 / ↑n))) atTop * limsup (fun n ↦ ↑(L + ε)) atTop = ↑(L + ε)
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ limsup (fun n ↦ ↑(A ^ (↑n)⁻¹)) atTop * (↑L + ↑ε) = ↑L + ↑ε; c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ limsup (fun n ↦ ↑(A ^ (↑n)⁻¹)) atTop = 1
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ Tendsto (fun n ↦ ↑(A ^ (↑n)⁻¹)) atTop (nhds 1)
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ Tendsto (fun x ↦ ↑x) (nhds 1) (nhds 1)c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ Tendsto (fun n ↦ A ^ (↑n)⁻¹) atTop (nhds 1)
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ Tendsto (fun x ↦ ↑x) (nhds 1) (nhds 1) c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ ↑1 = 1; All goals completed! 🐙
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ Tendsto (fun x ↦ A ^ x) (nhds 0) (nhds 1)c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ Tendsto (fun n ↦ (↑n)⁻¹) atTop (nhds 0)
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ Tendsto (fun x ↦ A ^ x) (nhds 0) (nhds 1) apply (continuous_const_rpow (c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := limsup (fun n ↦ ↑(c (n + 1) / c n)) atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤ε:ℝ := y.toReal - Lhε:0 < εthis✝:y = ↑(L + ε)hε':L' < ↑(L + ε)N':ℤhN:∀ b ≥ N', ↑(c (b + 1) / c b) < ↑(L + ε)N:ℤ := max N' (max m 1)this:∀ n ≥ N, c (n + 1) / c n ≤ L + εA:ℝ := c N * (L + ε) ^ (-N)hA:0 < Awhy2:∀ n ≥ N, c n ≤ A * (L + ε) ^ nwhy2_root:∀ n ≥ N, ↑(c n ^ (1 / ↑n)) ≤ ↑(A ^ (1 / ↑n) * (L + ε))⊢ A ≠ 0 All goals completed! 🐙)).tendsto'; All goals completed! 🐙
All goals completed! 🐙Corollary 7.5.3 (Ratio test)
theorem Series.ratio_test_pos {s : Series} (hnon: ∀ n ≥ s.m, s.seq n ≠ 0)
(h : atTop.limsup (fun n ↦ ((|s.seq (n+1)| / |s.seq n|:ℝ):EReal)) < 1) : s.absConverges := s:Serieshnon:∀ n ≥ s.m, s.seq n ≠ 0h:limsup (fun n ↦ ↑(|s.seq (n + 1)| / |s.seq n|)) atTop < 1⊢ s.absConverges
s:Serieshnon:∀ n ≥ s.m, s.seq n ≠ 0h:limsup (fun n ↦ ↑(|s.seq (n + 1)| / |s.seq n|)) atTop < 1⊢ limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTop ≤ limsup (fun n ↦ ↑(|s.seq (n + 1)| / |s.seq n|)) atTop
s:Serieshnon:∀ n ≥ s.m, s.seq n ≠ 0h:limsup (fun n ↦ ↑(|s.seq (n + 1)| / |s.seq n|)) atTop < 1⊢ ∀ n ≥ s.m, |s.seq n| > 0
s:Serieshnon:∀ n ≥ s.m, s.seq n ≠ 0h:limsup (fun n ↦ ↑(|s.seq (n + 1)| / |s.seq n|)) atTop < 1n:ℤ⊢ n ≥ s.m → |s.seq n| > 0 ↔ n ≥ s.m → s.seq n ≠ 0
All goals completed! 🐙Corollary 7.5.3 (Ratio test)
theorem Series.ratio_test_neg {s : Series} (hnon: ∀ n ≥ s.m, s.seq n ≠ 0)
(h : atTop.liminf (fun n ↦ ((|s.seq (n+1)| / |s.seq n|:ℝ):EReal)) > 1) : s.diverges := s:Serieshnon:∀ n ≥ s.m, s.seq n ≠ 0h:liminf (fun n ↦ ↑(|s.seq (n + 1)| / |s.seq n|)) atTop > 1⊢ s.diverges
s:Serieshnon:∀ n ≥ s.m, s.seq n ≠ 0h:liminf (fun n ↦ ↑(|s.seq (n + 1)| / |s.seq n|)) atTop > 1⊢ liminf (fun n ↦ ↑(|s.seq (n + 1)| / |s.seq n|)) atTop ≤ limsup (fun n ↦ ↑(|s.seq n| ^ (1 / ↑n))) atTop
s:Serieshnon:∀ n ≥ s.m, s.seq n ≠ 0h:liminf (fun n ↦ ↑(|s.seq (n + 1)| / |s.seq n|)) atTop > 1n:ℤ⊢ |s.seq (n + 1)| = |s.seq (n + 1)|s:Serieshnon:∀ n ≥ s.m, s.seq n ≠ 0h:liminf (fun n ↦ ↑(|s.seq (n + 1)| / |s.seq n|)) atTop > 1⊢ ∀ n ≥ s.m, |s.seq n| > 0s:Serieshnon:∀ n ≥ s.m, s.seq n ≠ 0h:liminf (fun n ↦ ↑(|s.seq (n + 1)| / |s.seq n|)) atTop > 1⊢ ∀ n ≥ s.m, |s.seq n| > 0; s:Serieshnon:∀ n ≥ s.m, s.seq n ≠ 0h:liminf (fun n ↦ ↑(|s.seq (n + 1)| / |s.seq n|)) atTop > 1⊢ ∀ n ≥ s.m, |s.seq n| > 0s:Serieshnon:∀ n ≥ s.m, s.seq n ≠ 0h:liminf (fun n ↦ ↑(|s.seq (n + 1)| / |s.seq n|)) atTop > 1⊢ ∀ n ≥ s.m, |s.seq n| > 0
all_goals s:Serieshnon:∀ n ≥ s.m, s.seq n ≠ 0h:liminf (fun n ↦ ↑(|s.seq (n + 1)| / |s.seq n|)) atTop > 1n:ℤ⊢ n ≥ s.m → |s.seq n| > 0 ↔ n ≥ s.m → s.seq n ≠ 0; All goals completed! 🐙Corollary 7.5.3 (Ratio test) / Exercise 7.5.3
theorem Series.ratio_test_inconclusive: ∃ s:Series, (∀ n ≥ s.m, s.seq n ≠ 0) ∧
atTop.Tendsto (fun n ↦ |s.seq (n+1)| / |s.seq n|) (nhds 1) ∧ s.diverges := ⊢ ∃ s, (∀ n ≥ s.m, s.seq n ≠ 0) ∧ Tendsto (fun n ↦ |s.seq (n + 1)| / |s.seq n|) atTop (nhds 1) ∧ s.diverges
All goals completed! 🐙Corollary 7.5.3 (Ratio test) / Exercise 7.5.3
theorem Series.ratio_test_inconclusive' : ∃ s:Series, (∀ n ≥ s.m, s.seq n ≠ 0) ∧
atTop.Tendsto (fun n ↦ |s.seq (n+1)| / |s.seq n|) (nhds 1) ∧ s.absConverges := ⊢ ∃ s, (∀ n ≥ s.m, s.seq n ≠ 0) ∧ Tendsto (fun n ↦ |s.seq (n + 1)| / |s.seq n|) atTop (nhds 1) ∧ s.absConverges
All goals completed! 🐙Proposition 7.5.4
theorem Series.root_self_converges : atTop.Tendsto (fun (n:ℕ) ↦ (n:ℝ)^(1 / (n:ℝ))) (nhds 1) := ⊢ Tendsto (fun n ↦ ↑n ^ (1 / ↑n)) atTop (nhds 1)
All goals completed! 🐙Exercise 7.5.2
theorem Series.poly_mul_geom_converges {x:ℝ} (hx: |x|<1) (q:ℝ) : (fun n:ℕ ↦ (n:ℝ)^q * x^n : Series).converges
∧ atTop.Tendsto (fun n:ℕ ↦ (n:ℝ)^q * x^n) (nhds 0) := x:ℝhx:|x| < 1q:ℝ⊢ { m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ ↑n ^ q * x ^ n) n.toNat else 0, vanish := ⋯ }.converges ∧
Tendsto (fun n ↦ ↑n ^ q * x ^ n) atTop (nhds 0)
All goals completed! 🐙end Chapter7