Аналіз I, Розділ 6.3: Супремуми та інфімуми послідовностей

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

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

• Супремуми та інфімуми послідовностей.

@[reducible, inline]

noncomputable abbrev Chapter6.Sequence.sup (a : Sequence) : EReal

Визначення 6.3.1

Equations

• a.sup = sSup {x : EReal | ∃ n ≥ a.m, x = ↑(a.seq n)}

@[reducible, inline]

noncomputable abbrev Chapter6.Sequence.inf (a : Sequence) : EReal

Визначення 6.3.1

Equations

• a.inf = sInf {x : EReal | ∃ n ≥ a.m, x = ↑(a.seq n)}

@[reducible, inline]

abbrev Chapter6.Sequence.BddAboveBy (a : Sequence) (M : ℝ) : Prop

Equations

• a.BddAboveBy M = ∀ n ≥ a.m, a.seq n ≤ M

@[reducible, inline]

abbrev Chapter6.Sequence.BddAbove (a : Sequence) : Prop

Equations

• a.BddAbove = ∃ (M : ℝ), a.BddAboveBy M

@[reducible, inline]

abbrev Chapter6.Sequence.BddBelowBy (a : Sequence) (M : ℝ) : Prop

Equations

• a.BddBelowBy M = ∀ n ≥ a.m, a.seq n ≥ M

@[reducible, inline]

abbrev Chapter6.Sequence.BddBelow (a : Sequence) : Prop

Equations

• a.BddBelow = ∃ (M : ℝ), a.BddBelowBy M

theorem Chapter6.Sequence.bounded_iff (a : Sequence) : a.IsBounded ↔ a.BddAbove ∧ a.BddBelow

theorem Chapter6.Sequence.sup_of_bounded {a : Sequence} (h : a.IsBounded) : a.sup.IsFinite

theorem Chapter6.Sequence.inf_of_bounded {a : Sequence} (h : a.IsBounded) : a.inf.IsFinite

theorem Chapter6.Sequence.le_sup {a : Sequence} {n : ℤ} (hn : n ≥ a.m) : ↑(a.seq n) ≤ a.sup

Твердження 6.3.6 (Властивість найменшої верхньої межі) / Вправа 6.3.2

theorem Chapter6.Sequence.sup_le_upper {a : Sequence} {M : EReal} (h : ∀ n ≥ a.m, ↑(a.seq n) ≤ M) : a.sup ≤ M

Твердження 6.3.6 (Властивість найменшої верхньої межі) / Вправа 6.3.2

theorem Chapter6.Sequence.exists_between_lt_sup {a : Sequence} {y : EReal} (h : y < a.sup) : ∃ n ≥ a.m, y < ↑(a.seq n) ∧ ↑(a.seq n) ≤ a.sup

Твердження 6.3.6 (Властивість найменшої верхньої межі) / Вправа 6.3.2

theorem Chapter6.Sequence.ge_inf {a : Sequence} {n : ℤ} (hn : n ≥ a.m) : ↑(a.seq n) ≥ a.inf

Зауваження 6.3.7

theorem Chapter6.Sequence.inf_ge_lower {a : Sequence} {M : EReal} (h : ∀ n ≥ a.m, ↑(a.seq n) ≥ M) : a.inf ≥ M

Зауваження 6.3.7

theorem Chapter6.Sequence.exists_between_gt_inf {a : Sequence} {y : EReal} (h : y > a.inf) : ∃ n ≥ a.m, y > ↑(a.seq n) ∧ ↑(a.seq n) ≥ a.inf

Зауваження 6.3.7

@[reducible, inline]

abbrev Chapter6.Sequence.IsMonotone (a : Sequence) : Prop

Equations

• a.IsMonotone = ∀ n ≥ a.m, a.seq (n + 1) ≥ a.seq n

@[reducible, inline]

abbrev Chapter6.Sequence.IsAntitone (a : Sequence) : Prop

Equations

• a.IsAntitone = ∀ n ≥ a.m, a.seq (n + 1) ≤ a.seq n

theorem Chapter6.Sequence.convergent_of_monotone {a : Sequence} (hbound : a.BddAbove) (hmono : a.IsMonotone) : a.Convergent

Твердження 6.3.8 / Вправа 6.3.3

theorem Chapter6.Sequence.lim_of_monotone {a : Sequence} (hbound : a.BddAbove) (hmono : a.IsMonotone) : ↑(lim a) = a.sup

Твердження 6.3.8 / Вправа 6.3.3

theorem Chapter6.Sequence.convergent_of_antitone {a : Sequence} (hbound : a.BddBelow) (hmono : a.IsAntitone) : a.Convergent

theorem Chapter6.Sequence.lim_of_antitone {a : Sequence} (hbound : a.BddBelow) (hmono : a.IsAntitone) : ↑(lim a) = a.inf

theorem Chapter6.Sequence.convergent_iff_bounded_of_monotone {a : Sequence} (ha : a.IsMonotone) : a.Convergent ↔ a.IsBounded

theorem Chapter6.Sequence.bounded_iff_convergent_of_antitone {a : Sequence} (ha : a.IsAntitone) : a.Convergent ↔ a.IsBounded

@[reducible, inline]

noncomputable abbrev Chapter6.Example_6_3_9 (n : ℕ) : ℝ

Приклад 6.3.9

Equations

• Chapter6.Example_6_3_9 n = ↑⌊Real.pi * 10 ^ n⌋ / 10 ^ n

theorem Chapter6.lim_of_exp {x : ℝ} (hpos : 0 < x) (hbound : x < 1) : (↑fun (n : ℕ) => x ^ n).Convergent ∧ (lim ↑fun (n : ℕ) => x ^ n) = 0

Твердження 6.3.1

theorem Chapter6.lim_of_exp' {x : ℝ} (hbound : x > 1) : ¬(↑fun (n : ℕ) => x ^ n).Convergent

Вправа 6.3.4