Documentation

Analysis.Section_5_5

Аналіз I, Розділ 5.5: Властивість найменшої верхньої межі #

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

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

Верхня межа та найменша верхня межа на дійсній прямій

Підказки від попередніх користувачів #

Користувачі супровідного матеріалу, які виконали вправи в цьому розділі, можуть надсилати свої поради майбутнім користувачам цього розділу як PRи.

(Додайте підказку тут)

theorem Chapter5.Real.upperBound_def (E : Set Real) (M : Real) :

M ∈ upperBounds E ↔ ∀ x ∈ E, x ≤ M

Визначення 5.5.1 (верхні межі). Тут ми використовуємо множину upperBounds, визначену в 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 для Приклада 5.5.2

theorem Chapter5.Real.mem_Icc (x y z : Real) :

z ∈ Set.Icc x y ↔ x ≤ z ∧ z ≤ y

API для Приклада 5.5.2

theorem Chapter5.Real.Ioi_def (x : Real) :

Set.Ioi x = {z : Real | z > x}

API для Приклада 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 (найменша верхня межа). Тут ми використовуємо предикат isLUB, визначений у 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 (Єдиність найменшої верхньої межі)

theorem Chapter5.Real.bddAbove_def (E : Set Real) :

BddAbove E ↔ ∃ (M : Real), M ∈ upperBounds E

Визначення "обмежено зверху" з використанням нотації Mathlib

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.Sequence.IsCauchy.abs {a : ℕ → ℚ} (ha : (↑a).IsCauchy) :

(↑|a|).IsCauchy

Леми можуть бути корисними для доведення 5.5.4

theorem Chapter5.Real.LIM.abs_eq {a b : ℕ → ℚ} (ha : (↑a).IsCauchy) (hb : (↑b).IsCauchy) (h : LIM a = LIM b) :

LIM |a| = LIM |b|

theorem Chapter5.Real.LIM.abs_eq_pos {a : ℕ → ℚ} (h : LIM a > 0) (ha : (↑a).IsCauchy) :

LIM a = LIM |a|

theorem Chapter5.Real.LIM_abs {a : ℕ → ℚ} (ha : (↑a).IsCauchy) :

|LIM a| = LIM |a|

theorem Chapter5.Real.LIM_of_le' {x : Real} {a : ℕ → ℚ} (hcauchy : (↑a).IsCauchy) (h : ∃ (N : ℕ), ∀ n ≥ N, ↑(a n) ≤ x) :

theorem Chapter5.Real.LIM_of_Cauchy {q : ℕ → ℚ} (hq : ∀ (M n : ℕ), n ≥ M → ∀ n' ≥ M, |q n - q n'| ≤ 1 / (↑M + 1)) :

(↑q).IsCauchy ∧ ∀ (M : ℕ), |↑(q M) - LIM q| ≤ 1 / (↑M + 1)

Вправа 5.5.4

theorem Chapter5.Real.LUB_claim1 (n : ℕ) {E : Set Real} (hE : E.Nonempty) (hbound : BddAbove E) :

∃! m : ℤ , ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E

Послідовність m₁, m₂, … визначена коректно. Цей доказ використовує іншу угоду щодо індексації, ніж у тексті.

theorem Chapter5.Real.LUB_claim2 {E : Set Real} (N : ℕ) {a b : ℕ → ℚ} (hb : ∀ (n : ℕ), b n = 1 / (↑n + 1)) (hm1 : ∀ (n : ℕ), ↑(a n) ∈ upperBounds E) (hm2 : ∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds E) (n : ℕ) :

n ≥ N → ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1)

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

∃ (S : Real), IsLUB E S

Теорема 5.5.9 (Існування найменшої верхньої межі)

inductive Chapter5.ExtendedReal :

Простий розширений клас дійсної величини для визначення супремуму.

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

Instances For

instance Chapter5.ExtendedReal.inst_Top :

Top ExtendedReal

Mathlib надає перевагу ⊤ для позначення елемента +∞.

Equations

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

instance Chapter5.ExtendedReal.inst_Bot :

Bot ExtendedReal

Mathlib надає перевагу ⊥ для позначення елемента -∞.

Equations

Chapter5.ExtendedReal.inst_Bot = { bot := Chapter5.ExtendedReal.neg_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.IsFinite (X : ExtendedReal) :

Equations

Instances For

theorem Chapter5.ExtendedReal.finite_eq_coe {X : ExtendedReal} (hX : X.IsFinite) :

X = real (match X with | neg_infty => 0 | real x => x | infty => 0)

@[reducible, inline]

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

Визначення 5.5.10 (Супремум)

Equations

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

Instances For

theorem Chapter5.ExtendedReal.sup_of_empty :

Визначення 5.5.10 (Супремум)

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

Визначення 5.5.10 (Супремум)

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 (Супремум)

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

(sup E).IsFinite

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.mem_neg (E : Set Real) (x : Real) :

x ∈ -E ↔ -x ∈ E

Допоміжна лема для Вправи 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.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) :

Equations

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

Instances For

theorem Chapter5.ExtendedReal.inf_of_empty :

theorem Chapter5.ExtendedReal.inf_of_unbounded {E : Set Real} (hb : ¬BddBelow 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).IsFinite

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 :

Equations

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

noncomputable instance Chapter5.Real.inst_conditionallyCompleteLattice :

ConditionallyCompleteLattice Real

Використайте операцію sSup для побудови умовно повної ґратчастої структури на Real

Equations

Chapter5.Real.inst_conditionallyCompleteLattice = conditionallyCompleteLatticeOfLatticeOfsSup Chapter5.Real ⋯

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

IsLUB E (sSup E)