Imports
import Mathlib.Tactic
import Analysis.Section_6_4Analysis 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 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.BddBelown:ℤhn:n ≥ a.m⊢ a.seq (n + 1) ≤ a.seq n; k:ℕa:Sequence := ↑fun n ↦ 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelown:ℤ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.BddBelown:ℤ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.BddBelown:ℤ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.BddBelown:ℤhn:n ≥ a.mhn':0 ≤ n + 1⊢ 0 ≤ ↑n.toNat + 1k:ℕa:Sequence := ↑fun n ↦ 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelown:ℤhn:n ≥ a.mhn':0 ≤ n + 1⊢ 0 ≤ ↑(n + 1).toNat + 1k:ℕa:Sequence := ↑fun n ↦ 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelown:ℤhn:n ≥ a.mhn':0 ≤ n + 1⊢ 0 < (↑k + 1)⁻¹k:ℕa:Sequence := ↑fun n ↦ 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelown:ℤ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.BddBelown:ℤ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.BddBelown:ℤ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.BddBelown:ℤhn:n ≥ a.mhn':0 ≤ n + 1⊢ 0 ≤ ↑n.toNat + 1k:ℕa:Sequence := ↑fun n ↦ 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelown:ℤhn:n ≥ a.mhn':0 ≤ n + 1⊢ 0 ≤ ↑(n + 1).toNat + 1k:ℕa:Sequence := ↑fun n ↦ 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelown:ℤhn:n ≥ a.mhn':0 ≤ n + 1⊢ 0 < (↑k + 1)⁻¹k:ℕa:Sequence := ↑fun n ↦ 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelown:ℤ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.BddBelown:ℤ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.BddBelowha':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.BddBelowha':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.BddBelowha':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.BddBelowha':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.BddBelowha':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.BddBelowha':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.BddBelowha':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.BddBelowha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)⊢ lim (a ^ (k + 1)) = 0; k:ℕa:Sequence := ↑fun n ↦ 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelowha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)⊢ a ^ (k + 1) = ↑fun n ↦ (↑n + 1)⁻¹; k:ℕa:Sequence := ↑fun n ↦ 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelowha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)⊢ (a ^ (k + 1)).m = (↑fun n ↦ (↑n + 1)⁻¹).mk:ℕa:Sequence := ↑fun n ↦ 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelowha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)x✝:ℤ⊢ (a ^ (k + 1)).seq x✝ = (↑fun n ↦ (↑n + 1)⁻¹).seq x✝; k:ℕa:Sequence := ↑fun n ↦ 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelowha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)x✝:ℤ⊢ (a ^ (k + 1)).seq x✝ = (↑fun n ↦ (↑n + 1)⁻¹).seq x✝
k:ℕa:Sequence := ↑fun n ↦ 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelowha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)x✝:ℤ⊢ (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.BddBelowha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)x✝:ℤ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.BddBelowha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)x✝:ℤh:¬x✝ ≥ 0⊢ 0 = 0
k:ℕa:Sequence := ↑fun n ↦ 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelowha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)x✝:ℤ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.BddBelowha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)x✝:ℤ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.BddBelowha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)x✝:ℤ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.BddBelowha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)x✝:ℤh:x✝ ≥ 0⊢ (↑k + 1)⁻¹ * ↑(k + 1) = 1; k:ℕa:Sequence := ↑fun n ↦ 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelowha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)x✝:ℤh:x✝ ≥ 0⊢ ↑(k + 1) = ↑k + 1; k:ℕa:Sequence := ↑fun n ↦ 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelowha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)x✝:ℤh:x✝ ≥ 0⊢ ↑k + 1 = ↑k + 1; All goals completed! 🐙
k:ℕa:Sequence := ↑fun n ↦ 1 / (↑n + 1) ^ (1 / (↑k + 1))ha:a.BddBelowha':a.Convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).Convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)x✝:ℤh:¬x✝ ≥ 0⊢ 0 = 0 All goals completed! 🐙
All goals completed! 🐙Lemma 6.5.2 (ratio of absolute value less than one) / Exercise 6.5.2
theorem 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 (ratio one) / Exercise 6.5.2
theorem 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 (ratio minus one or of absolute value greater than one) / Exercise 6.5.2
theorem 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 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 (i)
theorem 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 (ii)
theorem 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