Analysis I, Section 6.5: Some standard limits
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:
-
Some standard limits, including limits of sequences of the form 1/n^α, x^n, and x^(1/n).
namespace Chapter6theorem declaration uses `sorry`Sequence.lim_of_const (c:ℝ) : ((fun (_:ℕ) ↦ c):Sequence).TendsTo c := c:ℝ⊢ (↑fun x => c).TendsTo c All goals completed! 🐙instance Sequence.inst_pow: Pow Sequence ℕ where
pow a k := {
m := a.m
seq n := if n ≥ a.m then a n ^ k else 0
vanish := a:Sequencek:ℕ⊢ ∀ n < a.m, (if n ≥ a.m then a.seq n ^ k else 0) = 0 All goals completed! 🐙
}@[simp]
lemma Sequence.pow_eval {a:Sequence} {k: ℕ} {n: ℤ} (hn : n ≥ a.m): (a ^ k) n = a n ^ k := a:Sequencek:ℕn:ℤhn:n ≥ a.m⊢ (a ^ k).seq n = a.seq n ^ k
a:Sequencek:ℕn:ℤhn:n ≥ a.m⊢ ({
hPow := fun a b =>
{ pow := fun a k => { m := a.m, seq := fun n => if n ≥ a.m then a.seq n ^ k else 0, vanish := ⋯ } }.1 a
b }.1
a k).seq
n =
a.seq n ^ k
All goals completed! 🐙@[simp]
lemma Sequence.pow_one (a:Sequence) : a^1 = a := a:Sequence⊢ a ^ 1 = a
a:Sequence⊢ (a ^ 1).m = a.ma:Sequencen:ℤ⊢ (a ^ 1).seq n = a.seq n; a:Sequencen:ℤ⊢ (a ^ 1).seq n = a.seq n; a:Sequencen:ℤ⊢ (if n ≥ a.m then Monoid.npow 1 (a.seq n) else 0) = a.seq n; a:Sequencen:ℤh:n ≥ a.m⊢ Monoid.npow 1 (a.seq n) = a.seq na:Sequencen:ℤh:¬n ≥ a.m⊢ 0 = a.seq n; a:Sequencen:ℤh:¬n ≥ a.m⊢ 0 = a.seq n; All goals completed! 🐙lemma Sequence.pow_succ (a:Sequence) (k:ℕ): a^(k+1) = a^k * a := a:Sequencek:ℕ⊢ a ^ (k + 1) = a ^ k * a
a:Sequencek:ℕ⊢ (a ^ (k + 1)).m = (a ^ k * a).ma:Sequencek:ℕx:ℤ⊢ (a ^ (k + 1)).seq x = (a ^ k * a).seq x
a:Sequencek:ℕ⊢ (a ^ (k + 1)).m = (a ^ k * a).m a:Sequencek:ℕ⊢ (a ^ k * a).m = (a ^ (k + 1)).m; All goals completed! 🐙
a:Sequencek:ℕx:ℤ⊢ (a ^ (k + 1)).seq x = (a ^ k * a).seq x a:Sequencek:ℕx:ℤ⊢ (a ^ (k + 1)).seq x = (a ^ k).seq x * a.seq x
a:Sequencek:ℕx:ℤh:x ≥ a.m⊢ (a ^ (k + 1)).seq x = (a ^ k).seq x * a.seq xa:Sequencek:ℕx:ℤh:¬x ≥ a.m⊢ (a ^ (k + 1)).seq x = (a ^ k).seq x * a.seq x
a:Sequencek:ℕx:ℤh:x ≥ a.m⊢ (a ^ (k + 1)).seq x = (a ^ k).seq x * a.seq x a:Sequencek:ℕx:ℤh:x ≥ a.m⊢ a.seq x ^ (k + 1) = a.seq x ^ k * a.seq x
All goals completed! 🐙
a:Sequencek:ℕx:ℤh:¬x ≥ a.m⊢ (a ^ (k + 1)).seq x = (a ^ k).seq x * a.seq x a:Sequencek:ℕx:ℤh:¬x ≥ a.m⊢ (a ^ (k + 1)).seq x = 0
exact vanish _ _ (a:Sequencek:ℕx:ℤh:¬x ≥ a.m⊢ x < (a ^ (k + 1)).m a:Sequencek:ℕx:ℤh:x < a.m⊢ x < (a ^ (k + 1)).m; All goals completed! 🐙)Corollary 6.5.1
theorem Sequence.lim_of_power_decay {k:ℕ} :
((fun (n:ℕ) ↦ 1/((n:ℝ)+1)^(1/(k+1:ℝ))):Sequence).TendsTo 0 := k:ℕ⊢ (↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))).TendsTo 0
-- This proof is written to follow the structure of the original text.
k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))⊢ a.TendsTo 0
have ha : a.BddBelow := k:ℕ⊢ (↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))).TendsTo 0 k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))⊢ a.BddBelowBy 0; intro n k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))n:ℤa✝:n ≥ a.m⊢ a.seq n ≥ 0; k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))n:ℤa✝:n ≥ a.m⊢ 0 ≤ if 0 ≤ n then ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)⁻¹ else 0; All goals completed! 🐙
have ha' : a.IsAntitone := k:ℕ⊢ (↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))).TendsTo 0
intro n k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))n:ℤhn:n ≥ a.m⊢ a.seq (n + 1) ≤ a.seq n; k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))n:ℤhn:n ≥ a.mhn':0 ≤ n + 1⊢ a.seq (n + 1) ≤ a.seq n; k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))n:ℤhn:n ≥ a.mhn':0 ≤ n + 1⊢ ((↑(n + 1).toNat + 1) ^ (↑k + 1)⁻¹)⁻¹ ≤ ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)⁻¹
k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))n:ℤhn:n ≥ a.mhn':0 ≤ n + 1⊢ ↑n.toNat + 1 ≤ ↑(n + 1).toNat + 1k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))n:ℤhn:n ≥ a.mhn':0 ≤ n + 1⊢ 0 ≤ ↑n.toNat + 1k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))n:ℤhn:n ≥ a.mhn':0 ≤ n + 1⊢ 0 ≤ ↑(n + 1).toNat + 1k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))n:ℤhn:n ≥ a.mhn':0 ≤ n + 1⊢ 0 < (↑k + 1)⁻¹k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))n:ℤhn:n ≥ a.mhn':0 ≤ n + 1⊢ 0 < (↑(n + 1).toNat + 1) ^ (↑k + 1)⁻¹k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))n:ℤhn:n ≥ a.mhn':0 ≤ n + 1⊢ 0 < (↑n.toNat + 1) ^ (↑k + 1)⁻¹ k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))n:ℤhn:n ≥ a.mhn':0 ≤ n + 1⊢ ↑n.toNat + 1 ≤ ↑(n + 1).toNat + 1k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))n:ℤhn:n ≥ a.mhn':0 ≤ n + 1⊢ 0 ≤ ↑n.toNat + 1k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))n:ℤhn:n ≥ a.mhn':0 ≤ n + 1⊢ 0 ≤ ↑(n + 1).toNat + 1k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))n:ℤhn:n ≥ a.mhn':0 ≤ n + 1⊢ 0 < (↑k + 1)⁻¹k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))n:ℤhn:n ≥ a.mhn':0 ≤ n + 1⊢ 0 < (↑(n + 1).toNat + 1) ^ (↑k + 1)⁻¹k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))n:ℤhn:n ≥ a.mhn':0 ≤ n + 1⊢ 0 < (↑n.toNat + 1) ^ (↑k + 1)⁻¹ try All goals completed! 🐙
All goals completed! 🐙
k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))ha':a.Convergent⊢ a.TendsTo 0
have hpow (n:ℕ): (a^(n+1)).Convergent ∧ lim (a^(n+1)) = (lim a)^(n+1) := k:ℕ⊢ (↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))).TendsTo 0
k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))ha':a.Convergent⊢ (a ^ (0 + 1)).Convergent ∧ lim (a ^ (0 + 1)) = lim a ^ (0 + 1)k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))ha':a.Convergentn:ℕih:(a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)⊢ (a ^ (n + 1 + 1)).Convergent ∧ lim (a ^ (n + 1 + 1)) = lim a ^ (n + 1 + 1)
k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))ha':a.Convergent⊢ (a ^ (0 + 1)).Convergent ∧ lim (a ^ (0 + 1)) = lim a ^ (0 + 1) All goals completed! 🐙
k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))ha':a.Convergentn:ℕih:(a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)⊢ (a ^ (n + 1) * a).Convergent ∧ lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1); k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))ha':a.Convergentn:ℕih:(a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)⊢ lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1) ↔ lim (a ^ (n + 1) * a) = lim (a ^ (n + 1)) * lim a; k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))ha':a.Convergentn:ℕih:(a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)⊢ lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1) ↔ lim (a ^ (n + 1) * a) = lim a ^ (n + 1) * lim a; All goals completed! 🐙
have hlim : (lim a)^(k+1) = 0 := k:ℕ⊢ (↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))).TendsTo 0
k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))ha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1) :=
fun n =>
Nat.recAux
(of_eq_true
(Eq.trans
(congr
(congrArg And
(Eq.trans (congrArg Convergent (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))) (eq_true ha')))
(Eq.trans
(congr (congrArg Eq (congrArg lim (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))))
(Eq.trans (congrArg (HPow.hPow (lim a)) (zero_add 1)) (_root_.pow_one (lim a))))
(eq_self (lim a))))
(and_self True)))
(fun n ih =>
Eq.mpr (id (congrArg (fun _a => _a.Convergent ∧ lim _a = lim a ^ (n + 1 + 1)) (pow_succ a (n + 1))))
(Eq.mpr
(eq_of_heq
((fun a b b' e'_2 =>
Eq.casesOn (motive := fun a_1 x => b' = a_1 → e'_2 ≍ x → (a ∧ b) ≍ (a ∧ b')) e'_2
(fun h =>
Eq.ndrec (motive := fun b' => ∀ (e_2 : b = b'), e_2 ≍ Eq.refl b → (a ∧ b) ≍ (a ∧ b'))
(fun e_2 h => HEq.refl (a ∧ b)) (Eq.symm h) e'_2)
(Eq.refl b') (HEq.refl e'_2))
(a ^ (n + 1) * a).Convergent (lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1))
(lim (a ^ (n + 1) * a) = lim (a ^ (n + 1)) * lim a)
(propext
(Eq.mpr
(id
(congrArg
(fun _a => lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1) ↔ lim (a ^ (n + 1) * a) = _a * lim a)
ih.right))
(lim_of_power_decay._proof_10 n)))))
(lim_mul ih.left ha')))
n⊢ lim (a ^ (k + 1)) = 0; k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))ha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1) :=
fun n =>
Nat.recAux
(of_eq_true
(Eq.trans
(congr
(congrArg And
(Eq.trans (congrArg Convergent (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))) (eq_true ha')))
(Eq.trans
(congr (congrArg Eq (congrArg lim (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))))
(Eq.trans (congrArg (HPow.hPow (lim a)) (zero_add 1)) (_root_.pow_one (lim a))))
(eq_self (lim a))))
(and_self True)))
(fun n ih =>
Eq.mpr (id (congrArg (fun _a => _a.Convergent ∧ lim _a = lim a ^ (n + 1 + 1)) (pow_succ a (n + 1))))
(Eq.mpr
(eq_of_heq
((fun a b b' e'_2 =>
Eq.casesOn (motive := fun a_1 x => b' = a_1 → e'_2 ≍ x → (a ∧ b) ≍ (a ∧ b')) e'_2
(fun h =>
Eq.ndrec (motive := fun b' => ∀ (e_2 : b = b'), e_2 ≍ Eq.refl b → (a ∧ b) ≍ (a ∧ b'))
(fun e_2 h => HEq.refl (a ∧ b)) (Eq.symm h) e'_2)
(Eq.refl b') (HEq.refl e'_2))
(a ^ (n + 1) * a).Convergent (lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1))
(lim (a ^ (n + 1) * a) = lim (a ^ (n + 1)) * lim a)
(propext
(Eq.mpr
(id
(congrArg
(fun _a => lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1) ↔ lim (a ^ (n + 1) * a) = _a * lim a)
ih.right))
(lim_of_power_decay._proof_10 n)))))
(lim_mul ih.left ha')))
n⊢ a ^ (k + 1) = ↑fun n => (↑n + 1)⁻¹; k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))ha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1) :=
fun n =>
Nat.recAux
(of_eq_true
(Eq.trans
(congr
(congrArg And
(Eq.trans (congrArg Convergent (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))) (eq_true ha')))
(Eq.trans
(congr (congrArg Eq (congrArg lim (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))))
(Eq.trans (congrArg (HPow.hPow (lim a)) (zero_add 1)) (_root_.pow_one (lim a))))
(eq_self (lim a))))
(and_self True)))
(fun n ih =>
Eq.mpr (id (congrArg (fun _a => _a.Convergent ∧ lim _a = lim a ^ (n + 1 + 1)) (pow_succ a (n + 1))))
(Eq.mpr
(eq_of_heq
((fun a b b' e'_2 =>
Eq.casesOn (motive := fun a_1 x => b' = a_1 → e'_2 ≍ x → (a ∧ b) ≍ (a ∧ b')) e'_2
(fun h =>
Eq.ndrec (motive := fun b' => ∀ (e_2 : b = b'), e_2 ≍ Eq.refl b → (a ∧ b) ≍ (a ∧ b'))
(fun e_2 h => HEq.refl (a ∧ b)) (Eq.symm h) e'_2)
(Eq.refl b') (HEq.refl e'_2))
(a ^ (n + 1) * a).Convergent (lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1))
(lim (a ^ (n + 1) * a) = lim (a ^ (n + 1)) * lim a)
(propext
(Eq.mpr
(id
(congrArg
(fun _a => lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1) ↔ lim (a ^ (n + 1) * a) = _a * lim a)
ih.right))
(lim_of_power_decay._proof_10 n)))))
(lim_mul ih.left ha')))
n⊢ (a ^ (k + 1)).m = (↑fun n => (↑n + 1)⁻¹).mk:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))ha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1) :=
fun n =>
Nat.recAux
(of_eq_true
(Eq.trans
(congr
(congrArg And
(Eq.trans (congrArg Convergent (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))) (eq_true ha')))
(Eq.trans
(congr (congrArg Eq (congrArg lim (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))))
(Eq.trans (congrArg (HPow.hPow (lim a)) (zero_add 1)) (_root_.pow_one (lim a))))
(eq_self (lim a))))
(and_self True)))
(fun n ih =>
Eq.mpr (id (congrArg (fun _a => _a.Convergent ∧ lim _a = lim a ^ (n + 1 + 1)) (pow_succ a (n + 1))))
(Eq.mpr
(eq_of_heq
((fun a b b' e'_2 =>
Eq.casesOn (motive := fun a_1 x => b' = a_1 → e'_2 ≍ x → (a ∧ b) ≍ (a ∧ b')) e'_2
(fun h =>
Eq.ndrec (motive := fun b' => ∀ (e_2 : b = b'), e_2 ≍ Eq.refl b → (a ∧ b) ≍ (a ∧ b'))
(fun e_2 h => HEq.refl (a ∧ b)) (Eq.symm h) e'_2)
(Eq.refl b') (HEq.refl e'_2))
(a ^ (n + 1) * a).Convergent (lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1))
(lim (a ^ (n + 1) * a) = lim (a ^ (n + 1)) * lim a)
(propext
(Eq.mpr
(id
(congrArg
(fun _a => lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1) ↔ lim (a ^ (n + 1) * a) = _a * lim a)
ih.right))
(lim_of_power_decay._proof_10 n)))))
(lim_mul ih.left ha')))
nx✝:ℤ⊢ (a ^ (k + 1)).seq x✝ = (↑fun n => (↑n + 1)⁻¹).seq x✝; k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))ha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1) :=
fun n =>
Nat.recAux
(of_eq_true
(Eq.trans
(congr
(congrArg And
(Eq.trans (congrArg Convergent (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))) (eq_true ha')))
(Eq.trans
(congr (congrArg Eq (congrArg lim (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))))
(Eq.trans (congrArg (HPow.hPow (lim a)) (zero_add 1)) (_root_.pow_one (lim a))))
(eq_self (lim a))))
(and_self True)))
(fun n ih =>
Eq.mpr (id (congrArg (fun _a => _a.Convergent ∧ lim _a = lim a ^ (n + 1 + 1)) (pow_succ a (n + 1))))
(Eq.mpr
(eq_of_heq
((fun a b b' e'_2 =>
Eq.casesOn (motive := fun a_1 x => b' = a_1 → e'_2 ≍ x → (a ∧ b) ≍ (a ∧ b')) e'_2
(fun h =>
Eq.ndrec (motive := fun b' => ∀ (e_2 : b = b'), e_2 ≍ Eq.refl b → (a ∧ b) ≍ (a ∧ b'))
(fun e_2 h => HEq.refl (a ∧ b)) (Eq.symm h) e'_2)
(Eq.refl b') (HEq.refl e'_2))
(a ^ (n + 1) * a).Convergent (lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1))
(lim (a ^ (n + 1) * a) = lim (a ^ (n + 1)) * lim a)
(propext
(Eq.mpr
(id
(congrArg
(fun _a => lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1) ↔ lim (a ^ (n + 1) * a) = _a * lim a)
ih.right))
(lim_of_power_decay._proof_10 n)))))
(lim_mul ih.left ha')))
nx✝:ℤ⊢ (a ^ (k + 1)).seq x✝ = (↑fun n => (↑n + 1)⁻¹).seq x✝
k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))ha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1) :=
fun n =>
Nat.recAux
(of_eq_true
(Eq.trans
(congr
(congrArg And
(Eq.trans (congrArg Convergent (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))) (eq_true ha')))
(Eq.trans
(congr (congrArg Eq (congrArg lim (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))))
(Eq.trans (congrArg (HPow.hPow (lim a)) (zero_add 1)) (_root_.pow_one (lim a))))
(eq_self (lim a))))
(and_self True)))
(fun n ih =>
Eq.mpr (id (congrArg (fun _a => _a.Convergent ∧ lim _a = lim a ^ (n + 1 + 1)) (pow_succ a (n + 1))))
(Eq.mpr
(eq_of_heq
((fun a b b' e'_2 =>
Eq.casesOn (motive := fun a_1 x => b' = a_1 → e'_2 ≍ x → (a ∧ b) ≍ (a ∧ b')) e'_2
(fun h =>
Eq.ndrec (motive := fun b' => ∀ (e_2 : b = b'), e_2 ≍ Eq.refl b → (a ∧ b) ≍ (a ∧ b'))
(fun e_2 h => HEq.refl (a ∧ b)) (Eq.symm h) e'_2)
(Eq.refl b') (HEq.refl e'_2))
(a ^ (n + 1) * a).Convergent (lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1))
(lim (a ^ (n + 1) * a) = lim (a ^ (n + 1)) * lim a)
(propext
(Eq.mpr
(id
(congrArg
(fun _a => lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1) ↔ lim (a ^ (n + 1) * a) = _a * lim a)
ih.right))
(lim_of_power_decay._proof_10 n)))))
(lim_mul ih.left ha')))
nx✝:ℤ⊢ (if x✝ ≥ 0 then Monoid.npow (k + 1) (if x✝ ≥ 0 then 1 / (↑x✝.toNat + 1).rpow (1 / (↑k + 1)) else 0) else 0) =
if x✝ ≥ 0 then (↑x✝.toNat + 1)⁻¹ else 0; k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))ha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1) :=
fun n =>
Nat.recAux
(of_eq_true
(Eq.trans
(congr
(congrArg And
(Eq.trans (congrArg Convergent (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))) (eq_true ha')))
(Eq.trans
(congr (congrArg Eq (congrArg lim (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))))
(Eq.trans (congrArg (HPow.hPow (lim a)) (zero_add 1)) (_root_.pow_one (lim a))))
(eq_self (lim a))))
(and_self True)))
(fun n ih =>
Eq.mpr (id (congrArg (fun _a => _a.Convergent ∧ lim _a = lim a ^ (n + 1 + 1)) (pow_succ a (n + 1))))
(Eq.mpr
(eq_of_heq
((fun a b b' e'_2 =>
Eq.casesOn (motive := fun a_1 x => b' = a_1 → e'_2 ≍ x → (a ∧ b) ≍ (a ∧ b')) e'_2
(fun h =>
Eq.ndrec (motive := fun b' => ∀ (e_2 : b = b'), e_2 ≍ Eq.refl b → (a ∧ b) ≍ (a ∧ b'))
(fun e_2 h => HEq.refl (a ∧ b)) (Eq.symm h) e'_2)
(Eq.refl b') (HEq.refl e'_2))
(a ^ (n + 1) * a).Convergent (lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1))
(lim (a ^ (n + 1) * a) = lim (a ^ (n + 1)) * lim a)
(propext
(Eq.mpr
(id
(congrArg
(fun _a => lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1) ↔ lim (a ^ (n + 1) * a) = _a * lim a)
ih.right))
(lim_of_power_decay._proof_10 n)))))
(lim_mul ih.left ha')))
nx✝:ℤh:x✝ ≥ 0⊢ Monoid.npow (k + 1) (1 / (↑x✝.toNat + 1).rpow (1 / (↑k + 1))) = (↑x✝.toNat + 1)⁻¹k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))ha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1) :=
fun n =>
Nat.recAux
(of_eq_true
(Eq.trans
(congr
(congrArg And
(Eq.trans (congrArg Convergent (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))) (eq_true ha')))
(Eq.trans
(congr (congrArg Eq (congrArg lim (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))))
(Eq.trans (congrArg (HPow.hPow (lim a)) (zero_add 1)) (_root_.pow_one (lim a))))
(eq_self (lim a))))
(and_self True)))
(fun n ih =>
Eq.mpr (id (congrArg (fun _a => _a.Convergent ∧ lim _a = lim a ^ (n + 1 + 1)) (pow_succ a (n + 1))))
(Eq.mpr
(eq_of_heq
((fun a b b' e'_2 =>
Eq.casesOn (motive := fun a_1 x => b' = a_1 → e'_2 ≍ x → (a ∧ b) ≍ (a ∧ b')) e'_2
(fun h =>
Eq.ndrec (motive := fun b' => ∀ (e_2 : b = b'), e_2 ≍ Eq.refl b → (a ∧ b) ≍ (a ∧ b'))
(fun e_2 h => HEq.refl (a ∧ b)) (Eq.symm h) e'_2)
(Eq.refl b') (HEq.refl e'_2))
(a ^ (n + 1) * a).Convergent (lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1))
(lim (a ^ (n + 1) * a) = lim (a ^ (n + 1)) * lim a)
(propext
(Eq.mpr
(id
(congrArg
(fun _a => lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1) ↔ lim (a ^ (n + 1) * a) = _a * lim a)
ih.right))
(lim_of_power_decay._proof_10 n)))))
(lim_mul ih.left ha')))
nx✝:ℤh:¬x✝ ≥ 0⊢ 0 = 0
k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))ha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1) :=
fun n =>
Nat.recAux
(of_eq_true
(Eq.trans
(congr
(congrArg And
(Eq.trans (congrArg Convergent (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))) (eq_true ha')))
(Eq.trans
(congr (congrArg Eq (congrArg lim (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))))
(Eq.trans (congrArg (HPow.hPow (lim a)) (zero_add 1)) (_root_.pow_one (lim a))))
(eq_self (lim a))))
(and_self True)))
(fun n ih =>
Eq.mpr (id (congrArg (fun _a => _a.Convergent ∧ lim _a = lim a ^ (n + 1 + 1)) (pow_succ a (n + 1))))
(Eq.mpr
(eq_of_heq
((fun a b b' e'_2 =>
Eq.casesOn (motive := fun a_1 x => b' = a_1 → e'_2 ≍ x → (a ∧ b) ≍ (a ∧ b')) e'_2
(fun h =>
Eq.ndrec (motive := fun b' => ∀ (e_2 : b = b'), e_2 ≍ Eq.refl b → (a ∧ b) ≍ (a ∧ b'))
(fun e_2 h => HEq.refl (a ∧ b)) (Eq.symm h) e'_2)
(Eq.refl b') (HEq.refl e'_2))
(a ^ (n + 1) * a).Convergent (lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1))
(lim (a ^ (n + 1) * a) = lim (a ^ (n + 1)) * lim a)
(propext
(Eq.mpr
(id
(congrArg
(fun _a => lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1) ↔ lim (a ^ (n + 1) * a) = _a * lim a)
ih.right))
(lim_of_power_decay._proof_10 n)))))
(lim_mul ih.left ha')))
nx✝:ℤh:x✝ ≥ 0⊢ Monoid.npow (k + 1) (1 / (↑x✝.toNat + 1).rpow (1 / (↑k + 1))) = (↑x✝.toNat + 1)⁻¹ k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))ha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1) :=
fun n =>
Nat.recAux
(of_eq_true
(Eq.trans
(congr
(congrArg And
(Eq.trans (congrArg Convergent (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))) (eq_true ha')))
(Eq.trans
(congr (congrArg Eq (congrArg lim (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))))
(Eq.trans (congrArg (HPow.hPow (lim a)) (zero_add 1)) (_root_.pow_one (lim a))))
(eq_self (lim a))))
(and_self True)))
(fun n ih =>
Eq.mpr (id (congrArg (fun _a => _a.Convergent ∧ lim _a = lim a ^ (n + 1 + 1)) (pow_succ a (n + 1))))
(Eq.mpr
(eq_of_heq
((fun a b b' e'_2 =>
Eq.casesOn (motive := fun a_1 x => b' = a_1 → e'_2 ≍ x → (a ∧ b) ≍ (a ∧ b')) e'_2
(fun h =>
Eq.ndrec (motive := fun b' => ∀ (e_2 : b = b'), e_2 ≍ Eq.refl b → (a ∧ b) ≍ (a ∧ b'))
(fun e_2 h => HEq.refl (a ∧ b)) (Eq.symm h) e'_2)
(Eq.refl b') (HEq.refl e'_2))
(a ^ (n + 1) * a).Convergent (lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1))
(lim (a ^ (n + 1) * a) = lim (a ^ (n + 1)) * lim a)
(propext
(Eq.mpr
(id
(congrArg
(fun _a => lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1) ↔ lim (a ^ (n + 1) * a) = _a * lim a)
ih.right))
(lim_of_power_decay._proof_10 n)))))
(lim_mul ih.left ha')))
nx✝:ℤh:x✝ ≥ 0⊢ ((↑x✝.toNat + 1) ^ (↑k + 1)⁻¹) ^ (k + 1) = ↑x✝.toNat + 1
k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))ha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1) :=
fun n =>
Nat.recAux
(of_eq_true
(Eq.trans
(congr
(congrArg And
(Eq.trans (congrArg Convergent (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))) (eq_true ha')))
(Eq.trans
(congr (congrArg Eq (congrArg lim (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))))
(Eq.trans (congrArg (HPow.hPow (lim a)) (zero_add 1)) (_root_.pow_one (lim a))))
(eq_self (lim a))))
(and_self True)))
(fun n ih =>
Eq.mpr (id (congrArg (fun _a => _a.Convergent ∧ lim _a = lim a ^ (n + 1 + 1)) (pow_succ a (n + 1))))
(Eq.mpr
(eq_of_heq
((fun a b b' e'_2 =>
Eq.casesOn (motive := fun a_1 x => b' = a_1 → e'_2 ≍ x → (a ∧ b) ≍ (a ∧ b')) e'_2
(fun h =>
Eq.ndrec (motive := fun b' => ∀ (e_2 : b = b'), e_2 ≍ Eq.refl b → (a ∧ b) ≍ (a ∧ b'))
(fun e_2 h => HEq.refl (a ∧ b)) (Eq.symm h) e'_2)
(Eq.refl b') (HEq.refl e'_2))
(a ^ (n + 1) * a).Convergent (lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1))
(lim (a ^ (n + 1) * a) = lim (a ^ (n + 1)) * lim a)
(propext
(Eq.mpr
(id
(congrArg
(fun _a => lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1) ↔ lim (a ^ (n + 1) * a) = _a * lim a)
ih.right))
(lim_of_power_decay._proof_10 n)))))
(lim_mul ih.left ha')))
nx✝:ℤh:x✝ ≥ 0⊢ (↑x✝.toNat + 1) ^ ((↑k + 1)⁻¹ * ↑(k + 1)) = ↑x✝.toNat + 1
k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))ha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1) :=
fun n =>
Nat.recAux
(of_eq_true
(Eq.trans
(congr
(congrArg And
(Eq.trans (congrArg Convergent (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))) (eq_true ha')))
(Eq.trans
(congr (congrArg Eq (congrArg lim (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))))
(Eq.trans (congrArg (HPow.hPow (lim a)) (zero_add 1)) (_root_.pow_one (lim a))))
(eq_self (lim a))))
(and_self True)))
(fun n ih =>
Eq.mpr (id (congrArg (fun _a => _a.Convergent ∧ lim _a = lim a ^ (n + 1 + 1)) (pow_succ a (n + 1))))
(Eq.mpr
(eq_of_heq
((fun a b b' e'_2 =>
Eq.casesOn (motive := fun a_1 x => b' = a_1 → e'_2 ≍ x → (a ∧ b) ≍ (a ∧ b')) e'_2
(fun h =>
Eq.ndrec (motive := fun b' => ∀ (e_2 : b = b'), e_2 ≍ Eq.refl b → (a ∧ b) ≍ (a ∧ b'))
(fun e_2 h => HEq.refl (a ∧ b)) (Eq.symm h) e'_2)
(Eq.refl b') (HEq.refl e'_2))
(a ^ (n + 1) * a).Convergent (lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1))
(lim (a ^ (n + 1) * a) = lim (a ^ (n + 1)) * lim a)
(propext
(Eq.mpr
(id
(congrArg
(fun _a => lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1) ↔ lim (a ^ (n + 1) * a) = _a * lim a)
ih.right))
(lim_of_power_decay._proof_10 n)))))
(lim_mul ih.left ha')))
nx✝:ℤh:x✝ ≥ 0⊢ (↑k + 1)⁻¹ * ↑(k + 1) = 1; k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))ha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1) :=
fun n =>
Nat.recAux
(of_eq_true
(Eq.trans
(congr
(congrArg And
(Eq.trans (congrArg Convergent (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))) (eq_true ha')))
(Eq.trans
(congr (congrArg Eq (congrArg lim (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))))
(Eq.trans (congrArg (HPow.hPow (lim a)) (zero_add 1)) (_root_.pow_one (lim a))))
(eq_self (lim a))))
(and_self True)))
(fun n ih =>
Eq.mpr (id (congrArg (fun _a => _a.Convergent ∧ lim _a = lim a ^ (n + 1 + 1)) (pow_succ a (n + 1))))
(Eq.mpr
(eq_of_heq
((fun a b b' e'_2 =>
Eq.casesOn (motive := fun a_1 x => b' = a_1 → e'_2 ≍ x → (a ∧ b) ≍ (a ∧ b')) e'_2
(fun h =>
Eq.ndrec (motive := fun b' => ∀ (e_2 : b = b'), e_2 ≍ Eq.refl b → (a ∧ b) ≍ (a ∧ b'))
(fun e_2 h => HEq.refl (a ∧ b)) (Eq.symm h) e'_2)
(Eq.refl b') (HEq.refl e'_2))
(a ^ (n + 1) * a).Convergent (lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1))
(lim (a ^ (n + 1) * a) = lim (a ^ (n + 1)) * lim a)
(propext
(Eq.mpr
(id
(congrArg
(fun _a => lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1) ↔ lim (a ^ (n + 1) * a) = _a * lim a)
ih.right))
(lim_of_power_decay._proof_10 n)))))
(lim_mul ih.left ha')))
nx✝:ℤh:x✝ ≥ 0⊢ ↑(k + 1) = ↑k + 1; k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))ha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1) :=
fun n =>
Nat.recAux
(of_eq_true
(Eq.trans
(congr
(congrArg And
(Eq.trans (congrArg Convergent (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))) (eq_true ha')))
(Eq.trans
(congr (congrArg Eq (congrArg lim (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))))
(Eq.trans (congrArg (HPow.hPow (lim a)) (zero_add 1)) (_root_.pow_one (lim a))))
(eq_self (lim a))))
(and_self True)))
(fun n ih =>
Eq.mpr (id (congrArg (fun _a => _a.Convergent ∧ lim _a = lim a ^ (n + 1 + 1)) (pow_succ a (n + 1))))
(Eq.mpr
(eq_of_heq
((fun a b b' e'_2 =>
Eq.casesOn (motive := fun a_1 x => b' = a_1 → e'_2 ≍ x → (a ∧ b) ≍ (a ∧ b')) e'_2
(fun h =>
Eq.ndrec (motive := fun b' => ∀ (e_2 : b = b'), e_2 ≍ Eq.refl b → (a ∧ b) ≍ (a ∧ b'))
(fun e_2 h => HEq.refl (a ∧ b)) (Eq.symm h) e'_2)
(Eq.refl b') (HEq.refl e'_2))
(a ^ (n + 1) * a).Convergent (lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1))
(lim (a ^ (n + 1) * a) = lim (a ^ (n + 1)) * lim a)
(propext
(Eq.mpr
(id
(congrArg
(fun _a => lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1) ↔ lim (a ^ (n + 1) * a) = _a * lim a)
ih.right))
(lim_of_power_decay._proof_10 n)))))
(lim_mul ih.left ha')))
nx✝:ℤh:x✝ ≥ 0⊢ ↑k + 1 = ↑k + 1; All goals completed! 🐙
k:ℕa:Sequence := ↑fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelow :=
Exists.intro 0 fun n a_1 =>
Eq.mpr
(id
(Eq.trans
(congrFun'
(congrArg GE.ge
(ite_congr ge_iff_le._simp_1
(fun a =>
Eq.trans (congrArg (HDiv.hDiv 1) (congrArg (HPow.hPow (↑n.toNat + 1)) (one_div (↑k + 1))))
(one_div ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)))
fun a => Eq.refl 0))
0)
ge_iff_le._simp_1))
(Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (0 ≤ n)
(inv_pos_of_pos
(Real.rpow_pos_of_pos
(Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n.toNat)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Eq.refl (Nat.ble 1 1))))
(↑k + 1)⁻¹))
(Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))ha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1) :=
fun n =>
Nat.recAux
(of_eq_true
(Eq.trans
(congr
(congrArg And
(Eq.trans (congrArg Convergent (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))) (eq_true ha')))
(Eq.trans
(congr (congrArg Eq (congrArg lim (Eq.trans (congrArg (HPow.hPow a) (zero_add 1)) (pow_one a))))
(Eq.trans (congrArg (HPow.hPow (lim a)) (zero_add 1)) (_root_.pow_one (lim a))))
(eq_self (lim a))))
(and_self True)))
(fun n ih =>
Eq.mpr (id (congrArg (fun _a => _a.Convergent ∧ lim _a = lim a ^ (n + 1 + 1)) (pow_succ a (n + 1))))
(Eq.mpr
(eq_of_heq
((fun a b b' e'_2 =>
Eq.casesOn (motive := fun a_1 x => b' = a_1 → e'_2 ≍ x → (a ∧ b) ≍ (a ∧ b')) e'_2
(fun h =>
Eq.ndrec (motive := fun b' => ∀ (e_2 : b = b'), e_2 ≍ Eq.refl b → (a ∧ b) ≍ (a ∧ b'))
(fun e_2 h => HEq.refl (a ∧ b)) (Eq.symm h) e'_2)
(Eq.refl b') (HEq.refl e'_2))
(a ^ (n + 1) * a).Convergent (lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1))
(lim (a ^ (n + 1) * a) = lim (a ^ (n + 1)) * lim a)
(propext
(Eq.mpr
(id
(congrArg
(fun _a => lim (a ^ (n + 1) * a) = lim a ^ (n + 1 + 1) ↔ lim (a ^ (n + 1) * a) = _a * lim a)
ih.right))
(lim_of_power_decay._proof_10 n)))))
(lim_mul ih.left ha')))
nx✝:ℤh:¬x✝ ≥ 0⊢ 0 = 0 All goals completed! 🐙
All goals completed! 🐙Lemma 6.5.2 / Exercise 6.5.2
theorem declaration uses `sorry`Sequence.lim_of_geometric {x:ℝ} (hx: |x| < 1) : ((fun (n:ℕ) ↦ x^n):Sequence).TendsTo 0 := x:ℝhx:|x| < 1⊢ (↑fun n => x ^ n).TendsTo 0
All goals completed! 🐙Lemma 6.5.2 / Exercise 6.5.2
theorem declaration uses `sorry`Sequence.lim_of_geometric' {x:ℝ} (hx: x = 1) : ((fun (n:ℕ) ↦ x^n):Sequence).TendsTo 1 := x:ℝhx:x = 1⊢ (↑fun n => x ^ n).TendsTo 1
All goals completed! 🐙Lemma 6.5.2 / Exercise 6.5.2
theorem declaration uses `sorry`Sequence.lim_of_geometric'' {x:ℝ} (hx: x = -1 ∨ |x| > 1) :
((fun (n:ℕ) ↦ x^n):Sequence).Divergent := x:ℝhx:x = -1 ∨ |x| > 1⊢ (↑fun n => x ^ n).Divergent
All goals completed! 🐙Lemma 6.5.3 / Exercise 6.5.3
theorem declaration uses `sorry`Sequence.lim_of_roots {x:ℝ} (hx: x > 0) :
((fun (n:ℕ) ↦ x^(1/(n+1:ℝ))):Sequence).TendsTo 1 := x:ℝhx:x > 0⊢ (↑fun n => x ^ (1 / (↑n + 1))).TendsTo 1
All goals completed! 🐙Exercise 6.5.1
theorem declaration uses `sorry`Sequence.lim_of_rat_power_decay {q:ℚ} (hq: q > 0) :
(fun (n:ℕ) ↦ 1/((n+1:ℝ)^(q:ℝ)):Sequence).TendsTo 0 := q:ℚhq:q > 0⊢ (↑fun n => 1 / (↑n + 1) ^ ↑q).TendsTo 0
All goals completed! 🐙Exercise 6.5.1
theorem declaration uses `sorry`Sequence.lim_of_rat_power_growth {q:ℚ} (hq: q > 0) :
(fun (n:ℕ) ↦ ((n+1:ℝ)^(q:ℝ)):Sequence).Divergent := q:ℚhq:q > 0⊢ (↑fun n => (↑n + 1) ^ ↑q).Divergent
All goals completed! 🐙end Chapter6