Analysis I, Section 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

namespace Chapter5

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.

abbrev bounded_away_pos (a:ℕ → ℚ) : Prop := ∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≥ c

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

abbrev bounded_away_neg (a:ℕ → ℚ) : Prop := ∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≤ -c

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

theorem bounded_away_pos_def (a:ℕ → ℚ) : bounded_away_pos a ↔ ∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≥ c := bya:ℕ → ℚ⊢ bounded_away_pos a ↔ ∃ c > 0, ∀ (n : ℕ), a n ≥ c rflAll goals completed! 🐙

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

theorem bounded_away_neg_def (a:ℕ → ℚ) : bounded_away_neg a ↔ ∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≤ -c := bya:ℕ → ℚ⊢ bounded_away_neg a ↔ ∃ c > 0, ∀ (n : ℕ), a n ≤ -c rflAll goals completed! 🐙

Examples 5.4.2

declaration uses 'sorry'example : bounded_away_pos (fun n ↦ 1 + 10^(-(n:ℤ)-1)) := by⊢ bounded_away_pos fun n => 1 + 10 ^ (-↑n - 1) sorryAll goals completed! 🐙

Examples 5.4.2

declaration uses 'sorry'example : bounded_away_neg (fun n ↦ - - 10^(-(n:ℤ)-1)) := by⊢ bounded_away_neg fun n => - -10 ^ (-↑n - 1) sorryAll goals completed! 🐙

Examples 5.4.2

declaration uses 'sorry'example : ¬ bounded_away_pos (fun n ↦ (-1)^n) := by⊢ ¬bounded_away_pos fun n => (-1) ^ n sorryAll goals completed! 🐙declaration uses 'sorry'example : ¬ bounded_away_neg (fun n ↦ (-1)^n) := by⊢ ¬bounded_away_neg fun n => (-1) ^ n sorryAll goals completed! 🐙declaration uses 'sorry'example : bounded_away_zero (fun n ↦ (-1)^n) := by⊢ bounded_away_zero fun n => (-1) ^ n sorryAll goals completed! 🐙theorem declaration uses 'sorry'bounded_away_zero_of_pos {a:ℕ → ℚ} (ha: bounded_away_pos a) : bounded_away_zero a := bya:ℕ → ℚha:bounded_away_pos a⊢ bounded_away_zero a sorryAll goals completed! 🐙theorem declaration uses 'sorry'bounded_away_zero_of_neg {a:ℕ → ℚ} (ha: bounded_away_neg a) : bounded_away_zero a := bya:ℕ → ℚha:bounded_away_neg a⊢ bounded_away_zero a sorryAll goals completed! 🐙theorem declaration uses 'sorry'not_bounded_away_pos_neg {a:ℕ → ℚ} : ¬ (bounded_away_pos a ∧ bounded_away_neg a) := bya:ℕ → ℚ⊢ ¬(bounded_away_pos a ∧ bounded_away_neg a) sorryAll goals completed! 🐙abbrev Real.isPos (x:Real) : Prop := ∃ a:ℕ → ℚ, bounded_away_pos a ∧ (a:Sequence).isCauchy ∧ x = LIM aabbrev Real.isNeg (x:Real) : Prop := ∃ a:ℕ → ℚ, bounded_away_neg a ∧ (a:Sequence).isCauchy ∧ x = LIM a

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

theorem declaration uses 'sorry'Real.trichotomous (x:Real) : x = 0 ∨ x.isPos ∨ x.isNeg := byx:Real⊢ x = 0 ∨ x.isPos ∨ x.isNeg sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'Real.not_zero_pos (x:Real) : ¬ (x = 0 ∧ x.isPos) := byx:Real⊢ ¬(x = 0 ∧ x.isPos) sorryAll goals completed! 🐙theorem Real.nonzero_of_pos {x:Real} (hx: x.isPos) : x ≠ 0 := byx:Realhx:x.isPos⊢ x ≠ 0 have := not_zero_pos xx:Realhx:x.isPosthis:¬(x = 0 ∧ x.isPos)⊢ x ≠ 0 simp [hx] at this ⊢x:Realhx:x.isPosthis:¬x = 0⊢ ¬x = 0 assumptionAll goals completed! 🐙

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

