Аналіз I, Глава 6.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:

Some standard limits, including limits of sequences of the form 1/n^α, x^n, and x^(1/n).

namespace Chapter6

theorem declaration uses 'sorry'Sequence.lim_of_const (c:ℝ) :  ((fun (n:ℕ) ↦ c):Sequence).tendsTo c := byc:ℝ⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => c) n.toNat else 0, vanish := ⋯ }.tendsTo c sorryAll goals completed! 🐙

instance Sequence.inst_pow: Pow Sequence ℕ where
  pow a k := {
    m := a.m
    seq := fun (n:ℤ) ↦ if n ≥ a.m then a n ^ k else 0
    vanish := bya:Sequencek:ℕ⊢ ∀ n < a.m, (if n ≥ a.m then a.seq n ^ k else 0) = 0
      intro n hna:Sequencek:ℕn:ℤhn:n < a.m⊢ (if n ≥ a.m then a.seq n ^ k else 0) = 0
      rw [lt_iff_not_ge] at hna:Sequencek:ℕn:ℤhn:¬n ≥ a.m⊢ (if n ≥ a.m then a.seq n ^ k else 0) = 0
      simp [hn]All goals completed! 🐙
  }

@[simp]
lemma Sequence.pow_one (a:Sequence) : a^1 = a := bya:Sequence⊢ a ^ 1 = a
  ext nma:Sequence⊢ (a ^ 1).m = a.mseq.ha:Sequencen:ℤ⊢ (a ^ 1).seq n = a.seq n
  .ma:Sequence⊢ (a ^ 1).m = a.m rflAll goals completed! 🐙
  simp only [HPow.hPow, Pow.pow]seq.ha:Sequencen:ℤ⊢ (if n ≥ a.m then Monoid.npow 1 (a.seq n) else 0) = a.seq n
  by_cases h: n ≥ a.mposa:Sequencen:ℤh:n ≥ a.m⊢ (if n ≥ a.m then Monoid.npow 1 (a.seq n) else 0) = a.seq nnega:Sequencen:ℤh:¬n ≥ a.m⊢ (if n ≥ a.m then Monoid.npow 1 (a.seq n) else 0) = a.seq n
  .posa:Sequencen:ℤh:n ≥ a.m⊢ (if n ≥ a.m then Monoid.npow 1 (a.seq n) else 0) = a.seq n simp [h]All goals completed! 🐙
  simp [h, a.vanish n (by linarith)]All goals completed! 🐙

lemma Sequence.pow_succ (a:Sequence) (k:ℕ) : a^(k+1) = a^k * a := bya:Sequencek:ℕ⊢ a ^ (k + 1) = a ^ k * a
  ext nma:Sequencek:ℕ⊢ (a ^ (k + 1)).m = (a ^ k * a).mseq.ha:Sequencek:ℕn:ℤ⊢ (a ^ (k + 1)).seq n = (a ^ k * a).seq n
  .ma:Sequencek:ℕ⊢ (a ^ (k + 1)).m = (a ^ k * a).m simp only [HPow.hPow, Pow.pow, HMul.hMul, Mul.mul]ma:Sequencek:ℕ⊢ a.m = max a.m a.m
    simpAll goals completed! 🐙
  simp only [HPow.hPow, Pow.pow, HMul.hMul, Mul.mul]seq.ha:Sequencek:ℕn:ℤ⊢ (if n ≥ a.m then Monoid.npow (k + 1) (a.seq n) else 0) =
  if n ≥ max a.m a.m then Real.mul✝ (if n ≥ a.m then Monoid.npow k (a.seq n) else 0) (a.seq n) else 0
  by_cases h: n ≥ a.mposa:Sequencek:ℕn:ℤh:n ≥ a.m⊢ (if n ≥ a.m then Monoid.npow (k + 1) (a.seq n) else 0) =
  if n ≥ max a.m a.m then Real.mul✝ (if n ≥ a.m then Monoid.npow k (a.seq n) else 0) (a.seq n) else 0nega:Sequencek:ℕn:ℤh:¬n ≥ a.m⊢ (if n ≥ a.m then Monoid.npow (k + 1) (a.seq n) else 0) =
  if n ≥ max a.m a.m then Real.mul✝ (if n ≥ a.m then Monoid.npow k (a.seq n) else 0) (a.seq n) else 0
  .posa:Sequencek:ℕn:ℤh:n ≥ a.m⊢ (if n ≥ a.m then Monoid.npow (k + 1) (a.seq n) else 0) =
  if n ≥ max a.m a.m then Real.mul✝ (if n ≥ a.m then Monoid.npow k (a.seq n) else 0) (a.seq n) else 0 simp [h]posa:Sequencek:ℕn:ℤh:n ≥ a.m⊢ a.seq n ^ (k + 1) = Real.mul✝ (a.seq n ^ k) (a.seq n); rflAll goals completed! 🐙
  simp [h, a.vanish n (by linarith)]All goals completed! 🐙

