Аналіз I, Розділ 6.5: Деякі стандартні границі

Я (прим. перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним підходом Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підправити", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Основні конструкції та результати цього розділу:

• Деякі стандартні границі, включно з границями послідовностей виду 1/n^α, x^n та x^(1/n).

theorem Chapter6.Sequence.lim_of_const (c : ℝ) : (↑fun (x : ℕ) => c).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_eval {a : Sequence} {k : ℕ} {n : ℤ} (hn : n ≥ a.m) : (a ^ k).seq n = a.seq n ^ k

@[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 : ℕ} : (↑fun (n : ℕ) => 1 / (↑n + 1) ^ (1 / (↑k + 1))).TendsTo 0

Наслідок 6.5.1

theorem Chapter6.Sequence.lim_of_geometric {x : ℝ} (hx : |x| < 1) : (↑fun (n : ℕ) => x ^ n).TendsTo 0

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

theorem Chapter6.Sequence.lim_of_geometric' {x : ℝ} (hx : x = 1) : (↑fun (n : ℕ) => x ^ n).TendsTo 1

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

theorem Chapter6.Sequence.lim_of_geometric'' {x : ℝ} (hx : x = -1 ∨ |x| > 1) : (↑fun (n : ℕ) => x ^ n).Divergent

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

theorem Chapter6.Sequence.lim_of_roots {x : ℝ} (hx : x > 0) : (↑fun (n : ℕ) => x ^ (1 / (↑n + 1))).TendsTo 1

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

theorem Chapter6.Sequence.lim_of_rat_power_decay {q : ℚ} (hq : q > 0) : (↑fun (n : ℕ) => 1 / (↑n + 1) ^ ↑q).TendsTo 0

Вправа 6.5.1

theorem Chapter6.Sequence.lim_of_rat_power_growth {q : ℚ} (hq : q > 0) : (↑fun (n : ℕ) => (↑n + 1) ^ ↑q).Divergent

Вправа 6.5.1