Analysis I, Section 6.3: Suprema and infima of sequences

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

Definition 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

Definition 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

Proposition 6.3.6 (Least upper bound property) / Exercise 6.3.2

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

Proposition 6.3.6 (Least upper bound property) / Exercise 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

Proposition 6.3.6 (Least upper bound property) / Exercise 6.3.2

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

Remark 6.3.7

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

Remark 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

Remark 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

Proposition 6.3.8 / Exercise 6.3.3

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

Proposition 6.3.8 / Exercise 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 : ℕ) : ℝ

Example 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

Proposition 6.3.1

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

Exercise 6.3.4