Наслідок 6.5.1

theorem Sequence.lim_of_power_decay {k:ℕ} :
    ((fun (n:ℕ) ↦ 1/((n:ℝ)+1)^(1/(k+1:ℝ))):Sequence).tendsTo 0 := byk:ℕ⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }.tendsTo 0
  -- This proof is written to follow the structure of the original text.
  set a := ((fun (n:ℕ) ↦ 1/((n:ℝ)+1)^(1/(k+1:ℝ))):Sequence)k:ℕa:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }⊢ a.tendsTo 0
  have ha : a.bddBelow := byk:ℕ⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }.tendsTo 0
    use 0hk:ℕa:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }⊢ a.bddBelowBy 0
    intro n hnhk:ℕa:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }n:ℤhn:n ≥ a.m⊢ a.seq n ≥ 0
    simp [a]hk:ℕa:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }n:ℤhn:n ≥ a.m⊢ 0 ≤ if 0 ≤ n then ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)⁻¹ else 0
    positivityAll goals completed! 🐙
  have ha' : a.isAntitone := byk:ℕ⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }.tendsTo 0
    intro n hnk:ℕa:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }ha:a.bddBelown:ℤhn:n ≥ a.m⊢ a.seq (n + 1) ≤ a.seq n
    simp [a] at hn ⊢k:ℕa:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }ha:a.bddBelown:ℤhn:0 ≤ n⊢ (if 0 ≤ n + 1 then ((↑(n + 1).toNat + 1) ^ (↑k + 1)⁻¹)⁻¹ else 0) ≤ if 0 ≤ n then ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)⁻¹ else 0
    have hn' : 0 ≤ n+1 := byk:ℕ⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }.tendsTo 0 linarithAll goals completed! 🐙
    simp [hn,hn']k:ℕa:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }ha:a.bddBelown:ℤhn:0 ≤ nhn':0 ≤ n + 1⊢ ((↑(n + 1).toNat + 1) ^ (↑k + 1)⁻¹)⁻¹ ≤ ((↑n.toNat + 1) ^ (↑k + 1)⁻¹)⁻¹
    rw [inv_le_inv₀ (by positivity) (by positivity),
        Real.rpow_le_rpow_iff  (by positivity) (by positivity) (by positivity)]k:ℕa:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }ha:a.bddBelown:ℤhn:0 ≤ nhn':0 ≤ n + 1⊢ ↑n.toNat + 1 ≤ ↑(n + 1).toNat + 1
    simp [hn]All goals completed! 🐙
  replace ha' := convergent_of_antitone ha ha'k:ℕa:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }ha:a.bddBelowha':a.convergent⊢ a.tendsTo 0
  have hpow (n:ℕ): (a^(n+1)).convergent ∧ lim (a^(n+1)) = (lim a)^(n+1) := byk:ℕ⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }.tendsTo 0
    induction' n with n ihzerok:ℕa:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }ha:a.bddBelowha':a.convergent⊢ (a ^ (0 + 1)).convergent ∧ lim (a ^ (0 + 1)) = lim a ^ (0 + 1)succk:ℕa:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }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)
    .zerok:ℕa:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }ha:a.bddBelowha':a.convergent⊢ (a ^ (0 + 1)).convergent ∧ lim (a ^ (0 + 1)) = lim a ^ (0 + 1) simp only [zero_add, pow_one, _root_.pow_one, ha', true_and]All goals completed! 🐙
    rw [pow_succ]succk:ℕa:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }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)
    convert lim_mul ih.1 ha'h.e'_2.h.e'_3k:ℕa:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }ha:a.bddBelowha':a.convergentn:ℕih:(a ^ (n + 1)).convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)⊢ lim a ^ (n + 1 + 1) = lim (a ^ (n + 1)) * lim a
    rw [ih.2]h.e'_2.h.e'_3k:ℕa:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }ha:a.bddBelowha':a.convergentn:ℕih:(a ^ (n + 1)).convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)⊢ lim a ^ (n + 1 + 1) = lim a ^ (n + 1) * lim a
    rflAll goals completed! 🐙
  have hlim : (lim a)^(k+1) = 0 := byk:ℕ⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }.tendsTo 0
    rw [←(hpow k).2]k:ℕa:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }ha:a.bddBelowha':a.convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)⊢ lim (a ^ (k + 1)) = 0
    convert lim_harmonic.2 with nh.e'_2.h.e'_1.h.e'_2.hk:ℕa:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }ha:a.bddBelowha':a.convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)n:ℤ⊢ (a ^ (k + 1)).seq n = if n ≥ 0 then (fun n => (↑n + 1)⁻¹) n.toNat else 0
    simp only [HPow.hPow, Pow.pow, a]h.e'_2.h.e'_1.h.e'_2.hk:ℕa:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }ha:a.bddBelowha':a.convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)n:ℤ⊢ (if n ≥ 0 then Monoid.npow (k + 1) (if n ≥ 0 then 1 / (↑n.toNat + 1).rpow (1 / (↑k + 1)) else 0) else 0) =
  if n ≥ 0 then (↑n.toNat + 1)⁻¹ else 0
    by_cases h : n ≥ 0posk:ℕa:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }ha:a.bddBelowha':a.convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)n:ℤh:n ≥ 0⊢ (if n ≥ 0 then Monoid.npow (k + 1) (if n ≥ 0 then 1 / (↑n.toNat + 1).rpow (1 / (↑k + 1)) else 0) else 0) =
  if n ≥ 0 then (↑n.toNat + 1)⁻¹ else 0negk:ℕa:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }ha:a.bddBelowha':a.convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)n:ℤh:¬n ≥ 0⊢ (if n ≥ 0 then Monoid.npow (k + 1) (if n ≥ 0 then 1 / (↑n.toNat + 1).rpow (1 / (↑k + 1)) else 0) else 0) =
  if n ≥ 0 then (↑n.toNat + 1)⁻¹ else 0
    all_goals simp [h]All goals completed! 🐙
    rw [←Real.rpow_natCast,←Real.rpow_mul (by positivity)]posk:ℕa:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }ha:a.bddBelowha':a.convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)n:ℤh:n ≥ 0⊢ (↑n.toNat + 1) ^ ((↑k + 1)⁻¹ * ↑(k + 1)) = ↑n.toNat + 1
    convert Real.rpow_one _h.e'_2.h.e'_6k:ℕa:Sequence := { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }ha:a.bddBelowha':a.convergenthpow:∀ (n : ℕ), (a ^ (n + 1)).convergent ∧ lim (a ^ (n + 1)) = lim a ^ (n + 1)n:ℤh:n ≥ 0⊢ (↑k + 1)⁻¹ * ↑(k + 1) = 1
    field_simpAll goals completed! 🐙
  simp only [lim_eq, ha', true_and, pow_eq_zero hlim]All goals completed! 🐙

Лема 6.5.2 / Вправа 6.5.2

theorem declaration uses 'sorry'Sequence.lim_of_geometric {x:ℝ} (hx: |x| < 1) : lim ((fun (n:ℕ) ↦ x^n):Sequence) = 0 := byx:ℝhx:|x| < 1⊢ lim { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ } = 0
  sorryAll goals completed! 🐙

Лема 6.5.2 / Вправа 6.5.2

theorem declaration uses 'sorry'Sequence.lim_of_geometric' {x:ℝ} (hx: x = 1) : lim ((fun (n:ℕ) ↦ x^n):Sequence) = 1 := byx:ℝhx:x = 1⊢ lim { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ } = 1
  sorryAll goals completed! 🐙

Лема 6.5.2 / Вправа 6.5.2

theorem declaration uses 'sorry'Sequence.lim_of_geometric'' {x:ℝ} (hx: x = -1 ∨ |x| > 1) :
    ((fun (n:ℕ) ↦ x^n):Sequence).divergent := byx:ℝhx:x = -1 ∨ |x| > 1⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ n) n.toNat else 0, vanish := ⋯ }.divergent
  sorryAll goals completed! 🐙

