Аналіз I, Розділ 7.5: Ознаки кореня та відношення

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

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

• Ознаки кореня та відношення

Одне, що лише імпліцитно вказане в тексті, — це те, що для ознаки кореня та ознаки відношення нижню та верхню границі (lim inf і lim sup) слід розуміти в розширених дійсних числах. Формалізації в Lean нижче роблять це твердження більш явним.

theorem Chapter7.Series.root_test_pos {s : Series} (h : Filter.limsup (fun (n : ℤ) => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTop < 1) : s.absConverges

Твердження 7.5.1(a) (Ознака кореня). Потрібна технічна умова для забезпечення скінченності limsup.

theorem Chapter7.Series.root_test_neg {s : Series} (h : Filter.limsup (fun (n : ℤ) => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTop > 1) : s.diverges

Теорема 7.5.1(b) (Ознака кореня)

theorem Chapter7.Series.root_test_inconclusive : ∃ (s : Series), Filter.Tendsto (fun (n : ℤ) => |s.seq n| ^ (1 / ↑n)) Filter.atTop (nhds 1) ∧ s.diverges

Теорема 7.5.1(c) (Ознака кореня) / Вправа 7.5.3

theorem Chapter7.Series.root_test_inconclusive' : ∃ (s : Series), Filter.Tendsto (fun (n : ℤ) => |s.seq n| ^ (1 / ↑n)) Filter.atTop (nhds 1) ∧ s.absConverges

Теорема 7.5.1 (Ознака кореня) / Вправа 7.5.3

theorem Chapter7.Series.ratio_ineq {c : ℤ → ℝ} (m : ℤ) (hpos : ∀ n ≥ m, c n > 0) : Filter.liminf (fun (n : ℤ) => ↑(c (n + 1) / c n)) Filter.atTop ≤ Filter.liminf (fun (n : ℤ) => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧ Filter.liminf (fun (n : ℤ) => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun (n : ℤ) => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧ Filter.limsup (fun (n : ℤ) => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun (n : ℤ) => ↑(c (n + 1) / c n)) Filter.atTop

Лема 7.5.2 / Вправа 7.5.1

theorem Chapter7.Series.ratio_test_pos {s : Series} (hnon : ∀ n ≥ s.m, s.seq n ≠ 0) (h : Filter.limsup (fun (n : ℤ) => ↑(|s.seq (n + 1)| / |s.seq n|)) Filter.atTop < 1) : s.absConverges

Наслідок 7.5.3 (Ознака відношення)

theorem Chapter7.Series.ratio_test_neg {s : Series} (hnon : ∀ n ≥ s.m, s.seq n ≠ 0) (h : Filter.liminf (fun (n : ℤ) => ↑(|s.seq (n + 1)| / |s.seq n|)) Filter.atTop > 1) : s.diverges

Наслідок 7.5.3 (Ознака відношення)

theorem Chapter7.Series.ratio_test_inconclusive : ∃ (s : Series), (∀ n ≥ s.m, s.seq n ≠ 0) ∧ Filter.Tendsto (fun (n : ℤ) => |s.seq n + 1| / |s.seq n|) Filter.atTop (nhds 1) ∧ s.diverges

Наслідок 7.5.3 (Ознака відношення) / Вправа 7.5.3

theorem Chapter7.Series.ratio_test_inconclusive' : ∃ (s : Series), (∀ n ≥ s.m, s.seq n ≠ 0) ∧ Filter.Tendsto (fun (n : ℤ) => |s.seq n + 1| / |s.seq n|) Filter.atTop (nhds 1) ∧ s.absConverges

Наслідок 7.5.3 (Ознака відношення) / Вправа 7.5.3

theorem Chapter7.Series.root_self_converges : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => ↑n ^ (1 / ↑n)) n.toNat else 0, vanish := ⋯ }.convergesTo 1

Твердження 7.5.4

theorem Chapter7.Series.poly_mul_geom_converges {x : ℝ} (hx : |x| < 1) (q : ℝ) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => ↑n ^ q * x ^ n) n.toNat else 0, vanish := ⋯ }.converges ∧ Filter.Tendsto (fun (n : ℕ) => ↑n ^ q * x ^ n) Filter.atTop (nhds 0)

Вправа 7.5.2