class Chapter5.CauchySequenceextends Chapter5.Sequence : Type

A class of Cauchy sequences that start at zero.

• n₀ : ℤ
• seq : ℤ → ℚ
• vanish (n : ℤ) : n < self.n₀ → self.seq n = 0
• zero : self.n₀ = 0
• cauchy : self.IsCauchy

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

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

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

@[reducible, inline]

abbrev Chapter5.CauchySequence.mk' {a : ℕ → ℚ} (ha : (↑a).IsCauchy) : CauchySequence

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

Equations

• Chapter5.CauchySequence.mk' ha = { n₀ := 0, seq := (↑a).seq, vanish := ⋯, zero := Chapter5.CauchySequence.mk'._proof_2, cauchy := ha }

@[simp]

theorem Chapter5.CauchySequence.coe_eq {a : ℕ → ℚ} (ha : (↑a).IsCauchy) : (mk' ha).toSequence = ↑a

@[implicit_reducible]

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

Equations

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

@[simp]

theorem Chapter5.CauchySequence.coe_to_sequence (a : CauchySequence) : (↑fun (n : ℕ) => a.seq ↑n) = a.toSequence

@[simp]

theorem Chapter5.CauchySequence.coe_coe {a : ℕ → ℚ} (ha : (↑a).IsCauchy) : (fun (n : ℕ) => (mk' ha).seq ↑n) = a

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

Proposition 5.3.3 / Exercise 5.3.1

@[implicit_reducible]

instance Chapter5.CauchySequence.instSetoid : Setoid CauchySequence

Proposition 5.3.3 / Exercise 5.3.1

Equations

• Chapter5.CauchySequence.instSetoid = { r := fun (a b : Chapter5.CauchySequence) => Chapter5.Sequence.Equiv (fun (n : ℕ) => a.seq ↑n) fun (n : ℕ) => b.seq ↑n, iseqv := ⋯ }

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

theorem Chapter5.Sequence.IsCauchy.const (a : ℚ) : (↑fun (x : ℕ) => a).IsCauchy

Every constant sequence is Cauchy.

@[implicit_reducible]

instance Chapter5.CauchySequence.instZero : Zero CauchySequence

Equations

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

@[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 : (↑a).IsCauchy then Chapter5.CauchySequence.mk' h else 0⟧

theorem Chapter5.LIM_def {a : ℕ → ℚ} (ha : (↑a).IsCauchy) : LIM a = ⟦CauchySequence.mk' ha⟧

theorem Chapter5.Real.eq_lim (x : Real) : ∃ (a : ℕ → ℚ), (↑a).IsCauchy ∧ x = LIM a

Definition 5.3.1 (Real numbers)

theorem Chapter5.Real.LIM_eq_LIM {a b : ℕ → ℚ} (ha : (↑a).IsCauchy) (hb : (↑b).IsCauchy) : LIM a = LIM b ↔ Sequence.Equiv a b

Definition 5.3.1 (Real numbers)

theorem Chapter5.Sequence.IsCauchy.add {a b : ℕ → ℚ} (ha : (↑a).IsCauchy) (hb : (↑b).IsCauchy) : (↑(a + b)).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)

@[implicit_reducible]

noncomputable instance Chapter5.Real.add_inst : Add Real

Definition 5.3.4 (Addition of reals)

Equations

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

theorem Chapter5.Real.LIM_add {a b : ℕ → ℚ} (ha : (↑a).IsCauchy) (hb : (↑b).IsCauchy) : LIM a + LIM b = LIM (a + b)

Definition 5.3.4 (Addition of reals)

theorem Chapter5.Sequence.IsCauchy.mul {a b : ℕ → ℚ} (ha : (↑a).IsCauchy) (hb : (↑b).IsCauchy) : (↑(a * b)).IsCauchy

Proposition 5.3.10 (Product of Cauchy sequences is Cauchy)

theorem Chapter5.Sequence.mul_equiv_left {a a' : ℕ → ℚ} (b : ℕ → ℚ) (hb : (↑b).IsCauchy) (haa' : Equiv a a') : Equiv (a * b) (a' * b)

Proposition 5.3.10 (Product of equivalent sequences is equivalent) / Exercise 5.3.2

theorem Chapter5.Sequence.mul_equiv_right {b b' : ℕ → ℚ} (a : ℕ → ℚ) (ha : (↑a).IsCauchy) (hbb' : Equiv b b') : Equiv (a * b) (a * b')

Proposition 5.3.10 (Product of equivalent sequences is equivalent) / Exercise 5.3.2

theorem Chapter5.Sequence.mul_equiv {a b a' b' : ℕ → ℚ} (ha : (↑a).IsCauchy) (hb' : (↑b').IsCauchy) (haa' : Equiv a a') (hbb' : Equiv b b') : Equiv (a * b) (a' * b')

Proposition 5.3.10 (Product of equivalent sequences is equivalent) / Exercise 5.3.2

@[implicit_reducible]

noncomputable instance Chapter5.Real.mul_inst : Mul Real

Definition 5.3.9 (Product of reals)

Equations

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

theorem Chapter5.Real.LIM_mul {a b : ℕ → ℚ} (ha : (↑a).IsCauchy) (hb : (↑b).IsCauchy) : LIM a * LIM b = LIM (a * b)

@[implicit_reducible]

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

Exercise 5.3.3

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Chapter5.Real.instIntCast : IntCast Real

Equations

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

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

ratCast distributes over addition

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

ratCast distributes over multiplication

@[implicit_reducible]

noncomputable instance Chapter5.Real.instNeg : Neg Real

Equations

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

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

ratCast commutes with negation

theorem Chapter5.Real.neg_LIM (a : ℕ → ℚ) (ha : (↑a).IsCauchy) : -LIM a = LIM (-a)

It may be possible to omit the IsCauchy hypothesis here.

theorem Chapter5.Sequence.IsCauchy.neg (a : ℕ → ℚ) (ha : (↑a).IsCauchy) : (↑(-a)).IsCauchy

@[implicit_reducible]

noncomputable instance Chapter5.Real.addGroup_inst : AddGroup Real

Proposition 5.3.11 (laws of algebra)

Equations

• Chapter5.Real.addGroup_inst = AddGroup.ofLeftAxioms ⋯ ⋯ ⋯

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

theorem Chapter5.Sequence.IsCauchy.sub {a b : ℕ → ℚ} (ha : (↑a).IsCauchy) (hb : (↑b).IsCauchy) : (↑(a - b)).IsCauchy

theorem Chapter5.Real.LIM_sub {a b : ℕ → ℚ} (ha : (↑a).IsCauchy) (hb : (↑b).IsCauchy) : LIM a - LIM b = LIM (a - b)

LIM distributes over subtraction

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

ratCast distributes over subtraction

@[implicit_reducible]

noncomputable instance Chapter5.Real.instAddCommGroup : AddCommGroup Real

Proposition 5.3.11 (laws of algebra)

Equations

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

@[implicit_reducible]

noncomputable instance Chapter5.Real.instCommMonoid : CommMonoid Real

Proposition 5.3.11 (laws of algebra)

Equations

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

@[implicit_reducible]

noncomputable instance Chapter5.Real.instCommRing : CommRing Real

Proposition 5.3.11 (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

• Chapter5.Real.ratCast_hom = { toFun := RatCast.ratCast, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[reducible, inline]

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

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

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

theorem Chapter5.Real.boundedAwayZero_of_nonzero {x : Real} (hx : x ≠ 0) : ∃ (a : ℕ → ℚ), (↑a).IsCauchy ∧ BoundedAwayZero a ∧ x = LIM a

Lemma 5.3.14

theorem Chapter5.Real.lim_of_boundedAwayZero {a : ℕ → ℚ} (ha : BoundedAwayZero a) (ha_cauchy : (↑a).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.nonzero_of_boundedAwayZero {a : ℕ → ℚ} (ha : BoundedAwayZero a) (n : ℕ) : a n ≠ 0

theorem Chapter5.Real.inv_isCauchy_of_boundedAwayZero {a : ℕ → ℚ} (ha : BoundedAwayZero a) (ha_cauchy : (↑a).IsCauchy) : (↑a⁻¹).IsCauchy

Lemma 5.3.15

theorem Chapter5.Real.inv_of_equiv {a b : ℕ → ℚ} (ha : BoundedAwayZero a) (ha_cauchy : (↑a).IsCauchy) (hb : BoundedAwayZero b) (hb_cauchy : (↑b).IsCauchy) (hlim : LIM a = LIM b) : LIM a⁻¹ = LIM b⁻¹

Lemma 5.3.17 (Reciprocation is well-defined)

@[implicit_reducible]

noncomputable instance Chapter5.Real.instInv : Inv Real

Definition 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 : BoundedAwayZero a) (hc : (↑a).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.BoundedAwayZero.const {q : ℚ} (hq : q ≠ 0) : BoundedAwayZero fun (x : ℕ) => q

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

@[implicit_reducible]

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⁻¹

@[implicit_reducible]

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.IsBounded.equiv {a b : ℕ → ℚ} (ha : (↑a).IsBounded) (hab : Sequence.Equiv a b) : (↑b).IsBounded

Exercise 5.3.4

theorem Chapter5.Sequence.IsCauchy.harmonic' : (↑fun (n : ℕ) => 1 / (↑n + 1)).IsCauchy

Same as Sequence.IsCauchy.harmonic but reindexing the sequence as a₀ = 1, a₁ = 1/2, ... This form is more convenient for the upcoming proof of Theorem 5.5.9.

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

Exercise 5.3.5