Аналіз I, Розділ 5.4: Впорядкування дійсних чисел

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

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

• Порядок на дійсній прямій

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

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

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

@[reducible, inline]

abbrev Chapter5.BoundedAwayPos (a : ℕ → ℚ) : Prop

Визначення 5.4.1 (послідовності, обмежені від нуля з врахуванням знаку). Послідовності індексуються так, щоб починатися з нуля, оскільки це зручніше для цілей Mathlib.

Equations

• Chapter5.BoundedAwayPos a = ∃ c > 0, ∀ (n : ℕ), a n ≥ c

@[reducible, inline]

abbrev Chapter5.BoundedAwayNeg (a : ℕ → ℚ) : Prop

Визначення 5.4.1 (послідовності, обмежені від нуля з врахуванням знаку).

Equations

• Chapter5.BoundedAwayNeg a = ∃ c > 0, ∀ (n : ℕ), a n ≤ -c

theorem Chapter5.boundedAwayPos_def (a : ℕ → ℚ) : BoundedAwayPos a ↔ ∃ c > 0, ∀ (n : ℕ), a n ≥ c

Визначення 5.4.1 (послідовності, обмежені від нуля з врахуванням знаку).

theorem Chapter5.boundedAwayNeg_def (a : ℕ → ℚ) : BoundedAwayNeg a ↔ ∃ c > 0, ∀ (n : ℕ), a n ≤ -c

Визначення 5.4.1 (послідовності, обмежені від нуля з врахуванням знаку).

theorem Chapter5.BoundedAwayZero.boundedAwayPos {a : ℕ → ℚ} (ha : BoundedAwayPos a) : BoundedAwayZero a

theorem Chapter5.BoundedAwayZero.boundedAwayNeg {a : ℕ → ℚ} (ha : BoundedAwayNeg a) : BoundedAwayZero a

theorem Chapter5.not_boundedAwayPos_boundedAwayNeg {a : ℕ → ℚ} : ¬(BoundedAwayPos a ∧ BoundedAwayNeg a)

@[reducible, inline]

abbrev Chapter5.Real.IsPos (x : Real) : Prop

Equations

• x.IsPos = ∃ (a : ℕ → ℚ), Chapter5.BoundedAwayPos a ∧ (↑a).IsCauchy ∧ x = Chapter5.LIM a

@[reducible, inline]

abbrev Chapter5.Real.IsNeg (x : Real) : Prop

Equations

• x.IsNeg = ∃ (a : ℕ → ℚ), Chapter5.BoundedAwayNeg a ∧ (↑a).IsCauchy ∧ x = Chapter5.LIM a

theorem Chapter5.Real.isPos_def (x : Real) : x.IsPos ↔ ∃ (a : ℕ → ℚ), BoundedAwayPos a ∧ (↑a).IsCauchy ∧ x = LIM a

theorem Chapter5.Real.isNeg_def (x : Real) : x.IsNeg ↔ ∃ (a : ℕ → ℚ), BoundedAwayNeg a ∧ (↑a).IsCauchy ∧ x = LIM a

theorem Chapter5.Real.trichotomous (x : Real) : x = 0 ∨ x.IsPos ∨ x.IsNeg

Твердження 5.4.4 (базові властивості додатних дійсних чисел) / Вправа 5.4.1

theorem Chapter5.Real.not_zero_pos (x : Real) : ¬(x = 0 ∧ x.IsPos)

Твердження 5.4.4 (базові властивості додатних дійсних чисел) / Вправа 5.4.1

theorem Chapter5.Real.nonzero_of_pos {x : Real} (hx : x.IsPos) : x ≠ 0

theorem Chapter5.Real.not_zero_neg (x : Real) : ¬(x = 0 ∧ x.IsNeg)

Твердження 5.4.4 (базові властивості додатних дійсних чисел) / Вправа 5.4.1

theorem Chapter5.Real.nonzero_of_neg {x : Real} (hx : x.IsNeg) : x ≠ 0