theorem declaration uses 'sorry'Real.not_zero_neg (x:Real) : ¬ (x = 0 ∧ x.isNeg) := byx:Real⊢ ¬(x = 0 ∧ x.isNeg) sorryAll goals completed! 🐙theorem Real.nonzero_of_neg {x:Real} (hx: x.isNeg) : x ≠ 0 := byx:Realhx:x.isNeg⊢ x ≠ 0 have := not_zero_neg xx:Realhx:x.isNegthis:¬(x = 0 ∧ x.isNeg)⊢ x ≠ 0 simp [hx] at this ⊢x:Realhx:x.isNegthis:¬x = 0⊢ ¬x = 0 assumptionAll goals completed! 🐙

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

theorem declaration uses 'sorry'Real.not_pos_neg (x:Real) : ¬ (x.isPos ∧ x.isNeg) := byx:Real⊢ ¬(x.isPos ∧ x.isNeg) sorryAll goals completed! 🐙

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

@[simp] theorem declaration uses 'sorry'Real.neg_iff_pos_of_neg (x:Real) : x.isNeg ↔ (-x).isPos := byx:Real⊢ x.isNeg ↔ (-x).isPos sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'Real.pos_add {x y:Real} (hx: x.isPos) (hy: y.isPos) : (x+y).isPos := byx:Realy:Realhx:x.isPoshy:y.isPos⊢ (x + y).isPos sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'Real.pos_mul {x y:Real} (hx: x.isPos) (hy: y.isPos) : (x*y).isPos := byx:Realy:Realhx:x.isPoshy:y.isPos⊢ (x * y).isPos sorryAll goals completed! 🐙theorem declaration uses 'sorry'Real.pos_of_coe (q:ℚ) : (q:Real).isPos ↔ q > 0 := byq:ℚ⊢ (↑q).isPos ↔ q > 0 sorryAll goals completed! 🐙theorem declaration uses 'sorry'Real.neg_of_coe (q:ℚ) : (q:Real).isNeg ↔ q < 0 := byq:ℚ⊢ (↑q).isNeg ↔ q < 0 sorryAll goals completed! 🐙open Classical in /-- Need to use classical logic here because isPos and isNeg are not decidable -/ noncomputable abbrev Real.abs (x:Real) : Real := if x.isPos then x else (if x.isNeg then -x else 0)

Definition 5.4.5 (absolute value)

@[simp] theorem Real.abs_of_pos (x:Real) (hx: x.isPos) : Real.abs x = x := byx:Realhx:x.isPos⊢ x.abs = x simp [Real.abs, hx]All goals completed! 🐙

Definition 5.4.5 (absolute value)

@[simp] theorem Real.abs_of_neg (x:Real) (hx: x.isNeg) : Real.abs x = -x := byx:Realhx:x.isNeg⊢ x.abs = -x have : ¬ x.isPos := byx:Realhx:x.isNeg⊢ x.abs = -x have := Real.not_pos_neg xx:Realhx:x.isNegthis:¬(x.isPos ∧ x.isNeg)⊢ ¬x.isPos; simp only [hx, and_true] at thisx:Realhx:x.isNegthis:¬x.isPos⊢ ¬x.isPos; assumptionAll goals completed! 🐙 simp [Real.abs, hx, this]All goals completed! 🐙

Definition 5.4.5 (absolute value)

@[simp] theorem Real.abs_of_zero : Real.abs 0 = 0 := by⊢ abs 0 = 0 have hpos: ¬ (0:Real).isPos := by⊢ abs 0 = 0 have := Real.not_zero_pos 0this:¬(0 = 0 ∧ isPos 0)⊢ ¬isPos 0; simp only [true_and] at thisthis:¬isPos 0⊢ ¬isPos 0; assumptionAll goals completed! 🐙 have hneg: ¬ (0:Real).isNeg := by⊢ abs 0 = 0 have := Real.not_zero_neg 0hpos:¬isPos 0this:¬(0 = 0 ∧ isNeg 0)⊢ ¬isNeg 0; simp only [true_and] at thishpos:¬isPos 0this:¬isNeg 0⊢ ¬isNeg 0; assumptionAll goals completed! 🐙 simp [Real.abs, hpos, hneg]All goals completed! 🐙

Definition 5.4.6 (Ordering of the reals)

