Documentation

Analysis.Section_5_4

Analysis I, Section 5.4: Ordering the reals #

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

Tips from past users #

Users of the companion who have completed the exercises in this section are welcome to send their tips for future users in this section as PRs.

(Add tip here)

@[reducible, inline]

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

Definition 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.BoundedAwayPos a = ∃ c > 0, ∀ (n : ℕ), a n ≥ c

Instances For

@[reducible, inline]

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

Definition 5.4.1 (sequences bounded away from zero with sign).

Equations

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

Instances For

theorem Chapter5.boundedAwayPos_def (a : ℕ → ℚ) :

BoundedAwayPos a ↔ ∃ c > 0, ∀ (n : ℕ), a n ≥ c

Definition 5.4.1 (sequences bounded away from zero with sign).

theorem Chapter5.boundedAwayNeg_def (a : ℕ → ℚ) :

BoundedAwayNeg a ↔ ∃ c > 0, ∀ (n : ℕ), a n ≤ -c

Definition 5.4.1 (sequences bounded away from zero with sign).

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) :

Equations

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

Instances For

@[reducible, inline]

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

Equations

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

Instances For

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

Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1

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

¬(x = 0 ∧ x.IsPos)

Proposition 5.4.4 (basic properties of positive reals) / Exercise 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)

Proposition 5.4.4 (basic properties of positive reals) / Exercise 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)

Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1

@[simp]

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

x.IsNeg ↔ (-x).IsPos

Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1

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

(x + y).IsPos

Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1

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

(x * y).IsPos

Proposition 5.4.4 (basic properties of positive reals) / Exercise 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) :

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

Instances For

@[simp]

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

x.abs = x

Definition 5.4.5 (absolute value)

@[simp]

theorem Chapter5.Real.abs_of_neg (x : Real) (hx : x.IsNeg) :

x.abs = -x

Definition 5.4.5 (absolute value)

@[simp]

theorem Chapter5.Real.abs_of_zero :

abs 0 = 0

Definition 5.4.5 (absolute value)

instance Chapter5.Real.instLT :

Definition 5.4.6 (Ordering of the reals)

Equations

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

instance Chapter5.Real.instLE :

Definition 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

Proposition 5.4.7(a) (order trichotomy) / Exercise 5.4.2

theorem Chapter5.Real.not_gt_and_lt (x y : Real) :

¬(x > y ∧ x < y)

Proposition 5.4.7(a) (order trichotomy) / Exercise 5.4.2

theorem Chapter5.Real.not_gt_and_eq (x y : Real) :

¬(x > y ∧ x = y)

Proposition 5.4.7(a) (order trichotomy) / Exercise 5.4.2

theorem Chapter5.Real.not_lt_and_eq (x y : Real) :

¬(x < y ∧ x = y)

Proposition 5.4.7(a) (order trichotomy) / Exercise 5.4.2

theorem Chapter5.Real.antisymm (x y : Real) :

x < y ↔ (y - x).IsPos

Proposition 5.4.7(b) (order is anti-symmetric) / Exercise 5.4.2

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

x < z

Proposition 5.4.7(c) (order is transitive) / Exercise 5.4.2

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

x + z < y + z

Proposition 5.4.7(d) (addition preserves order) / Exercise 5.4.2

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

x * z < y * z

Proposition 5.4.7(e) (positive multiplication preserves order) / Exercise 5.4.2

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

z * x ≤ z * y

Proposition 5.4.7(e) (positive multiplication preserves order) / Exercise 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

(Not from textbook) 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.abs_eq_abs (x : Real) :

(Not from textbook) Linear Orders come with a definition of absolute value |.| Show that it agrees with our earlier definition.

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

Proposition 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

(Not from textbook) Real has the structure of a strict ordered ring.

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

Proposition 5.4.9 (The non-negative reals are closed)

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

LIM a ≤ LIM b

Corollary 5.4.10

theorem Chapter5.Real.LIM_mono_fail :

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

Remark 5.4.11 -

theorem Chapter5.Real.exists_rat_le_and_nat_ge {x : Real} (hx : x.IsPos) :

(∃ q > 0, ↑q ≤ x) ∧ ∃ (N : ℕ), x < ↑N

Proposition 5.4.12 (Bounding reals by rationals)

theorem Chapter5.Real.le_mul {ε : Real} (hε : ε.IsPos) (x : Real) :

∃ M > 0, ↑M * ε > x

Corollary 5.4.13 (Archimedean property )

theorem Chapter5.Real.rat_between {x y : Real} (hxy : x < y) :

∃ (q : ℚ), x < ↑q ∧ ↑q < y

Proposition 5.4.14 / Exercise 5.4.5

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

∃! n : ℤ , ↑n ≤ x ∧ x < ↑n + 1

Exercise 5.4.3

theorem Chapter5.Real.exist_inv_nat_le {x : Real} (hx : x.IsPos) :

∃ N > 0, (↑N)⁻¹ < x

Exercise 5.4.4

theorem Chapter5.Real.dist_lt_iff (ε x y : Real) :

|x - y| < ε ↔ y - ε < x ∧ x < y + ε

Exercise 5.4.6

theorem Chapter5.Real.dist_le_iff (ε x y : Real) :

|x - y| ≤ ε ↔ y - ε ≤ x ∧ x ≤ y + ε

Exercise 5.4.6

theorem Chapter5.Real.le_add_eps_iff (x y : Real) :

(∀ ε > 0, x ≤ y + ε) ↔ x ≤ y

Exercise 5.4.7

theorem Chapter5.Real.dist_le_eps_iff (x y : Real) :

(∀ ε > 0, |x - y| ≤ ε) ↔ x = y

Exercise 5.4.7

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

Exercise 5.4.8

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

Exercise 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)

Exercise 5.4.9

theorem Chapter5.Real.neg_min (x y : Real) :

min x y = -max (-x) (-y)

Exercise 5.4.9

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

max x y = max y x

Exercise 5.4.9

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

max x x = x

Exercise 5.4.9

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

max (x + z) (y + z) = max x y + z

Exercise 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

Exercise 5.4.9

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

min x y = min y x

Exercise 5.4.9

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

min x x = x

Exercise 5.4.9

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

min (x + z) (y + z) = min x y + z

Exercise 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

Exercise 5.4.9

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

(max x y)⁻¹ = min x⁻¹ y⁻¹

Exercise 5.4.9

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

(min x y)⁻¹ = max x⁻¹ y⁻¹

Exercise 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_1 }

Instances For