Аналіз 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).

theorem Chapter6.Sequence.lim_of_const (c : ℝ) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => c) n.toNat else 0, vanish := ⋯ }.tendsTo c

instance Chapter6.Sequence.inst_pow : Pow Sequence ℕ

Equations

• Chapter6.Sequence.inst_pow = { pow := fun (a : Chapter6.Sequence) (k : ℕ) => { m := a.m, seq := fun (n : ℤ) => if n ≥ a.m then a.seq n ^ k else 0, vanish := ⋯ } }

@[simp]

theorem Chapter6.Sequence.pow_one (a : Sequence) : a ^ 1 = a

theorem Chapter6.Sequence.pow_succ (a : Sequence) (k : ℕ) : a ^ (k + 1) = a ^ k * a

theorem Chapter6.Sequence.lim_of_power_decay {k : ℕ} : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => 1 / (↑n + 1) ^ (1 / (↑k + 1))) n.toNat else 0, vanish := ⋯ }.tendsTo 0

Наслідок 6.5.1

theorem Chapter6.Sequence.lim_of_geometric {x : ℝ} (hx : |x| < 1) : lim { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => x ^ n) n.toNat else 0, vanish := ⋯ } = 0

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

theorem Chapter6.Sequence.lim_of_geometric' {x : ℝ} (hx : x = 1) : lim { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => x ^ n) n.toNat else 0, vanish := ⋯ } = 1

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

theorem Chapter6.Sequence.lim_of_geometric'' {x : ℝ} (hx : x = -1 ∨ |x| > 1) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => x ^ n) n.toNat else 0, vanish := ⋯ }.divergent

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

theorem Chapter6.Sequence.lim_of_roots {x : ℝ} (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

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

theorem Chapter6.Sequence.lim_of_rat_power_decay {q : ℚ} (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

Вправа 6.5.1

theorem Chapter6.Sequence.lim_of_rat_power_growth {q : ℚ} (hq : q > 0) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => (↑n + 1) ^ ↑q) n.toNat else 0, vanish := ⋯ }.divergent

Вправа 6.5.1