theorem Chapter5.Real.not_pos_neg (x : Real) : ¬(x.IsPos ∧ x.IsNeg)

Твердження 5.4.4 (базові властивості додатних дійсних чисел) / Вправа 5.4.1

@[simp]

theorem Chapter5.Real.neg_iff_pos_of_neg (x : Real) : x.IsNeg ↔ (-x).IsPos

Твердження 5.4.4 (базові властивості додатних дійсних чисел) / Вправа 5.4.1

theorem Chapter5.Real.pos_add {x y : Real} (hx : x.IsPos) (hy : y.IsPos) : (x + y).IsPos

Твердження 5.4.4 (базові властивості додатних дійсних чисел) / Вправа 5.4.1

theorem Chapter5.Real.pos_mul {x y : Real} (hx : x.IsPos) (hy : y.IsPos) : (x * y).IsPos

Твердження 5.4.4 (базові властивості додатних дійсних чисел) / Вправа 5.4.1

theorem Chapter5.Real.pos_of_coe (q : ℚ) : (↑q).IsPos ↔ q > 0

theorem Chapter5.Real.neg_of_coe (q : ℚ) : (↑q).IsNeg ↔ q < 0

@[reducible, inline]

noncomputable abbrev Chapter5.Real.abs (x : Real) : Real

Тут потрібно використовувати класичну логіку, оскільки isPos і isNeg не є вирішуваними.

Equations

• x.abs = if x.IsPos then x else if x.IsNeg then -x else 0

@[simp]

theorem Chapter5.Real.abs_of_pos (x : Real) (hx : x.IsPos) : x.abs = x

Визначення 5.4.5 (модуль)

@[simp]

theorem Chapter5.Real.abs_of_neg (x : Real) (hx : x.IsNeg) : x.abs = -x

Визначення 5.4.5 (модуль)

@[simp]

theorem Chapter5.Real.abs_of_zero : abs 0 = 0

Визначення 5.4.5 (модуль)

instance Chapter5.Real.instLT : LT Real

Визначення 5.4.6 (Упорядкування дійсних чисел)

Equations

• Chapter5.Real.instLT = { lt := fun (x y : Chapter5.Real) => (x - y).IsNeg }

instance Chapter5.Real.instLE : LE Real

Визначення 5.4.6 (Упорядкування дійсних чисел)

Equations

• Chapter5.Real.instLE = { le := fun (x y : Chapter5.Real) => x < y ∨ x = y }

theorem Chapter5.Real.lt_iff (x y : Real) : x < y ↔ (x - y).IsNeg

theorem Chapter5.Real.le_iff (x y : Real) : x ≤ y ↔ x < y ∨ x = y

theorem Chapter5.Real.gt_iff (x y : Real) : x > y ↔ (x - y).IsPos

theorem Chapter5.Real.ge_iff (x y : Real) : x ≥ y ↔ x > y ∨ x = y

