Аналіз I, Глава 7.5
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 Chapter7
Теорема 7.5.1(a) (Root test). A technical condition hbound is needed to ensure the limsup is finite.
theorem Series.root_test_pos {s : Series}
(h : Filter.limsup (fun n ↦ ((|s.seq n|^(1/(n:ℝ)):ℝ):EReal)) Filter.atTop < 1) : s.absConverges := s:Seriesh:Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTop < 1⊢ s.absConverges
-- This proof is written to follow the structure of the original text.
s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atToph:α' < 1⊢ s.absConverges
have hpos : 0 ≤ α' := s:Seriesh:Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTop < 1⊢ s.absConverges
apply Filter.le_limsup_of_frequently_le _ (s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atToph:α' < 1⊢ Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) Filter.atTop fun n => ↑(|s.seq n| ^ (1 / ↑n)) All goals completed! 🐙)
s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atToph:α' < 1⊢ ∀ (x : ℤ), 0 ≤ ↑(|s.seq x| ^ (1 / ↑x))
s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atToph:α' < 1x✝:ℤ⊢ 0 ≤ ↑(|s.seq x✝| ^ (1 / ↑x✝)); All goals completed! 🐙
s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atToph:α' < 1hpos:0 ≤ α'α:ℝ := α'.toReal⊢ s.absConverges
have hαα' : α' = α := s:Seriesh:Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTop < 1⊢ s.absConverges
s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atToph:α' < 1hpos:0 ≤ α'α:ℝ := α'.toReal⊢ α' ≠ ⊤s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atToph:α' < 1hpos:0 ≤ α'α:ℝ := α'.toReal⊢ α' ≠ ⊥
s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atToph:α' < 1hpos:0 ≤ α'α:ℝ := α'.toReal⊢ α' ≠ ⊤ s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTophpos:0 ≤ α'α:ℝ := α'.toRealh:α' = ⊤⊢ 1 ≤ α'; All goals completed! 🐙
s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atToph:α' < 1α:ℝ := α'.toRealhpos:α' = ⊥⊢ α' < 0; All goals completed! 🐙
s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTopα:ℝ := α'.toRealhpos:0 ≤ ↑αh:↑α < 1hαα':α' = ↑α⊢ s.absConverges; s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ α⊢ s.absConverges
s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2⊢ s.absConverges
have hε : 0 < ε := s:Seriesh:Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTop < 1⊢ s.absConverges s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2⊢ α < 1; All goals completed! 🐙
have hε' : α' < (α+ε:ℝ) := s:Seriesh:Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTop < 1⊢ s.absConverges s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < ε⊢ α < α + ε; All goals completed! 🐙
have hα : α + ε < 1 := s:Seriesh:Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTop < 1⊢ s.absConverges s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)⊢ α + (1 - α) / 2 < 1; All goals completed! 🐙
have hα' : 0 < α + ε := s:Seriesh:Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTop < 1⊢ s.absConverges All goals completed! 🐙
have := Filter.eventually_lt_of_limsup_lt hε' (s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTopα:ℝ := α'.toRealhαα':α' = ↑αh:α < 1hpos:0 ≤ αε:ℝ := (1 - α) / 2hε:0 < εhε':α' < ↑(α + ε)hα:α + ε < 1hα':0 < α + ε⊢ Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) Filter.atTop fun n => ↑(|s.seq n| ^ (1 / ↑n)) All goals completed! 🐙)
s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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:Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTop < 1⊢ s.absConverges
have : n ≥ N' := s:Seriesh:Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTop < 1⊢ s.absConverges All goals completed! 🐙
have npos : 0 < n := s:Seriesh:Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTop < 1⊢ s.absConverges All goals completed! 🐙
s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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! 🐙) hN n.toNat
all_goals s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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:Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTop < 1⊢ s.absConverges All goals completed! 🐙
have hgeom : (fun n ↦ (α+ε) ^ n : Series).converges := s:Seriesh:Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTop < 1⊢ s.absConverges
All goals completed! 🐙
s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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:Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTop < 1⊢ s.absConverges
s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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! 🐙
s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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:Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTop < 1⊢ s.absConverges All goals completed! 🐙
s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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
s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 Ns:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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⊢ (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
s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 All goals completed! 🐙
s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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
all_goals s:Seriesα':EReal := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 := Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.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 ≥ Na✝:s.m + ↑k ≤ n⊢ s.seq n = 0; All goals completed! 🐙Теорема 7.5.1(b) (Root test)
theorem Series.root_test_neg {s : Series}
(h : Filter.limsup (fun n ↦ ((|s.seq n|^(1/(n:ℝ)):ℝ):EReal)) Filter.atTop > 1) : s.diverges := s:Seriesh:Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTop > 1⊢ s.diverges
-- This proof is written to follow the structure of the original text.
replace h := Filter.frequently_lt_of_lt_limsup (s:Seriesh:Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTop > 1⊢ Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) Filter.atTop fun n => ↑(|s.seq n| ^ (1 / ↑n)) All goals completed! 🐙) h
s:Seriesh:∃ᶠ (x : ℤ) in Filter.atTop, 1 < ↑(|s.seq x| ^ (1 / ↑x))⊢ ¬Filter.Tendsto s.seq Filter.atTop (nhds 0)
s:Seriesh:∃ᶠ (x : ℤ) in Filter.atTop, 1 < ↑(|s.seq x| ^ (1 / ↑x))this:Filter.Tendsto s.seq Filter.atTop (nhds 0)⊢ False
s:Seriesh:∃ᶠ (x : ℤ) in Filter.atTop, 1 < ↑(|s.seq x| ^ (1 / ↑x))this:∀ ε > 0, ∀ᶠ (b : ℤ) in Filter.atTop, |s.seq b - 0| < ε⊢ False
specialize this 1 (s:Seriesh:∃ᶠ (x : ℤ) in Filter.atTop, 1 < ↑(|s.seq x| ^ (1 / ↑x))this:∀ ε > 0, ∀ᶠ (b : ℤ) in Filter.atTop, |s.seq b - 0| < ε⊢ 1 > 0 All goals completed! 🐙)
s:Seriesh:∃ᶠ (x : ℤ) in Filter.atTop, 1 < ↑(|s.seq x| ^ (1 / ↑x))this:∀ᶠ (b : ℤ) in Filter.atTop, |s.seq b - 0| < 1n:ℤhn:n ≥ 1hs:1 < ↑(|s.seq n| ^ (1 / ↑n))hs':|s.seq n - 0| < 1⊢ False
s:Seriesh:∃ᶠ (x : ℤ) in Filter.atTop, 1 < ↑(|s.seq x| ^ (1 / ↑x))this:∀ᶠ (b : ℤ) in Filter.atTop, |s.seq b - 0| < 1n:ℤhn:n ≥ 1hs:1 < ↑(|s.seq n| ^ (1 / ↑n))hs':|s.seq n| < 1⊢ False
replace hs' := Real.rpow_lt_one (s:Seriesh:∃ᶠ (x : ℤ) in Filter.atTop, 1 < ↑(|s.seq x| ^ (1 / ↑x))this:∀ᶠ (b : ℤ) in Filter.atTop, |s.seq b - 0| < 1n:ℤhn:n ≥ 1hs:1 < ↑(|s.seq n| ^ (1 / ↑n))hs':|s.seq n| < 1⊢ 0 ≤ |s.seq n| All goals completed! 🐙) hs' (show 0 < 1/(n:ℝ) s:Seriesh:Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTop > 1⊢ s.diverges All goals completed! 🐙)
s:Seriesh:∃ᶠ (x : ℤ) in Filter.atTop, 1 < ↑(|s.seq x| ^ (1 / ↑x))this:∀ᶠ (b : ℤ) in Filter.atTop, |s.seq b - 0| < 1n:ℤhn:n ≥ 1hs:1 < |s.seq n| ^ (1 / ↑n)hs':|s.seq n| ^ (1 / ↑n) < 1⊢ False
All goals completed! 🐙Теорема 7.5.1(c) (Root test) / Вправа 7.5.3
theorem Series.root_test_inconclusive: ∃ s:Series,
Filter.Tendsto (fun n ↦ |s.seq n|^(1/(n:ℝ))) Filter.atTop (nhds 1) ∧ s.diverges := ⊢ ∃ s, Filter.Tendsto (fun n => |s.seq n| ^ (1 / ↑n)) Filter.atTop (nhds 1) ∧ s.diverges
All goals completed! 🐙Теорема 7.5.1 (Root test) / Вправа 7.5.3
theorem Series.root_test_inconclusive' : ∃ s:Series,
Filter.Tendsto (fun n ↦ |s.seq n|^(1/(n:ℝ))) Filter.atTop (nhds 1) ∧ s.absConverges := ⊢ ∃ s, Filter.Tendsto (fun n => |s.seq n| ^ (1 / ↑n)) Filter.atTop (nhds 1) ∧ s.absConverges
All goals completed! 🐙Лема 7.5.2 / Вправа 7.5.1
theorem Series.ratio_ineq {c:ℤ → ℝ} (m:ℤ) (hpos: ∀ n ≥ m, c n > 0) :
Filter.liminf (fun n ↦ ((c (n+1) / c n:ℝ): EReal)) Filter.atTop ≤
Filter.liminf (fun n ↦ (((c n)^(1/(n:ℝ)):ℝ):EReal)) Filter.atTop
∧ Filter.liminf (fun n ↦ (((c n)^(1/(n:ℝ)):ℝ):EReal)) Filter.atTop ≤
Filter.limsup (fun n ↦ (((c n)^(1/(n:ℝ)):ℝ):EReal)) Filter.atTop
∧ Filter.limsup (fun n ↦ (((c n)^(1/(n:ℝ)):ℝ):EReal)) Filter.atTop ≤
Filter.limsup (fun n ↦ ((c (n+1) / c n:ℝ):EReal)) Filter.atTop
:= c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ Filter.liminf (fun n => ↑(c (n + 1) / c n)) Filter.atTop ≤ Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTop
-- This proof is written to follow the structure of the original text.
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ Filter.liminf (fun n => ↑(c (n + 1) / c n)) Filter.atTop ≤ Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTopc:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTopc:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTop
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ Filter.liminf (fun n => ↑(c (n + 1) / c n)) Filter.atTop ≤ Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop All goals completed! 🐙
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop apply Filter.liminf_le_limsup (c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) Filter.atTop fun n => ↑(c n ^ (1 / ↑n)) All goals completed! 🐙) (c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) Filter.atTop fun n => ↑(c n ^ (1 / ↑n)) All goals completed! 🐙)
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTop⊢ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ L'
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTophL:L' = ⊤⊢ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ L'c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTophL:¬L' = ⊤⊢ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ L'
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTophL:L' = ⊤⊢ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ L' All goals completed! 🐙
have hL'pos : 0 ≤ L' := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ Filter.liminf (fun n => ↑(c (n + 1) / c n)) Filter.atTop ≤ Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTop
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTophL:¬L' = ⊤⊢ ∃ᶠ (a : ℤ) in Filter.atTop, 0 ≤ ↑(c (a + 1) / c a)
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTophL:¬L' = ⊤⊢ ∀ (a : ℤ), ∃ b ≥ a, 0 ≤ ↑(c (b + 1) / c b)
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTophL:¬L' = ⊤N:ℤ⊢ ∃ b ≥ N, 0 ≤ ↑(c (b + 1) / c b)
use max N m, c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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⊢ Filter.liminf (fun n => ↑(c (n + 1) / c n)) Filter.atTop ≤ Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTop All goals completed! 🐙
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toReal⊢ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ L'
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑L⊢ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ L'
have hLpos : 0 ≤ L := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ Filter.liminf (fun n => ↑(c (n + 1) / c n)) Filter.atTop ≤ Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTop
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ L⊢ ∀ (a : EReal), L' < a → Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ a
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L' < y⊢ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ y
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L' < yhy':y = ⊤⊢ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ yc:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L' < yhy':¬y = ⊤⊢ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ y
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L' < yhy':y = ⊤⊢ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ y All goals completed! 🐙
have : y = y.toReal := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ Filter.liminf (fun n => ↑(c (n + 1) / c n)) Filter.atTop ≤ Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTop
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTophL:¬L' = ⊤hL'pos:0 ≤ L'why:L' ≠ ⊥L:ℝ := L'.toRealhL':L' = ↑LhLpos:0 ≤ Ly:ERealhy:L < y.toRealhy':¬y = ⊤this:y = ↑y.toReal⊢ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ y
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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⊢ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ y
have hε : 0 < ε := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ Filter.liminf (fun n => ↑(c (n + 1) / c n)) Filter.atTop ≤ Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTop c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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⊢ L < y.toReal; All goals completed! 🐙
replace this : y = (L+ε:ℝ) := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ Filter.liminf (fun n => ↑(c (n + 1) / c n)) Filter.atTop ≤ Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTop c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 + ε)⊢ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ ↑(L + ε)
have hε' : L' < (L+ε:ℝ) := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ Filter.liminf (fun n => ↑(c (n + 1) / c n)) Filter.atTop ≤ Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTop c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 := Filter.eventually_lt_of_limsup_lt hε' (c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 + ε)⊢ Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) Filter.atTop fun n => ↑(c (n + 1) / c n) All goals completed! 🐙)
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 + ε)⊢ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ ↑(L + ε)
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 + ε)⊢ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ ↑(L + ε)
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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)⊢ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ ↑(L + ε)
have (n:ℤ) (hn: n ≥ N) : c (n+1) / c n ≤ (L + ε) := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ Filter.liminf (fun n => ↑(c (n + 1) / c n)) Filter.atTop ≤ Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTop
have : n ≥ N' := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ Filter.liminf (fun n => ↑(c (n + 1) / c n)) Filter.atTop ≤ Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTop All goals completed! 🐙
have npos : 0 < n := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ Filter.liminf (fun n => ↑(c (n + 1) / c n)) Filter.atTop ≤ Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTop All goals completed! 🐙
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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)⊢ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ ↑(L + ε)
have hA : 0 < A := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0⊢ Filter.liminf (fun n => ↑(c (n + 1) / c n)) Filter.atTop ≤ Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTop
specialize hpos N (c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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⊢ Filter.liminf (fun n => ↑(c (n + 1) / c n)) Filter.atTop ≤ Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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⊢ Filter.liminf (fun n => ↑(c (n + 1) / c n)) Filter.atTop ≤ Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTop
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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⊢ Filter.liminf (fun n => ↑(c (n + 1) / c n)) Filter.atTop ≤ Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.liminf (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧
Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.atTop All goals completed! 🐙
calc
_ ≤ (A * (L+ε)^n)^(1/(n:ℝ)) := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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)
apply Real.rpow_le_rpow (le_of_lt (hpos n (c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 ≥ m All goals completed! 🐙)))
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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
have : n ≥ 0 := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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) All goals completed! 🐙
All goals completed! 🐙
_ = A^(1/(n:ℝ)) * ((L+ε)^n)^(1/(n:ℝ)) := Real.mul_rpow (c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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
_ ≤ Filter.limsup (fun n:ℤ ↦ ((A^(1/(n:ℝ)) * (L+ε):ℝ):EReal)) Filter.atTop := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 + ε))⊢ Filter.limsup (fun n => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤
Filter.limsup (fun n => ↑(A ^ (1 / ↑n) * (L + ε))) Filter.atTop
apply Filter.limsup_le_limsup _ (c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 + ε))⊢ Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) Filter.atTop fun n => ↑(c n ^ (1 / ↑n)) All goals completed! 🐙) (c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 + ε))⊢ Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) Filter.atTop fun n => ↑(A ^ (1 / ↑n) * (L + ε)) All goals completed! 🐙)
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 Filter.atTop, (fun n => ↑(c n ^ (1 / ↑n))) x ≤ (fun n => ↑(A ^ (1 / ↑n) * (L + ε))) x
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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! 🐙
_ ≤ (Filter.limsup (fun n:ℤ ↦ ((A^(1/(n:ℝ)):ℝ):EReal)) Filter.atTop) * (Filter.limsup (fun n:ℤ ↦ ((L+ε:ℝ):EReal)) Filter.atTop) := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 + ε))⊢ Filter.limsup (fun n => ↑(A ^ (1 / ↑n) * (L + ε))) Filter.atTop ≤
Filter.limsup (fun n => ↑(A ^ (1 / ↑n))) Filter.atTop * Filter.limsup (fun n => ↑(L + ε)) Filter.atTop
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 Filter.atTop, 0 ≤ ↑(A ^ (1 / ↑x))c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 ≤ᶠ[Filter.atTop] fun n => ↑(L + ε)c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 + ε))⊢ Filter.limsup (fun n => ↑(A ^ (1 / ↑n))) Filter.atTop ≠ 0 ∨ Filter.limsup (fun n => ↑(L + ε)) Filter.atTop ≠ ⊤c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 + ε))⊢ Filter.limsup (fun n => ↑(A ^ (1 / ↑n))) Filter.atTop ≠ ⊤ ∨ Filter.limsup (fun n => ↑(L + ε)) Filter.atTop ≠ 0
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 Filter.atTop, 0 ≤ ↑(A ^ (1 / ↑x)) c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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:ℤ⊢ 0 ≤ ↑(A ^ (1 / ↑n)); All goals completed! 🐙
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 ≤ᶠ[Filter.atTop] fun n => ↑(L + ε) c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 Filter.atTop, 0 x ≤ (fun n => ↑(L + ε)) x
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 + ε))⊢ Filter.limsup (fun n => ↑(A ^ (1 / ↑n))) Filter.atTop ≠ 0 ∨ Filter.limsup (fun n => ↑(L + ε)) Filter.atTop ≠ ⊤ All goals completed! 🐙
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 + ε))⊢ ¬Filter.limsup (fun n => ↑(A ^ (↑n)⁻¹)) Filter.atTop = ⊤ ∨ ¬L + ε = 0
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 + ε))⊢ ¬L + ε = 0; All goals completed! 🐙
_ = (L+ε:ℝ) := c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 + ε))⊢ Filter.limsup (fun n => ↑(A ^ (1 / ↑n))) Filter.atTop * Filter.limsup (fun n => ↑(L + ε)) Filter.atTop = ↑(L + ε)
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 + ε))⊢ Filter.limsup (fun n => ↑(A ^ (↑n)⁻¹)) Filter.atTop * (↑L + ↑ε) = ↑L + ↑ε
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 + ε))⊢ Filter.limsup (fun n => ↑(A ^ (↑n)⁻¹)) Filter.atTop = 1
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 + ε))⊢ Filter.Tendsto (fun n => ↑(A ^ (↑n)⁻¹)) Filter.atTop (nhds 1)
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 + ε))⊢ Filter.Tendsto (fun x => ↑x) (nhds 1) (nhds 1)c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 + ε))⊢ Filter.Tendsto (fun n => A ^ (↑n)⁻¹) Filter.atTop (nhds 1)
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 + ε))⊢ Filter.Tendsto (fun x => ↑x) (nhds 1) (nhds 1) apply Continuous.tendsto' continuous_coe_real_ereal _ _ (c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 + ε))⊢ Filter.Tendsto (fun x => A ^ x) (nhds 0) (nhds 1)c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 + ε))⊢ Filter.Tendsto (fun n => (↑n)⁻¹) Filter.atTop (nhds 0)
c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 + ε))⊢ Filter.Tendsto (fun x => A ^ x) (nhds 0) (nhds 1) apply Continuous.tendsto' (Real.continuous_const_rpow (c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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! 🐙)) _ _ (c:ℤ → ℝm:ℤhpos:∀ n ≥ m, c n > 0L':EReal := Filter.limsup (fun n => ↑(c (n + 1) / c n)) Filter.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 = 1 All goals completed! 🐙)
All goals completed! 🐙Наслідок 7.5.3 (Ratio test)
theorem Series.ratio_test_pos {s : Series} (hnon: ∀ n ≥ s.m, s.seq n ≠ 0)
(h : Filter.limsup (fun n ↦ ((|s.seq (n+1)| / |s.seq n|:ℝ):EReal)) Filter.atTop < 1) : s.absConverges := s:Serieshnon:∀ n ≥ s.m, s.seq n ≠ 0h:Filter.limsup (fun n => ↑(|s.seq (n + 1)| / |s.seq n|)) Filter.atTop < 1⊢ s.absConverges
s:Serieshnon:∀ n ≥ s.m, s.seq n ≠ 0h:Filter.limsup (fun n => ↑(|s.seq (n + 1)| / |s.seq n|)) Filter.atTop < 1⊢ Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTop ≤
Filter.limsup (fun n => ↑(|s.seq (n + 1)| / |s.seq n|)) Filter.atTop
s:Serieshnon:∀ n ≥ s.m, s.seq n ≠ 0h:Filter.limsup (fun n => ↑(|s.seq (n + 1)| / |s.seq n|)) Filter.atTop < 1⊢ ∀ n ≥ s.m, |s.seq n| > 0
s:Serieshnon:∀ n ≥ s.m, s.seq n ≠ 0h:Filter.limsup (fun n => ↑(|s.seq (n + 1)| / |s.seq n|)) Filter.atTop < 1n:ℤ⊢ n ≥ s.m → |s.seq n| > 0 ↔ n ≥ s.m → s.seq n ≠ 0
All goals completed! 🐙Наслідок 7.5.3 (Ratio test)
theorem Series.ratio_test_neg {s : Series} (hnon: ∀ n ≥ s.m, s.seq n ≠ 0)
(h : Filter.liminf (fun n ↦ ((|s.seq (n+1)| / |s.seq n|:ℝ):EReal)) Filter.atTop > 1) : s.diverges := s:Serieshnon:∀ n ≥ s.m, s.seq n ≠ 0h:Filter.liminf (fun n => ↑(|s.seq (n + 1)| / |s.seq n|)) Filter.atTop > 1⊢ s.diverges
s:Serieshnon:∀ n ≥ s.m, s.seq n ≠ 0h:Filter.liminf (fun n => ↑(|s.seq (n + 1)| / |s.seq n|)) Filter.atTop > 1⊢ Filter.liminf (fun n => ↑(|s.seq (n + 1)| / |s.seq n|)) Filter.atTop ≤
Filter.limsup (fun n => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTop
s:Serieshnon:∀ n ≥ s.m, s.seq n ≠ 0h:Filter.liminf (fun n => ↑(|s.seq (n + 1)| / |s.seq n|)) Filter.atTop > 1n:ℤ⊢ |s.seq (n + 1)| = |s.seq (n + 1)|s:Serieshnon:∀ n ≥ s.m, s.seq n ≠ 0h:Filter.liminf (fun n => ↑(|s.seq (n + 1)| / |s.seq n|)) Filter.atTop > 1⊢ ∀ n ≥ s.m, |s.seq n| > 0s:Serieshnon:∀ n ≥ s.m, s.seq n ≠ 0h:Filter.liminf (fun n => ↑(|s.seq (n + 1)| / |s.seq n|)) Filter.atTop > 1⊢ ∀ n ≥ s.m, |s.seq n| > 0
s:Serieshnon:∀ n ≥ s.m, s.seq n ≠ 0h:Filter.liminf (fun n => ↑(|s.seq (n + 1)| / |s.seq n|)) Filter.atTop > 1n:ℤ⊢ |s.seq (n + 1)| = |s.seq (n + 1)| All goals completed! 🐙
all_goals s:Serieshnon:∀ n ≥ s.m, s.seq n ≠ 0h:Filter.liminf (fun n => ↑(|s.seq (n + 1)| / |s.seq n|)) Filter.atTop > 1n:ℤ⊢ n ≥ s.m → |s.seq n| > 0 ↔ n ≥ s.m → s.seq n ≠ 0; All goals completed! 🐙Наслідок 7.5.3 (Ratio test) / Вправа 7.5.3
theorem Series.ratio_test_inconclusive: ∃ s:Series, (∀ n ≥ s.m, s.seq n ≠ 0) ∧
Filter.Tendsto (fun n ↦ |s.seq n+1| / |s.seq n|) Filter.atTop (nhds 1) ∧ s.diverges := ⊢ ∃ s, (∀ n ≥ s.m, s.seq n ≠ 0) ∧ Filter.Tendsto (fun n => |s.seq n + 1| / |s.seq n|) Filter.atTop (nhds 1) ∧ s.diverges
All goals completed! 🐙Наслідок 7.5.3 (Ratio test) / Вправа 7.5.3
theorem Series.ratio_test_inconclusive' : ∃ s:Series, (∀ n ≥ s.m, s.seq n ≠ 0) ∧
Filter.Tendsto (fun n ↦ |s.seq n+1| / |s.seq n|) Filter.atTop (nhds 1) ∧ s.absConverges := ⊢ ∃ s,
(∀ n ≥ s.m, s.seq n ≠ 0) ∧ Filter.Tendsto (fun n => |s.seq n + 1| / |s.seq n|) Filter.atTop (nhds 1) ∧ s.absConverges
All goals completed! 🐙Твердження 7.5.4
theorem Series.root_self_converges : (fun (n:ℕ) ↦ (n:ℝ)^(1 / n : ℝ) : Series).convergesTo 1 := ⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => ↑n ^ (1 / ↑n)) n.toNat else 0, vanish := ⋯ }.convergesTo 1
-- This proof is written to follow the structure of the original text.
All goals completed! 🐙Вправа 7.5.2
theorem Series.poly_mul_geom_converges {x:ℝ} (hx: |x|<1) (q:ℝ) : (fun n:ℕ ↦ (n:ℝ)^q * x^n : Series).converges ∧ Filter.Tendsto (fun n:ℕ ↦ (n:ℝ)^q * x^n) Filter.atTop (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 ∧
Filter.Tendsto (fun n => ↑n ^ q * x ^ n) Filter.atTop (nhds 0)
All goals completed! 🐙end Chapter7