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

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:

• Notion of a formal limit of a Cauchy sequence
• Construction of a real number type Chapter5.Real
• Basic arithmetic operations and properties

class Chapter5.CauchySequenceextends Chapter5.Sequence : Type

A class of Cauchy sequences that start at zero

• n₀ : ℤ
• seq : ℤ → ℚ
• vanish (n : ℤ) : n < CauchySequence.toSequence.n₀ → CauchySequence.toSequence.seq n = 0
• zero : toSequence.n₀ = 0
• cauchy : toSequence.isCauchy

theorem Chapter5.CauchySequence.ext {x y : CauchySequence} (n₀ : toSequence.n₀ = toSequence.n₀) (seq : toSequence.seq = toSequence.seq) : x = y

theorem Chapter5.CauchySequence.ext_iff {x y : CauchySequence} : x = y ↔ toSequence.n₀ = toSequence.n₀ ∧ toSequence.seq = toSequence.seq

theorem Chapter5.CauchySequence.ext' {a b : CauchySequence} (h : toSequence.seq = toSequence.seq) : a = b

@[reducible, inline]

abbrev Chapter5.CauchySequence.mk' {a : ℕ → ℚ} (ha : { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy) : CauchySequence

A sequence starting at zero that is Cauchy, can be viewed as a Cauchy sequence.

Equations

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

@[simp]

theorem Chapter5.CauchySequence.coe_eq {a : ℕ → ℚ} (ha : { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy) : toSequence = { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }

instance Chapter5.CauchySequence.instCoeFun : CoeFun CauchySequence fun (x : CauchySequence) => ℕ → ℚ

Equations

• Chapter5.CauchySequence.instCoeFun = { coe := fun (a : Chapter5.CauchySequence) (n : ℕ) => Chapter5.CauchySequence.toSequence.seq ↑n }

@[simp]

theorem Chapter5.CauchySequence.coe_to_sequence (a : CauchySequence) : { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => toSequence.seq ↑n) n.toNat else 0, vanish := ⋯ } = toSequence

@[simp]

theorem Chapter5.CauchySequence.coe_coe {a : ℕ → ℚ} (ha : { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy) : (fun (n : ℕ) => toSequence.seq ↑n) = a

theorem Chapter5.Sequence.equiv_trans {a b c : ℕ → ℚ} (hab : equiv a b) (hbc : equiv b c) : equiv a c

Твердження 5.3.3 / Вправа 5.3.1

instance Chapter5.CauchySequence.instSetoid : Setoid CauchySequence

Твердження 5.3.3 / Вправа 5.3.1

Equations

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

theorem Chapter5.CauchySequence.equiv_iff (a b : CauchySequence) : a ≈ b ↔ Sequence.equiv (fun (n : ℕ) => toSequence.seq ↑n) fun (n : ℕ) => toSequence.seq ↑n

theorem Chapter5.Sequence.isCauchy_of_const (a : ℚ) : { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => a) n.toNat else 0, vanish := ⋯ }.isCauchy

Every constant sequence is Cauchy

instance Chapter5.CauchySequence.instZero : Zero CauchySequence

Equations

