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

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:

• Ordering on the real line

@[reducible, inline]

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

Визначення 5.4.1 (sequences bounded away from zero with sign). Sequences are indexed to start from zero as this is more convenient for Mathlib purposes.

Equations

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

@[reducible, inline]

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

Визначення 5.4.1 (sequences bounded away from zero with sign).

Equations

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

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

Визначення 5.4.1 (sequences bounded away from zero with sign).

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

Визначення 5.4.1 (sequences bounded away from zero with sign).

theorem Chapter5.bounded_away_zero_of_pos {a : ℕ → ℚ} (ha : bounded_away_pos a) : bounded_away_zero a

theorem Chapter5.bounded_away_zero_of_neg {a : ℕ → ℚ} (ha : bounded_away_neg a) : bounded_away_zero a

theorem Chapter5.not_bounded_away_pos_neg {a : ℕ → ℚ} : ¬(bounded_away_pos a ∧ bounded_away_neg a)

@[reducible, inline]

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

Equations

• x.isPos = ∃ (a : ℕ → ℚ), Chapter5.bounded_away_pos a ∧ { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ∧ x = Chapter5.LIM a

@[reducible, inline]

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

Equations

• x.isNeg = ∃ (a : ℕ → ℚ), Chapter5.bounded_away_neg a ∧ { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ∧ x = Chapter5.LIM a

theorem Chapter5.Real.isPos_def (x : Real) : x.isPos ↔ ∃ (a : ℕ → ℚ), bounded_away_pos a ∧ { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ∧ x = LIM a

theorem Chapter5.Real.isNeg_def (x : Real) : x.isNeg ↔ ∃ (a : ℕ → ℚ), bounded_away_neg a ∧ { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ∧ x = LIM a

theorem Chapter5.Real.trichotomous (x : Real) : x = 0 ∨ x.isPos ∨ x.isNeg

Твердження 5.4.4 (basic properties of positive reals) / Вправа 5.4.1

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

Твердження 5.4.4 (basic properties of positive reals) / Вправа 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 (basic properties of positive reals) / Вправа 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 (basic properties of positive reals) / Вправа 5.4.1

@[simp]

theorem Chapter5.Real.neg_iff_pos_of_neg (x : Real) : x.isNeg ↔ (-x).isPos

Твердження 5.4.4 (basic properties of positive reals) / Вправа 5.4.1

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

Твердження 5.4.4 (basic properties of positive reals) / Вправа 5.4.1

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

Твердження 5.4.4 (basic properties of positive reals) / Вправа 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

Need to use classical logic here because isPos and isNeg are not decidable

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 (absolute value)

@[simp]

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

Визначення 5.4.5 (absolute value)

@[simp]

theorem Chapter5.Real.abs_of_zero : abs 0 = 0

Визначення 5.4.5 (absolute value)

instance Chapter5.Real.instLT : LT Real

Визначення 5.4.6 (Ordering of the reals)

Equations

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

instance Chapter5.Real.instLE : LE Real

Визначення 5.4.6 (Ordering of the reals)

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) (order trichotomy) / Вправа 5.4.2

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

Твердження 5.4.7(a) (order trichotomy) / Вправа 5.4.2

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

Твердження 5.4.7(a) (order trichotomy) / Вправа 5.4.2

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

Твердження 5.4.7(a) (order trichotomy) / Вправа 5.4.2

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

Твердження 5.4.7(b) (order is anti-symmetric) / Вправа 5.4.2

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

Твердження 5.4.7(c) (order is transitive) / Вправа 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) (addition preserves order) / Вправа 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) (positive multiplication preserves order) / Вправа 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) (positive multiplication preserves order) / Вправа 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

(Не із книги) Real has the structure of a linear ordering. The order is not computable, and so classical logic is required to impose decidability.

Equations

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

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

(Не із книги) Real has the structure of a strict ordered ring.

theorem Chapter5.Real.LIM_of_nonneg {a : ℕ → ℚ} (ha : ∀ (n : ℕ), a n ≥ 0) (hcauchy : { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy) : LIM a ≥ 0

Твердження 5.4.9 (The non-negative reals are closed)

theorem Chapter5.Real.LIM_mono {a b : ℕ → ℚ} (ha : { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy) (hb : { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchy) (hmono : ∀ (n : ℕ), a n ≤ b n) : LIM a ≤ LIM b

Наслідок 5.4.10

theorem Chapter5.Real.LIM_mono_fail : ∃ (a : ℕ → ℚ) (b : ℕ → ℚ), { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ∧ { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchy ∧ (¬∀ (n : ℕ), a n > b n) ∧ ¬LIM a > LIM b

Ремарка 5.4.11 -

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

Твердження 5.4.12 (Bounding reals by rationals)

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

Наслідок 5.4.13 (Archimedean property )

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 : { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy) (h : ∀ (n : ℕ), ↑(a n) ≤ x) : LIM a ≤ x

Вправа 5.4.8

theorem Chapter5.Real.LIM_of_ge {x : Real} {a : ℕ → ℚ} (hcauchy : { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.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

Not from textbook: the rationals map as an ordered ring homomorphism into the reals.

Equations

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