Лема 6.5.3 / Вправа 6.5.3

theorem declaration uses 'sorry'Sequence.lim_of_roots {x:ℝ} (hx: x > 0) :
    lim ((fun (n:ℕ) ↦ x^(1/(n+1))):Sequence) = 1 := byx:ℝhx:x > 0⊢ lim { m := 0, seq := fun n => if n ≥ 0 then (fun n => x ^ (1 / (n + 1))) n.toNat else 0, vanish := ⋯ } = 1
  sorryAll goals completed! 🐙

Вправа 6.5.1

theorem declaration uses 'sorry'Sequence.lim_of_rat_power_decay {q:ℚ} (hq: q > 0) :
    lim ((fun (n:ℕ) ↦ 1/((n:ℝ)+1)^(q:ℝ)):Sequence) = 0 := byq:ℚhq:q > 0⊢ lim { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1) ^ ↑q) n.toNat else 0, vanish := ⋯ } = 0
  sorryAll goals completed! 🐙

Вправа 6.5.1

theorem declaration uses 'sorry'Sequence.lim_of_rat_power_growth {q:ℚ} (hq: q > 0) :
    ((fun (n:ℕ) ↦ ((n:ℝ)+1)^(q:ℝ)):Sequence).divergent := byq:ℚhq:q > 0⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => (↑n + 1) ^ ↑q) n.toNat else 0, vanish := ⋯ }.divergent
  sorryAll goals completed! 🐙

end Chapter6