instance Real.instLT : LT Real where lt x y := (x-y).isNeg

Definition 5.4.6 (Ordering of the reals)

instance Real.instLE : LE Real where le x y := (x < y) ∨ (x = y)theorem Real.lt_iff (x y:Real) : x < y ↔ (x-y).isNeg := byx:Realy:Real⊢ x < y ↔ (x - y).isNeg rflAll goals completed! 🐙theorem Real.le_iff (x y:Real) : x ≤ y ↔ (x < y) ∨ (x = y) := byx:Realy:Real⊢ x ≤ y ↔ x < y ∨ x = y rflAll goals completed! 🐙theorem declaration uses 'sorry'Real.gt_iff (x y:Real) : x > y ↔ (x-y).isPos := byx:Realy:Real⊢ x > y ↔ (x - y).isPos sorryAll goals completed! 🐙theorem declaration uses 'sorry'Real.ge_iff (x y:Real) : x ≥ y ↔ (x > y) ∨ (x = y) := byx:Realy:Real⊢ x ≥ y ↔ x > y ∨ x = y sorryAll goals completed! 🐙theorem declaration uses 'sorry'Real.lt_of_coe (q q':ℚ): q < q' ↔ (q:Real) < (q':Real) := byq:ℚq':ℚ⊢ q < q' ↔ ↑q < ↑q' sorryAll goals completed! 🐙theorem Real.gt_of_coe (q q':ℚ): q > q' ↔ (q:Real) > (q':Real) := Real.lt_of_coe _ _

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

theorem declaration uses 'sorry'Real.trichotomous' (x y z:Real) : x > y ∨ x < y ∨ x = y := byx:Realy:Realz:Real⊢ x > y ∨ x < y ∨ x = y sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'Real.not_gt_and_lt (x y:Real) : ¬ (x > y ∧ x < y):= byx:Realy:Real⊢ ¬(x > y ∧ x < y) sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'Real.not_gt_and_eq (x y:Real) : ¬ (x > y ∧ x = y):= byx:Realy:Real⊢ ¬(x > y ∧ x = y) sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'Real.not_lt_and_eq (x y:Real) : ¬ (x < y ∧ x = y):= byx:Realy:Real⊢ ¬(x < y ∧ x = y) sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'Real.antisymm (x y:Real) : x < y ↔ (y - x).isPos := byx:Realy:Real⊢ x < y ↔ (y - x).isPos sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'Real.lt_trans {x y z:Real} (hxy: x < y) (hyz: y < z) : x < z := byx:Realy:Realz:Realhxy:x < yhyz:y < z⊢ x < z sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'Real.add_lt_add_right {x y:Real} (z:Real) (hxy: x < y) : x + z < y + z := byx:Realy:Realz:Realhxy:x < y⊢ x + z < y + z sorryAll goals completed! 🐙

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

theorem Real.mul_lt_mul_right {x y z:Real} (hxy: x < y) (hz: z.isPos) : x * z < y * z := byx:Realy:Realz:Realhxy:x < yhz:z.isPos⊢ x * z < y * z rw [antisymm] at hxy ⊢x:Realy:Realz:Realhxy:(y - x).isPoshz:z.isPos⊢ (y * z - x * z).isPos convert pos_mul hxy hz using 1h.e'_1x:Realy:Realz:Realhxy:(y - x).isPoshz:z.isPos⊢ y * z - x * z = (y - x) * z ringAll goals completed! 🐙

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

theorem declaration uses 'sorry'Real.mul_le_mul_left {x y z:Real} (hxy: x ≤ y) (hz: z.isPos) : z * x ≤ z * y := byx:Realy:Realz:Realhxy:x ≤ yhz:z.isPos⊢ z * x ≤ z * y sorryAll goals completed! 🐙theorem declaration uses 'sorry'Real.mul_pos_neg {x y:Real} (hx: x.isPos) (hy: y.isNeg) : (x * y).isNeg := byx:Realy:Realhx:x.isPoshy:y.isNeg⊢ (x * y).isNeg sorryAll goals completed! 🐙

(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.

noncomputable instance declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Real.instLinearOrder : LinearOrder Real where le_refl := sorry le_trans := sorry lt_iff_le_not_le := sorry le_antisymm := sorry le_total := sorry toDecidableLE := by⊢ DecidableLE Real classical exact Classical.decRel _All goals completed! 🐙

Proposition 5.4.8

theorem Real.inv_of_pos {x:Real} (hx: x.isPos) : x⁻¹.isPos := byx:Realhx:x.isPos⊢ x⁻¹.isPos have hnon: x ≠ 0 := nonzero_of_pos hxx:Realhx:x.isPoshnon:x ≠ 0⊢ x⁻¹.isPos have hident := inv_mul_self hnonx:Realhx:x.isPoshnon:x ≠ 0hident:x * x⁻¹ = 1⊢ x⁻¹.isPos have hinv_non: x⁻¹ ≠ 0 := byx:Realhx:x.isPos⊢ x⁻¹.isPos contrapose! hidentx:Realhx:x.isPoshnon:x ≠ 0hident:x⁻¹ = 0⊢ x * x⁻¹ ≠ 1; simp [hident]All goals completed! 🐙 have hnonneg : ¬ x⁻¹.isNeg := byx:Realhx:x.isPos⊢ x⁻¹.isPos intro hx:Realhx:x.isPoshnon:x ≠ 0hident:x * x⁻¹ = 1hinv_non:x⁻¹ ≠ 0h:x⁻¹.isNeg⊢ False have := mul_pos_neg hx hx:Realhx:x.isPoshnon:x ≠ 0hident:x * x⁻¹ = 1hinv_non:x⁻¹ ≠ 0h:x⁻¹.isNegthis:(x * x⁻¹).isNeg⊢ False have id : -(1:Real) = (-1:ℚ) := byx:Realhx:x.isPos⊢ x⁻¹.isPos simpAll goals completed! 🐙 simp only [hident, neg_iff_pos_of_neg, id, pos_of_coe] at thisx:Realhx:x.isPoshnon:x ≠ 0hident:x * x⁻¹ = 1hinv_non:x⁻¹ ≠ 0h:x⁻¹.isNegid:-1 = ↑(-1)this:-1 > 0⊢ False linarithAll goals completed! 🐙 have trich := Real.trichotomous x⁻¹x:Realhx:x.isPoshnon:x ≠ 0hident:x * x⁻¹ = 1hinv_non:x⁻¹ ≠ 0hnonneg:¬x⁻¹.isNegtrich:x⁻¹ = 0 ∨ x⁻¹.isPos ∨ x⁻¹.isNeg⊢ x⁻¹.isPos simp [hinv_non, hnonneg] at trichx:Realhx:x.isPoshnon:x ≠ 0hident:x * x⁻¹ = 1hinv_non:x⁻¹ ≠ 0hnonneg:¬x⁻¹.isNegtrich:x⁻¹.isPos⊢ x⁻¹.isPos assumptionAll goals completed! 🐙theorem Real.inv_of_gt {x y:Real} (hx: x.isPos) (hy: y.isPos) (hxy: x > y) : x⁻¹ < y⁻¹ := byx:Realy:Realhx:x.isPoshy:y.isPoshxy:x > y⊢ x⁻¹ < y⁻¹ have hxnon: x ≠ 0 := nonzero_of_pos hxx:Realy:Realhx:x.isPoshy:y.isPoshxy:x > yhxnon:x ≠ 0⊢ x⁻¹ < y⁻¹ have hynon: y ≠ 0 := nonzero_of_pos hyx:Realy:Realhx:x.isPoshy:y.isPoshxy:x > yhxnon:x ≠ 0hynon:y ≠ 0⊢ x⁻¹ < y⁻¹ have hxinv : x⁻¹.isPos := inv_of_pos hxx:Realy:Realhx:x.isPoshy:y.isPoshxy:x > yhxnon:x ≠ 0hynon:y ≠ 0hxinv:x⁻¹.isPos⊢ x⁻¹ < y⁻¹ have hyinv : y⁻¹.isPos := inv_of_pos hyx:Realy:Realhx:x.isPoshy:y.isPoshxy:x > yhxnon:x ≠ 0hynon:y ≠ 0hxinv:x⁻¹.isPoshyinv:y⁻¹.isPos⊢ x⁻¹ < y⁻¹ by_contra! thisx:Realy:Realhx:x.isPoshy:y.isPoshxy:x > yhxnon:x ≠ 0hynon:y ≠ 0hxinv:x⁻¹.isPoshyinv:y⁻¹.isPosthis:y⁻¹ ≤ x⁻¹⊢ False have : (1:Real) > 1 := calc 1 = x * x⁻¹ := (inv_mul_self hxnon).symm _ > y * x⁻¹ := mul_lt_mul_right hxy hxinv _ ≥ y * y⁻¹ := mul_le_mul_left this hy _ = _ := inv_mul_self hynonx:Realy:Realhx:x.isPoshy:y.isPoshxy:x > yhxnon:x ≠ 0hynon:y ≠ 0hxinv:x⁻¹.isPoshyinv:y⁻¹.isPosthis✝:y⁻¹ ≤ x⁻¹this:1 > 1⊢ False simp at thisAll goals completed! 🐙

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

instance declaration uses 'sorry'Real.instIsStrictOrderedRing : IsStrictOrderedRing Real where add_le_add_left := by⊢ ∀ (a b : Real), a ≤ b → ∀ (c : Real), c + a ≤ c + b sorryAll goals completed! 🐙 add_le_add_right := by⊢ ∀ (a b : Real), a ≤ b → ∀ (c : Real), a + c ≤ b + c sorryAll goals completed! 🐙 mul_lt_mul_of_pos_left := by⊢ ∀ (a b c : Real), a < b → 0 < c → c * a < c * b sorryAll goals completed! 🐙 mul_lt_mul_of_pos_right := by⊢ ∀ (a b c : Real), a < b → 0 < c → a * c < b * c sorryAll goals completed! 🐙 le_of_add_le_add_left := by⊢ ∀ (a b c : Real), a + b ≤ a + c → b ≤ c sorryAll goals completed! 🐙 zero_le_one := by⊢ 0 ≤ 1 sorryAll goals completed! 🐙

Proposition 5.4.9 (The non-negative reals are closed)

theorem declaration uses 'sorry'Real.LIM_of_nonneg {a: ℕ → ℚ} (ha: ∀ n, a n ≥ 0) (hcauchy: (a:Sequence).isCauchy) : LIM a ≥ 0 := bya:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy⊢ LIM a ≥ 0 sorryAll goals completed! 🐙 --TODO

Corollary 5.4.10

theorem declaration uses 'sorry'Real.LIM_mono {a b:ℕ → ℚ} (ha: (a:Sequence).isCauchy) (hb: (b:Sequence).isCauchy) (hmono: ∀ n, a n ≤ b n) : LIM a ≤ LIM b := bya:ℕ → ℚb:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhmono:∀ (n : ℕ), a n ≤ b n⊢ LIM a ≤ LIM b sorryAll goals completed! 🐙 --TODO

Remark 5.4.11 -

theorem declaration uses 'sorry'Real.LIM_mono_fail : ∃ (a b:ℕ → ℚ), (a:Sequence).isCauchy ∧ (b:Sequence).isCauchy ∧ ¬ (∀ n, a n > b n) ∧ ¬ LIM a > LIM b := by⊢ ∃ 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 use (fun n ↦ 1 + 1/(n:ℚ))h⊢ ∃ b, { n₀ := 0, seq := fun n => if n ≥ 0 then (fun n => 1 + 1 / ↑n) n.toNat else 0, vanish := ⋯ }.isCauchy ∧ { n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchy ∧ (¬∀ (n : ℕ), (fun n => 1 + 1 / ↑n) n > b n) ∧ ¬(LIM fun n => 1 + 1 / ↑n) > LIM b use (fun n ↦ 1 - 1/(n:ℚ))h⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then 1 + 1 / ↑n.toNat else 0, vanish := ⋯ }.isCauchy ∧ { n₀ := 0, seq := fun n => if n ≥ 0 then (fun n => 1 - 1 / ↑n) n.toNat else 0, vanish := ⋯ }.isCauchy ∧ (¬∀ (n : ℕ), 1 + 1 / ↑n > (fun n => 1 - 1 / ↑n) n) ∧ ¬(LIM fun n => 1 + 1 / ↑n) > LIM fun n => 1 - 1 / ↑n sorryAll goals completed! 🐙end Chapter5