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

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.

In this section we begin to use the Mathlib API for sets; the Chapter 3 set theory is deprecated in favor of this API.

Main constructions and results of this section:

• Upper bound and least upper bound on the real line

theorem Chapter5.Real.upperBound_def (E : Set Real) (M : Real) : M ∈ upperBounds E ↔ ∀ x ∈ E, x ≤ M

Визначення 5.5.1 (upper bounds). Here we use the upperBounds set defined in Mathlib.

theorem Chapter5.Real.lowerBound_def (E : Set Real) (M : Real) : M ∈ lowerBounds E ↔ ∀ x ∈ E, x ≥ M

theorem Chapter5.Real.Icc_def (x y : Real) : Set.Icc x y = {z : Real | x ≤ z ∧ z ≤ y}

API for Example 5.5.2

theorem Chapter5.Real.mem_Icc (x y z : Real) : z ∈ Set.Icc x y ↔ x ≤ z ∧ z ≤ y

API for Example 5.5.2

theorem Chapter5.Real.Ioi_def (x : Real) : Set.Ioi x = {z : Real | z > x}

API for Example 5.5.3

theorem Chapter5.Real.upperBound_upper {M M' : Real} (h : M ≤ M') {E : Set Real} (hb : M ∈ upperBounds E) : M' ∈ upperBounds E

theorem Chapter5.Real.isLUB_def (E : Set Real) (M : Real) : IsLUB E M ↔ M ∈ upperBounds E ∧ ∀ M' ∈ upperBounds E, M' ≥ M

Визначення 5.5.5 (least upper bound). Here we use the isLUB predicate defined in Mathlib.

theorem Chapter5.Real.isGLB_def (E : Set Real) (M : Real) : IsGLB E M ↔ M ∈ lowerBounds E ∧ ∀ M' ∈ lowerBounds E, M' ≤ M

theorem Chapter5.Real.LUB_unique {E : Set Real} {M M' : Real} (h1 : IsLUB E M) (h2 : IsLUB E M') : M = M'

Твердження 5.5.8 (Uniqueness of least upper bound)

theorem Chapter5.Real.bddAbove_def (E : Set Real) : BddAbove E ↔ ∃ (M : Real), M ∈ upperBounds E

Визначення of "bounded above", using Mathlib notation

theorem Chapter5.Real.bddBelow_def (E : Set Real) : BddBelow E ↔ ∃ (M : Real), M ∈ lowerBounds E

theorem Chapter5.Real.upperBound_between {E : Set Real} {n : ℕ} {L K : ℤ} (hLK : L < K) (hK : ↑K * ↑(1 / (↑n + 1)) ∈ upperBounds E) (hL : ↑L * ↑(1 / (↑n + 1)) ∉ upperBounds E) : ∃ (m : ℤ), L < m ∧ m ≤ K ∧ ↑m * ↑(1 / (↑n + 1)) ∈ upperBounds E ∧ (↑m - 1) * ↑(1 / (↑n + 1)) ∉ upperBounds E

Вправа 5.5.2