• Chapter5.CauchySequence.instZero = { zero := Chapter5.CauchySequence.mk' Chapter5.CauchySequence.instZero._proof_5 }

@[reducible, inline]

abbrev Chapter5.Real : Type

Equations

• Chapter5.Real = Quotient Chapter5.CauchySequence.instSetoid

@[reducible, inline]

noncomputable abbrev Chapter5.LIM (a : ℕ → ℚ) : Real

It is convenient in Lean to assign the "dummy" value of 0 to LIM a when a is not Cauchy. This requires Classical logic, because the property of being Cauchy is not computable or decidable.

Equations

• Chapter5.LIM a = ⟦if h : { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy then Chapter5.CauchySequence.mk' h else 0⟧

theorem Chapter5.LIM_def {a : ℕ → ℚ} (ha : { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy) : LIM a = ⟦CauchySequence.mk' ha⟧

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

Визначення 5.3.1 (Real numbers)

theorem Chapter5.Real.LIM_eq_LIM {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) : LIM a = LIM b ↔ Sequence.equiv a b

Визначення 5.3.1 (Real numbers)

theorem Chapter5.Sequence.add_cauchy {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) : { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then (a + b) n.toNat else 0, vanish := ⋯ }.isCauchy

Lemma 5.3.6 (Sum of Cauchy sequences is Cauchy)

theorem Chapter5.Sequence.add_equiv_left {a a' : ℕ → ℚ} (b : ℕ → ℚ) (haa' : equiv a a') : equiv (a + b) (a' + b)

Lemma 5.3.7 (Sum of equivalent sequences is equivalent)

theorem Chapter5.Sequence.add_equiv_right {b b' : ℕ → ℚ} (a : ℕ → ℚ) (hbb' : equiv b b') : equiv (a + b) (a + b')

Lemma 5.3.7 (Sum of equivalent sequences is equivalent)

theorem Chapter5.Sequence.add_equiv {a b a' b' : ℕ → ℚ} (haa' : equiv a a') (hbb' : equiv b b') : equiv (a + b) (a' + b')

Lemma 5.3.7 (Sum of equivalent sequences is equivalent)

noncomputable instance Chapter5.Real.add_inst : Add Real

Визначення 5.3.4 (Addition of reals)

Equations

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

theorem Chapter5.Real.add_of_LIM {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) : LIM a + LIM b = LIM (a + b)

Визначення 5.3.4 (Addition of reals)

theorem Chapter5.Sequence.mul_cauchy {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) : { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then (a * b) n.toNat else 0, vanish := ⋯ }.isCauchy

Твердження 5.3.10 (Product of Cauchy sequences is Cauchy)

theorem Chapter5.Sequence.mul_equiv_left {a a' : ℕ → ℚ} (b : ℕ → ℚ) (haa' : equiv a a') : equiv (a * b) (a' * b)

Твердження 5.3.10 (Product of equivalent sequences is equivalent) / Вправа 5.3.2

theorem Chapter5.Sequence.mul_equiv_right {b b' : ℕ → ℚ} (a : ℕ → ℚ) (hbb' : equiv b b') : equiv (a * b) (a * b')

Proposition 5.3.10 (Product of equivalent sequences is equivalent) / Вправа 5.3.2

theorem Chapter5.Sequence.mul_equiv {a b a' b' : ℕ → ℚ} (haa' : equiv a a') (hbb' : equiv b b') : equiv (a * b) (a' * b')

Proposition 5.3.10 (Product of equivalent sequences is equivalent) / Вправа 5.3.2

noncomputable instance Chapter5.Real.mul_inst : Mul Real

Визначення 5.3.9 (Product of reals)

Equations

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

theorem Chapter5.Real.mul_of_LIM {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) : LIM a * LIM b = LIM (a * b)

instance Chapter5.Real.instRatCast : RatCast Real

Equations

• Chapter5.Real.instRatCast = { ratCast := fun (q : ℚ) => ⟦Chapter5.CauchySequence.mk' ⋯⟧ }

theorem Chapter5.Real.ratCast_def (q : ℚ) : ↑q = LIM fun (x : ℕ) => q

@[simp]

theorem Chapter5.Real.ratCast_inj (q r : ℚ) : ↑q = ↑r ↔ q = r

Вправа 5.3.3

instance Chapter5.Real.instOfNat {n : ℕ} : OfNat Real n

Equations

• Chapter5.Real.instOfNat = { ofNat := ↑↑n }

instance Chapter5.Real.instNatCast : NatCast Real

Equations

• Chapter5.Real.instNatCast = { natCast := fun (n : ℕ) => ↑↑n }

@[simp]

theorem Chapter5.Real.LIM_zero : (LIM fun (x : ℕ) => 0) = 0

instance Chapter5.Real.instIntCast : IntCast Real

Equations

• Chapter5.Real.instIntCast = { intCast := fun (n : ℤ) => ↑↑n }

theorem Chapter5.Real.add_of_ratCast (a b : ℚ) : ↑a + ↑b = ↑(a + b)

theorem Chapter5.Real.mul_of_ratCast (a b : ℚ) : ↑a * ↑b = ↑(a * b)

noncomputable instance Chapter5.Real.instNeg : Neg Real

Equations

• Chapter5.Real.instNeg = { neg := fun (x : Chapter5.Real) => ↑(-1) * x }

theorem Chapter5.Real.neg_of_ratCast (a : ℚ) : -↑a = ↑(-a)

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

It may be possible to omit the Cauchy sequence hypothesis here.

theorem Chapter5.Real.neg_of_cauchy (a : ℕ → ℚ) (ha : { 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 (-a) n.toNat else 0, vanish := ⋯ }.isCauchy

noncomputable instance Chapter5.Real.addGroup_inst : AddGroup Real

Твердження 5.3.11

Equations

• Chapter5.Real.addGroup_inst = AddGroup.ofLeftAxioms Chapter5.Real.addGroup_inst._proof_9 Chapter5.Real.addGroup_inst._proof_10 Chapter5.Real.addGroup_inst._proof_11

theorem Chapter5.Real.sub_eq_add_neg (x y : Real) : x - y = x + -y

theorem Chapter5.Real.sub_of_cauchy {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) : { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then (a - b) n.toNat else 0, vanish := ⋯ }.isCauchy

theorem Chapter5.Real.sub_of_LIM {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) : LIM a - LIM b = LIM (a - b)

theorem Chapter5.Real.sub_of_ratCast (a b : ℚ) : ↑a - ↑b = ↑(a - b)

noncomputable instance Chapter5.Real.instAddCommGroup : AddCommGroup Real

Твердження 5.3.12 (laws of algebra)

Equations

• Chapter5.Real.instAddCommGroup = { toAddGroup := Chapter5.Real.addGroup_inst, add_comm := Chapter5.Real.instAddCommGroup._proof_12 }

noncomputable instance Chapter5.Real.instCommMonoid : CommMonoid Real

Твердження 5.3.12 (laws of algebra)

Equations

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

noncomputable instance Chapter5.Real.instCommRing : CommRing Real

Твердження 5.3.12 (laws of algebra)

Equations

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

@[reducible, inline]

abbrev Chapter5.Real.ratCast_hom : ℚ →+* Real

Equations

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

@[reducible, inline]

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

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

Equations

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

theorem Chapter5.bounded_away_zero_def (a : ℕ → ℚ) : bounded_away_zero a ↔ ∃ c > 0, ∀ (n : ℕ), |a n| ≥ c

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

Лема 5.3.14

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

This result was not explicitly stated in the text, but is needed in the theory. It's a good exercise, so I'm setting it as such.

theorem Chapter5.Real.bounded_away_zero_nonzero {a : ℕ → ℚ} (ha : bounded_away_zero a) (n : ℕ) : a n ≠ 0

theorem Chapter5.Real.inv_of_bounded_away_zero_cauchy {a : ℕ → ℚ} (ha : bounded_away_zero a) (ha_cauchy : { 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 a⁻¹ n.toNat else 0, vanish := ⋯ }.isCauchy

Лема 5.3.15

theorem Chapter5.Real.inv_of_equiv {a b : ℕ → ℚ} (ha : bounded_away_zero a) (ha_cauchy : { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy) (hb : bounded_away_zero b) (hb_cauchy : { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchy) (hlim : LIM a = LIM b) : LIM a⁻¹ = LIM b⁻¹

Лема 5.3.17 (Reciprocation is well-defined)

noncomputable instance Chapter5.Real.instInv : Inv Real

Визначення 5.3.16 (Reciprocation of real numbers). Requires classical logic because we need to assign a "junk" value to the inverse of 0.

Equations

• Chapter5.Real.instInv = { inv := fun (x : Chapter5.Real) => if h : x ≠ 0 then Chapter5.LIM ⋯.choose⁻¹ else 0 }

theorem Chapter5.Real.inv_def {a : ℕ → ℚ} (h : bounded_away_zero a) (hc : { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy) : (LIM a)⁻¹ = LIM a⁻¹

@[simp]

theorem Chapter5.Real.inv_zero : 0⁻¹ = 0

theorem Chapter5.Real.self_mul_inv {x : Real} (hx : x ≠ 0) : x * x⁻¹ = 1

theorem Chapter5.Real.inv_mul_self {x : Real} (hx : x ≠ 0) : x * x⁻¹ = 1

theorem Chapter5.Real.inv_of_ratCast (q : ℚ) : (↑q)⁻¹ = ↑q⁻¹

noncomputable instance Chapter5.Real.instDivInvMonoid : DivInvMonoid Real

Default definition of division

Equations

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

theorem Chapter5.Real.div_eq (x y : Real) : x / y = x * y⁻¹

noncomputable instance Chapter5.Real.instField : Field Real

Equations

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

theorem Chapter5.Real.mul_right_cancel₀ {x y z : Real} (hz : z ≠ 0) (h : x * z = y * z) : x = y

theorem Chapter5.Real.mul_right_nocancel : ¬∀ (x y z : Real), z = 0 → x * z = y * z → x = y

theorem Chapter5.Real.equiv_of_bounded {a b : ℕ → ℚ} (ha : { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isBounded) (hab : Sequence.equiv a b) : { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isBounded

Вправа 5.3.4

theorem Chapter5.Real.Cauchy_of_harmonic : { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => 1 / (↑n + 1)) n.toNat else 0, vanish := ⋯ }.isCauchy

Вправа 5.3.5

theorem Chapter5.Real.LIM_of_harmonic : (LIM fun (n : ℕ) => 1 / (↑n + 1)) = 0

Вправа 5.3.5