Аналіз I, Глава 6.3

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:

• Suprema and infima of sequences

@[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 (Least upper bound property) / Вправа 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 (Least upper bound property) / Вправа 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 (Least upper bound property) / Вправа 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) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => x ^ n) n.toNat else 0, vanish := ⋯ }.convergent ∧ lim { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => x ^ n) n.toNat else 0, vanish := ⋯ } = 0

Твердження 6.3.1

theorem Chapter6.lim_of_exp' {x : ℝ} (hbound : x > 1) : ¬{ m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => x ^ n) n.toNat else 0, vanish := ⋯ }.convergent

Вправа 6.3.4