theorem Chapter5.Real.upperBound_discrete_unique {E : Set Real} {n : ℕ} {m m' : ℤ} (hm1 : ↑(↑m / (↑n + 1)) ∈ upperBounds E) (hm2 : ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E) (hm'1 : ↑(↑m' / (↑n + 1)) ∈ upperBounds E) (hm'2 : ↑(↑m' / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E) : m = m'

Вправа 5.5.3

theorem Chapter5.Real.LIM_of_Cauchy {q : ℕ → ℚ} (hq : ∀ (M n : ℕ), n ≥ M → ∀ n' ≥ M, |q n - q n'| ≤ 1 / (↑M + 1)) : { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then q n.toNat else 0, vanish := ⋯ }.isCauchy ∧ ∀ (M : ℕ), |↑(q M) - LIM q| ≤ 1 / (↑M + 1)

Вправа 5.5.4

theorem Chapter5.Real.LUB_exist {E : Set Real} (hE : E.Nonempty) (hbound : BddAbove E) : ∃ (S : Real), IsLUB E S

Теорема 5.5.9 (Existence of least upper bound)

inductive Chapter5.ExtendedReal : Type

A bare-bones extended real class to define supremum.

• neg_infty : ExtendedReal
• real (x : Real) : ExtendedReal
• infty : ExtendedReal

instance Chapter5.ExtendedReal.inst_Top : Top ExtendedReal

Mathlib prefers ⊤ to denote the +∞ element.

Equations

• Chapter5.ExtendedReal.inst_Top = { top := Chapter5.ExtendedReal.infty }

instance Chapter5.ExtendedReal.inst_Bot : Bot ExtendedReal

Mathlib prefers ⊥ to denote the -∞ element.

Equations

• Chapter5.ExtendedReal.inst_Bot = { bot := Chapter5.ExtendedReal.infty }

instance Chapter5.ExtendedReal.coe_real : Coe Real ExtendedReal

Equations

• Chapter5.ExtendedReal.coe_real = { coe := fun (x : Chapter5.Real) => Chapter5.ExtendedReal.real x }

instance Chapter5.ExtendedReal.real_coe : Coe ExtendedReal Real

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Chapter5.ExtendedReal.is_finite (X : ExtendedReal) : Prop

Equations

• Chapter5.ExtendedReal.neg_infty.is_finite = False
• (Chapter5.ExtendedReal.real x).is_finite = True
• Chapter5.ExtendedReal.infty.is_finite = False

theorem Chapter5.ExtendedReal.finite_eq_coe {X : ExtendedReal} (hX : X.is_finite) : X = real (match X with | neg_infty => 0 | real x => x | infty => 0)

@[reducible, inline]

noncomputable abbrev Chapter5.ExtendedReal.sup (E : Set Real) : ExtendedReal

Визначення 5.5.10 (Supremum)

Equations

• Chapter5.ExtendedReal.sup E = if h1 : E.Nonempty then if h2 : BddAbove E then Chapter5.ExtendedReal.real ⋯.choose else ⊤ else ⊥

theorem Chapter5.ExtendedReal.sup_of_empty : sup ∅ = ⊥

Визначення 5.5.10 (Supremum)

theorem Chapter5.ExtendedReal.sup_of_unbounded {E : Set Real} (hb : ¬BddAbove E) : sup E = ⊤

Визначення 5.5.10 (Supremum)

theorem Chapter5.ExtendedReal.sup_of_bounded {E : Set Real} (hnon : E.Nonempty) (hb : BddAbove E) : IsLUB E (match sup E with | neg_infty => 0 | real x => x | infty => 0)

Визначення 5.5.10 (Supremum)

theorem Chapter5.ExtendedReal.sup_of_bounded_finite {E : Set Real} (hnon : E.Nonempty) (hb : BddAbove E) : (sup E).is_finite

theorem Chapter5.Real.exist_sqrt_two : ∃ (x : Real), x ^ 2 = 2

Твердження 5.5.12

theorem Chapter5.Real.exist_irrational : ∃ (x : Real), ¬∃ (q : ℚ), x = ↑q

Ремарка 5.5.13

theorem Chapter5.Real.GLB_exist {E : Set Real} (hE : E.Nonempty) (hbound : BddBelow E) : ∃ (S : Real), IsGLB E S

@[reducible, inline]

noncomputable abbrev Chapter5.ExtendedReal.inf (E : Set Real) : ExtendedReal

Equations

• Chapter5.ExtendedReal.inf E = if h1 : E.Nonempty then if h2 : BddBelow E then Chapter5.ExtendedReal.real ⋯.choose else ⊥ else ⊤

theorem Chapter5.ExtendedReal.inf_of_empty : inf ∅ = ⊤

theorem Chapter5.ExtendedReal.inf_of_unbounded {E : Set Real} (hb : ¬BddBelow E) : inf E = ⊥

theorem Chapter5.ExtendedReal.inf_of_bounded {E : Set Real} (hnon : E.Nonempty) (hb : BddBelow E) : IsGLB E (match inf E with | neg_infty => 0 | real x => x | infty => 0)

theorem Chapter5.ExtendedReal.inf_of_bounded_finite {E : Set Real} (hnon : E.Nonempty) (hb : BddBelow E) : (inf E).is_finite

theorem Chapter5.Real.mem_neg (E : Set Real) (x : Real) : x ∈ -E ↔ -x ∈ E

Helper lemma for Exercise 5.5.1.

theorem Chapter5.Real.inf_neg {E : Set Real} {M : Real} (h : IsLUB E M) : IsGLB (-E) (-M)

Вправа 5.5.1

theorem Chapter5.Real.irrat_between {x y : Real} (hxy : x < y) : ∃ (z : Real), x < z ∧ z < y ∧ ¬∃ (q : ℚ), z = ↑q

Вправа 5.5.5

noncomputable instance Chapter5.Real.inst_SupSet : SupSet Real

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance Chapter5.Real.inst_conditionallyCompleteLattice : ConditionallyCompleteLattice Real

Use the sSup operation to build a conditionally complete lattice structure on Real

Equations

• One or more equations did not get rendered due to their size.

theorem Chapter5.ExtendedReal.sSup_of_bounded {E : Set Real} (hnon : E.Nonempty) (hb : BddAbove E) : IsLUB E (sSup E)