theorem Chapter5.Real.lt_of_coe (q q' : ℚ) : q < q' ↔ ↑q < ↑q'

theorem Chapter5.Real.gt_of_coe (q q' : ℚ) : q > q' ↔ ↑q > ↑q'

theorem Chapter5.Real.isPos_iff (x : Real) : x.IsPos ↔ x > 0

theorem Chapter5.Real.isNeg_iff (x : Real) : x.IsNeg ↔ x < 0

theorem Chapter5.Real.trichotomous' (x y : Real) : x > y ∨ x < y ∨ x = y

Твердження 5.4.7(a) (трихотомія порядку) / Вправа 5.4.2

theorem Chapter5.Real.not_gt_and_lt (x y : Real) : ¬(x > y ∧ x < y)

Твердження 5.4.7(a) (трихотомія порядку) / Вправа 5.4.2

theorem Chapter5.Real.not_gt_and_eq (x y : Real) : ¬(x > y ∧ x = y)

Твердження 5.4.7(a) (трихотомія порядку) / Вправа 5.4.2

theorem Chapter5.Real.not_lt_and_eq (x y : Real) : ¬(x < y ∧ x = y)

Твердження 5.4.7(a) (трихотомія порядку) / Вправа 5.4.2

theorem Chapter5.Real.antisymm (x y : Real) : x < y ↔ y > x

Твердження 5.4.7(b) (порядок є антисиметричним) / Вправа 5.4.2

theorem Chapter5.Real.lt_trans {x y z : Real} (hxy : x < y) (hyz : y < z) : x < z

Твердження 5.4.7(c) (порядок є транзитивним) / Вправа 5.4.2

theorem Chapter5.Real.add_lt_add_right {x y : Real} (z : Real) (hxy : x < y) : x + z < y + z

Твердження 5.4.7(d) (додавання зберігає порядок) / Вправа 5.4.2

theorem Chapter5.Real.mul_lt_mul_right {x y z : Real} (hxy : x < y) (hz : z.IsPos) : x * z < y * z

Твердження 5.4.7(e) (множення на додатне число зберігає порядок) / Вправа 5.4.2

theorem Chapter5.Real.mul_le_mul_left {x y z : Real} (hxy : x ≤ y) (hz : z.IsPos) : z * x ≤ z * y

Твердження 5.4.7(e) (множення на додатне число зберігає порядок) / Вправа 5.4.2

theorem Chapter5.Real.mul_pos_neg {x y : Real} (hx : x.IsPos) (hy : y.IsNeg) : (x * y).IsNeg

noncomputable instance Chapter5.Real.instLinearOrder : LinearOrder Real

(Не в підручнику) Дійсні числа мають структуру лінійного впорядкування. Це впорядкування не є обчислюваним, тому для забезпечення розв'язності необхідна класична логіка.

Equations

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

theorem Chapter5.Real.abs_eq_abs (x : Real) : |x| = x.abs

(Не в підручнику) Лінійні впорядкування включають визначення абсолютного значення |·|. Покажіть, що воно збігається з нашим попереднім визначенням.

theorem Chapter5.Real.inv_of_pos {x : Real} (hx : x.IsPos) : x⁻¹.IsPos

Твердження 5.4.8

theorem Chapter5.Real.div_of_pos {x y : Real} (hx : x.IsPos) (hy : y.IsPos) : (x / y).IsPos

theorem Chapter5.Real.inv_of_gt {x y : Real} (hx : x.IsPos) (hy : y.IsPos) (hxy : x > y) : x⁻¹ < y⁻¹

instance Chapter5.Real.instIsStrictOrderedRing : IsStrictOrderedRing Real

(Не в підручнику) Дійсні числа мають структуру строго впорядкованого кільця.

theorem Chapter5.Real.LIM_of_nonneg {a : ℕ → ℚ} (ha : ∀ (n : ℕ), a n ≥ 0) (hcauchy : (↑a).IsCauchy) : LIM a ≥ 0

Твердження 5.4.9 (Невід'ємні дійсні числа утворюють замкнену множину.)

theorem Chapter5.Real.LIM_mono {a b : ℕ → ℚ} (ha : (↑a).IsCauchy) (hb : (↑b).IsCauchy) (hmono : ∀ (n : ℕ), a n ≤ b n) : LIM a ≤ LIM b

Наслідок 5.4.10

theorem Chapter5.Real.LIM_mono_fail : ∃ (a : ℕ → ℚ) (b : ℕ → ℚ), (↑a).IsCauchy ∧ (↑b).IsCauchy ∧ (∀ (n : ℕ), a n > b n) ∧ ¬LIM a > LIM b

Зауваження 5.4.11 -

theorem Chapter5.Real.exists_rat_le_and_nat_gt {x : Real} (hx : x.IsPos) : (∃ q > 0, ↑q ≤ x) ∧ ∃ (N : ℕ), x < ↑N

Твердження 5.4.12 (Обмеження дійсних чисел раціональними)

theorem Chapter5.Real.le_mul {ε : Real} (hε : ε.IsPos) (x : Real) : ∃ M > 0, ↑M * ε > x

Наслідок 5.4.13 (Архімедова властивість )

theorem Chapter5.Real.rat_between {x y : Real} (hxy : x < y) : ∃ (q : ℚ), x < ↑q ∧ ↑q < y

Твердження 5.4.14 / Вправа 5.4.5

theorem Chapter5.Real.floor_exist (x : Real) : ∃! n : ℤ, ↑n ≤ x ∧ x < ↑n + 1

Вправа 5.4.3

theorem Chapter5.Real.exist_inv_nat_le {x : Real} (hx : x.IsPos) : ∃ N > 0, (↑N)⁻¹ < x

Вправа 5.4.4

theorem Chapter5.Real.dist_lt_iff (ε x y : Real) : |x - y| < ε ↔ y - ε < x ∧ x < y + ε

Вправа 5.4.6

theorem Chapter5.Real.dist_le_iff (ε x y : Real) : |x - y| ≤ ε ↔ y - ε ≤ x ∧ x ≤ y + ε

Вправа 5.4.6

theorem Chapter5.Real.le_add_eps_iff (x y : Real) : (∀ ε > 0, x ≤ y + ε) ↔ x ≤ y

Вправа 5.4.7

theorem Chapter5.Real.dist_le_eps_iff (x y : Real) : (∀ ε > 0, |x - y| ≤ ε) ↔ x = y

Вправа 5.4.7

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

Вправа 5.4.8

theorem Chapter5.Real.LIM_of_ge {x : Real} {a : ℕ → ℚ} (hcauchy : (↑a).IsCauchy) (h : ∀ (n : ℕ), ↑(a n) ≥ x) : LIM a ≥ x

Вправа 5.4.8

theorem Chapter5.Real.max_eq (x y : Real) : max x y = if x ≥ y then x else y

theorem Chapter5.Real.min_eq (x y : Real) : min x y = if x ≤ y then x else y

theorem Chapter5.Real.neg_max (x y : Real) : max x y = -min (-x) (-y)

Вправа 5.4.9

theorem Chapter5.Real.neg_min (x y : Real) : min x y = -max (-x) (-y)

Вправа 5.4.9

theorem Chapter5.Real.max_comm (x y : Real) : max x y = max y x

Вправа 5.4.9

theorem Chapter5.Real.max_self (x : Real) : max x x = x

Вправа 5.4.9

theorem Chapter5.Real.max_add (x y z : Real) : max (x + z) (y + z) = max x y + z

Вправа 5.4.9

theorem Chapter5.Real.max_mul (x y : Real) {z : Real} (hz : z.IsPos) : max (x * z) (y * z) = max x y * z

Вправа 5.4.9

theorem Chapter5.Real.min_comm (x y : Real) : min x y = min y x

Вправа 5.4.9

theorem Chapter5.Real.min_self (x : Real) : min x x = x

Вправа 5.4.9

theorem Chapter5.Real.min_add (x y z : Real) : min (x + z) (y + z) = min x y + z

Вправа 5.4.9

theorem Chapter5.Real.min_mul (x y : Real) {z : Real} (hz : z.IsPos) : min (x * z) (y * z) = min x y * z

Вправа 5.4.9

theorem Chapter5.Real.inv_max {x y : Real} (hx : x.IsPos) (hy : y.IsPos) : (max x y)⁻¹ = min x⁻¹ y⁻¹

Вправа 5.4.9

theorem Chapter5.Real.inv_min {x y : Real} (hx : x.IsPos) (hy : y.IsPos) : (min x y)⁻¹ = max x⁻¹ y⁻¹

Вправа 5.4.9

@[reducible, inline]

abbrev Chapter5.Real.ratCast_ordered_hom : ℚ →+*o Real

Не з підручника: раціональні числа вкладаються в дійсні як гомоморфізм впорядкованих кілець.

Equations

• Chapter5.Real.ratCast_ordered_hom = { toRingHom := Chapter5.Real.ratCast_hom, monotone' := Chapter5.Real.ratCast_ordered_hom._proof_1 }