Documentation

@[reducible, inline]

abbrev IsCauchy (x : MyNat → MyRat) :

Equations

IsCauchy x = ∀ (ε : MyRat), 0 < ε → ∃ (N : MyNat), ∀ (p q : MyNat), N ≤ p → N ≤ q → |x p - x q| ≤ ε

Instances For

theorem IsCauchy.bounded {x : MyNat → MyRat} (hx : IsCauchy x) :

∃ (B : MyRat), 0 < B ∧ ∀ (n : MyNat), |x n| ≤ B

@[reducible, inline]

abbrev MyPrereal :

Type

Equations

MyPrereal = { x : MyNat → MyRat // IsCauchy x }

Instances For

@[implicit_reducible]

instance MyPrereal.funLike :

FunLike MyPrereal MyNat MyRat

Equations

MyPrereal.funLike = { coe := Subtype.val, coe_injective := MyPrereal.funLike._proof_1 }

theorem MyPrereal.prop (x : MyPrereal) (ε : MyRat) :

0 < ε → ∃ (N : MyNat), ∀ (p q : MyNat), N ≤ p → N ≤ q → |x p - x q| ≤ ε

@[simp]

theorem MyPrereal.coe_apply {x : MyNat → MyRat} (hx : IsCauchy x) (n : MyNat) :

⟨x, hx⟩ n = x n

theorem MyPrereal.bounded (x : MyPrereal) :

∃ (B : MyRat), 0 < B ∧ ∀ (n : MyNat), |x n| ≤ B

The equivalence relation on the pre-reals #

def MyPrereal.R (x y : MyPrereal) :

Equations

x.R y = ∀ (ε : MyRat), 0 < ε → ∃ (N : MyNat), ∀ (n : MyNat), N ≤ n → |x n - y n| ≤ ε

Instances For

theorem MyPrereal.R_def (x y : MyPrereal) :

x.R y ↔ ∀ (ε : MyRat), 0 < ε → ∃ (N : MyNat), ∀ (n : MyNat), N ≤ n → |x n - y n| ≤ ε

theorem MyPrereal.R_refl (x : MyPrereal) :

x.R x

theorem MyPrereal.R_symm {x y : MyPrereal} :

x.R y → y.R x

theorem MyPrereal.R_trans {x y z : MyPrereal} :

x.R y → y.R z → x.R z

@[implicit_reducible]

instance MyPrereal.R_equiv :

Setoid MyPrereal

Equations

MyPrereal.R_equiv = { r := MyPrereal.R, iseqv := MyPrereal.R_equiv._proof_1 }

@[simp]

theorem MyPrereal.equiv_def (x y : MyPrereal) :

x ≈ y ↔ ∀ (ε : MyRat), 0 < ε → ∃ (N : MyNat), ∀ (n : MyNat), N ≤ n → |x n - y n| ≤ ε

@[simp]

theorem MyPrereal.equiv_def' (x y : MyPrereal) :

R_equiv x y ↔ ∀ (ε : MyRat), 0 < ε → ∃ (N : MyNat), ∀ (n : MyNat), N ≤ n → |x n - y n| ≤ ε

The algebraic structure on the pre-reals #

theorem MyPrereal.IsCauchy.const (x : MyRat) :

IsCauchy fun (x_1 : MyNat) => x

@[implicit_reducible]

instance MyPrereal.zero :

Zero MyPrereal

Equations

MyPrereal.zero = { zero := ⟨0, MyPrereal.zero._proof_1 ⟩ }

@[simp]

theorem MyPrereal.zero_def (n : MyNat) :

0 n = 0

@[implicit_reducible]

instance MyPrereal.one :

One MyPrereal

Equations

MyPrereal.one = { one := ⟨1, MyPrereal.one._proof_1 ⟩ }

@[simp]

theorem MyPrereal.one_def (n : MyNat) :

1 n = 1

theorem MyPrereal.IsCauchy.neg {x : MyNat → MyRat} (hx : IsCauchy x) :

IsCauchy (-x)

@[implicit_reducible]

instance MyPrereal.instNeg :

Neg MyPrereal

Equations

MyPrereal.instNeg = { neg := fun (x : MyPrereal) => ⟨-⇑x, ⋯⟩ }

@[simp]

theorem MyPrereal.neg_def (x : MyPrereal) (n : MyNat) :

(-x) n = -x n

theorem MyPrereal.neg_quotient ⦃x x' : MyPrereal⦄ (h : x ≈ x') :

-x ≈ -x'

theorem MyPrereal.IsCauchy.add {x y : MyNat → MyRat} (hx : IsCauchy x) (hy : IsCauchy y) :

IsCauchy (x + y)

@[implicit_reducible]

instance MyPrereal.instAdd :

Add MyPrereal

Equations

MyPrereal.instAdd = { add := fun (x y : MyPrereal) => ⟨⇑x + ⇑y, ⋯⟩ }

@[implicit_reducible]

instance MyPrereal.instSub :

Sub MyPrereal

Equations

MyPrereal.instSub = { sub := fun (x y : MyPrereal) => x + -y }

@[simp]

theorem MyPrereal.add_def (x y : MyPrereal) (n : MyNat) :

(x + y) n = x n + y n

@[simp]

theorem MyPrereal.sub_def (x y : MyPrereal) (n : MyNat) :

(x - y) n = x n - y n

theorem MyPrereal.add_quotient ⦃x x' : MyPrereal⦄ (h : x ≈ x') ⦃y y' : MyPrereal⦄ (h' : y ≈ y') :

x + y ≈ x' + y'

theorem MyPrereal.IsCauchy.mul {x y : MyNat → MyRat} (hx : IsCauchy x) (hy : IsCauchy y) :

IsCauchy (x * y)

@[implicit_reducible]

instance MyPrereal.instMul :

Mul MyPrereal

Equations

MyPrereal.instMul = { mul := fun (x y : MyPrereal) => ⟨⇑x * ⇑y, ⋯⟩ }

@[simp]

theorem MyPrereal.mul_def (x y : MyPrereal) (n : MyNat) :

(x * y) n = x n * y n

theorem MyPrereal.mul_quotient ⦃x x' : MyPrereal⦄ (h : x ≈ x') ⦃y y' : MyPrereal⦄ (h' : y ≈ y') :

x * y ≈ x' * y'

theorem MyPrereal.pos_of_not_equiv_zero {x : MyPrereal} (H : ¬x ≈ 0) :

∃ (δ : MyRat), 0 < δ ∧ ∃ (N : MyNat), ∀ (n : MyNat), N ≤ n → δ < |x n|

theorem MyPrereal.IsCauchy.inv {x : MyPrereal} (H : ¬x ≈ 0) :

IsCauchy (⇑x)⁻¹

noncomputable def MyPrereal.inv (x : MyPrereal) :

MyPrereal

Equations

x.inv = if H : ¬x ≈ 0 then ⟨(⇑x)⁻¹, ⋯⟩ else 0

Instances For

@[simp]

theorem MyPrereal.inv_def {x : MyPrereal} (H : ¬x ≈ 0) (n : MyNat) :

x.inv n = (x n)⁻¹

@[simp]

theorem MyPrereal.inv_def' {x : MyPrereal} (H : ¬x ≈ 0) (n : MyNat) :

⟨(⇑x)⁻¹, ⋯⟩ n = (x n)⁻¹

theorem MyPrereal.inv_quotient ⦃x x' : MyPrereal⦄ (h : x ≈ x') :

x.inv ≈ x'.inv

The reals: definition and algebraic structure #

@[reducible, inline]

abbrev MyReal :

Type

Equations

MyReal = Quotient MyPrereal.R_equiv

Instances For

@[simp]

theorem MyReal.Quot_eq_Quotient (x : MyPrereal) :

Quot.mk (⇑MyPrereal.R_equiv) x = ⟦x⟧

@[implicit_reducible]

instance MyReal.zero :

Zero MyReal

Equations

MyReal.zero = { zero := ⟦0⟧ }

theorem MyReal.zero_def :

0 = ⟦0⟧

@[implicit_reducible]

instance MyReal.one :

One MyReal

Equations

MyReal.one = { one := ⟦1⟧ }

theorem MyReal.one_def :

1 = ⟦1⟧

def MyReal.neg :

MyReal → MyReal

Equations

MyReal.neg = Quotient.map Neg.neg MyPrereal.neg_quotient

Instances For

@[implicit_reducible]

instance MyReal.instNeg :

Neg MyReal

Equations

MyReal.instNeg = { neg := MyReal.neg }

theorem MyReal.neg_def (x : MyPrereal) :

-⟦x⟧ = ⟦-x⟧

def MyReal.add :

MyReal → MyReal → MyReal

Equations

MyReal.add = Quotient.map₂ HAdd.hAdd MyPrereal.add_quotient

Instances For

@[implicit_reducible]

instance MyReal.instAdd :

Add MyReal

Equations

MyReal.instAdd = { add := MyReal.add }

theorem MyReal.add_def (x y : MyPrereal) :

⟦x⟧ + ⟦y⟧ = ⟦x + y⟧

def MyReal.mul :

MyReal → MyReal → MyReal

Equations

MyReal.mul = Quotient.map₂ HMul.hMul MyPrereal.mul_quotient

Instances For

@[implicit_reducible]

instance MyReal.instMul :

Mul MyReal

Equations

MyReal.instMul = { mul := MyReal.mul }

theorem MyReal.mul_def (x y : MyPrereal) :

⟦x⟧ * ⟦y⟧ = ⟦x * y⟧

noncomputable def MyReal.inv :

MyReal → MyReal

Equations

MyReal.inv = Quotient.map MyPrereal.inv MyPrereal.inv_quotient

Instances For

@[implicit_reducible]

noncomputable instance MyReal.instInv :

Inv MyReal

Equations

MyReal.instInv = { inv := MyReal.inv }

theorem MyReal.inv_def (x : MyPrereal) :

(⟦x⟧)⁻¹ = ⟦x.inv⟧

def MyReal.tacticQuot_proof₁ :

Equations

MyReal.tacticQuot_proof₁ = Lean.ParserDescr.node `MyReal.tacticQuot_proof₁ 1024 (Lean.ParserDescr.nonReservedSymbol "quot_proof₁" false)

Instances For

def MyReal.tacticQuot_proof₂ :

Equations

MyReal.tacticQuot_proof₂ = Lean.ParserDescr.node `MyReal.tacticQuot_proof₂ 1024 (Lean.ParserDescr.nonReservedSymbol "quot_proof₂" false)

Instances For

def MyReal.tacticQuot_proof₃ :

Equations

MyReal.tacticQuot_proof₃ = Lean.ParserDescr.node `MyReal.tacticQuot_proof₃ 1024 (Lean.ParserDescr.nonReservedSymbol "quot_proof₃" false)

Instances For

def MyReal.tacticQuot_proof :

Equations

MyReal.tacticQuot_proof = Lean.ParserDescr.node `MyReal.tacticQuot_proof 1024 (Lean.ParserDescr.nonReservedSymbol "quot_proof" false)

Instances For

@[implicit_reducible]

instance MyReal.commRing :

CommRing MyReal

Equations

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

theorem MyReal.sub_def (x y : MyPrereal) :

⟦x⟧ - ⟦y⟧ = ⟦x - y⟧

theorem MyReal.zero_ne_one :

0 ≠ 1

theorem MyReal.mul_inv_cancel (x : MyReal) (hx : x ≠ 0) :

x * x⁻¹ = 1

@[implicit_reducible]

noncomputable instance MyReal.field :

Field MyReal

Equations

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

The map from the rationals to the reals #

def MyReal.k (x : MyRat) :

MyReal

The natural map from the rationals to the reals.

Equations

MyReal.k x = ⟦⟨fun (x_1 : MyNat) => x, ⋯⟩⟧

Instances For

@[simp]

theorem MyReal.k_zero :

k 0 = 0

@[simp]

theorem MyReal.k_one :

k 1 = 1

@[simp]

theorem MyReal.k_neg (x : MyRat) :

k (-x) = -k x

theorem MyReal.k_add (x y : MyRat) :

k (x + y) = k x + k y

theorem MyReal.k_sub (x y : MyRat) :

k (x - y) = k x - k y

theorem MyReal.k_mul (x y : MyRat) :

k (x * y) = k x * k y

theorem MyReal.k_injective :

Function.Injective k

theorem MyReal.k_inv (x : MyRat) :

k x⁻¹ = (k x)⁻¹

@[simp]

theorem MyReal.k_inj {x y : MyRat} :

k x = k y ↔ x = y

Positivity and order #

def MyPrereal.IsPos (x : MyPrereal) :

Equations

x.IsPos = ∃ (δ : MyRat), 0 < δ ∧ ∃ (N : MyNat), ∀ (n : MyNat), N ≤ n → δ ≤ x n

Instances For

theorem MyPrereal.pos_of_isPos {x : MyPrereal} (hx : x.IsPos) :

∃ (N : MyNat), ∀ (n : MyNat), N ≤ n → 0 < x n

@[simp]

theorem MyPrereal.one_pos :

IsPos 1

theorem MyPrereal.not_isPos_zero {x : MyPrereal} (hx : x ≈ 0) :

¬x.IsPos

theorem MyPrereal.not_isPos_zero' {x : MyPrereal} (hx : ⟦x⟧ = 0) :

¬x.IsPos

theorem MyPrereal.not_equiv_zero_of_isPos {x : MyPrereal} (hx : x.IsPos) :

¬x ≈ 0

theorem MyPrereal.not_equiv_zero_of_isPos' {x : MyPrereal} (hx : x.IsPos) :

⟦x⟧ ≠ 0

theorem MyPrereal.isPos_quotient ⦃x x' : MyPrereal⦄ (h : x ≈ x') (hx : x.IsPos) :

x'.IsPos

theorem MyPrereal.IsPos.add {x y : MyPrereal} (hx : x.IsPos) (hy : y.IsPos) :

(x + y).IsPos

theorem MyPrereal.IsPos.mul {x y : MyPrereal} (hx : x.IsPos) (hy : y.IsPos) :

(x * y).IsPos

def MyPrereal.IsNonneg (x : MyPrereal) :

Equations

x.IsNonneg = (x.IsPos ∨ x ≈ 0)

Instances For

theorem MyPrereal.IsNonneg_of_equiv_zero {x : MyPrereal} (hx : x ≈ 0) :

x.IsNonneg

theorem MyPrereal.IsNonneg_of_nonneg {x : MyPrereal} (N : MyNat) (hx : ∀ (n : MyNat), N ≤ n → 0 ≤ x n) :

x.IsNonneg

@[simp]

theorem MyPrereal.zero_nonneg :

IsNonneg 0

@[simp]

theorem MyPrereal.one_nonneg :

IsNonneg 1

theorem MyPrereal.isNonneg_quotient ⦃x x' : MyPrereal⦄ (h : x ≈ x') (hx : x.IsNonneg) :

x'.IsNonneg

theorem MyPrereal.eq_zero_of_isNonneg_of_isNonneg_neg {x : MyPrereal} (h : x.IsNonneg) (h' : (-x).IsNonneg) :

x ≈ 0

theorem MyPrereal.isNonneg_neg_of_not_isNonneg {x : MyPrereal} (hx : ¬x.IsNonneg) :

(-x).IsNonneg

def MyReal.IsNonneg :

MyReal → Prop

Equations

MyReal.IsNonneg = Quotient.lift MyPrereal.IsNonneg MyReal.IsNonneg._proof_1

Instances For

theorem MyReal.isNonneg_def {x : MyPrereal} :

IsNonneg ⟦x⟧ ↔ x.IsNonneg

@[simp]

theorem MyReal.zero_nonneg :

IsNonneg 0

theorem MyReal.eq_zero_of_isNonneg_of_isNonneg_neg {x : MyReal} (h : x.IsNonneg) (h' : (-x).IsNonneg) :

x = 0

theorem MyReal.IsNonneg.add {x y : MyReal} (hx : x.IsNonneg) (hy : y.IsNonneg) :

(x + y).IsNonneg

theorem MyReal.IsNonneg.mul {x y : MyReal} (hx : x.IsNonneg) (hy : y.IsNonneg) :

(x * y).IsNonneg

def MyReal.le (x y : MyReal) :

Equations

x.le y = (y - x).IsNonneg

Instances For

@[implicit_reducible]

instance MyReal.instLE :

LE MyReal

Equations

MyReal.instLE = { le := MyReal.le }

theorem MyReal.le_def (x y : MyReal) :

x ≤ y ↔ (y - x).IsNonneg

theorem MyReal.zero_le_iff_isNonneg (x : MyReal) :

0 ≤ x ↔ x.IsNonneg

theorem MyReal.le_of_eventually_le {x y : MyPrereal} (N : MyNat) (h : ∀ (n : MyNat), N ≤ n → x n ≤ y n) :

⟦x⟧ ≤ ⟦y⟧

theorem MyReal.zero_le_one :

0 ≤ 1

theorem MyReal.le_refl (x : MyReal) :

x ≤ x

theorem MyReal.le_trans (x y z : MyReal) (h1 : x ≤ y) (h2 : y ≤ z) :

x ≤ z

theorem MyReal.le_antisymm (x y : MyReal) (hxy : x ≤ y) (hyx : y ≤ x) :

x = y

@[implicit_reducible]

instance MyReal.instPartialOrder :

PartialOrder MyReal

Equations

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

instance MyReal.instZeroLEOneClass :

ZeroLEOneClass MyReal

theorem MyReal.pos_def {x : MyPrereal} :

x.IsPos ↔ 0 < ⟦x⟧

theorem MyReal.add_le_add_left (x y : MyReal) (h : x ≤ y) (t : MyReal) :

x + t ≤ y + t

theorem MyReal.mul_nonneg (x y : MyReal) (hx : 0 ≤ x) (hy : 0 ≤ y) :

0 ≤ x * y

IsOrderedAddMonoid MyReal

instance MyReal.instIsOrderedAddMonoid :

instance MyReal.instIsOrderedRing :

IsOrderedRing MyReal

theorem MyReal.k_le_iff (x y : MyRat) :

k x ≤ k y ↔ x ≤ y

theorem MyReal.k_lt_iff (x y : MyRat) :

k x < k y ↔ x < y

theorem MyReal.le_total (x y : MyReal) :

x ≤ y ∨ y ≤ x

@[implicit_reducible]

noncomputable instance MyReal.linearOrder :

LinearOrder MyReal

Equations

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

theorem MyReal.mul_pos (a b : MyReal) (ha : 0 < a) (hb : 0 < b) :

0 < a * b

IsStrictOrderedRing MyReal

instance MyReal.instIsStrictOrderedRing :

theorem MyReal.myRat_dense_rat' (x : MyReal) {ε : MyRat} (hε : 0 < ε) :

∃ (r : MyRat), |x - k r| ≤ k ε

theorem MyReal.myRat_dense_of_pos {x : MyReal} (hx : 0 < x) :

∃ (r : MyRat), 0 < r ∧ k r < x

theorem MyReal.myRat_dense_rat (x : MyReal) {ε : MyReal} (hε : 0 < ε) :

∃ (r : MyRat), |x - k r| < ε

@[reducible, inline]

abbrev MyReal.TendsTo (f : MyNat → MyReal) (x : MyReal) :

Equations

MyReal.TendsTo f x = ∀ (ε : MyReal), 0 < ε → ∃ (N : MyNat), ∀ (n : MyNat), N ≤ n → |f n - x| ≤ ε

Instances For

theorem MyReal.tendsTo_of_myRat_tendsTo {f : MyNat → MyReal} {x : MyReal} (h : ∀ (ε : MyRat), 0 < ε → ∃ (N : MyNat), ∀ (n : MyNat), N ≤ n → |f n - x| ≤ k ε) :

TendsTo f x

@[reducible, inline]

abbrev MyReal.IsConvergent (f : MyNat → MyReal) :

Equations

MyReal.IsConvergent f = ∃ (x : MyReal), MyReal.TendsTo f x

Instances For

@[reducible, inline]

abbrev MyReal.IsCauchy (f : MyNat → MyReal) :

Equations

MyReal.IsCauchy f = ∀ (ε : MyReal), 0 < ε → ∃ (N : MyNat), ∀ (p q : MyNat), N ≤ p → N ≤ q → |f p - f q| ≤ ε

Instances For

theorem MyReal.tendsTo_myRat (x : MyPrereal) :

TendsTo (fun (n : MyNat) => k (x n)) ⟦x⟧

Completeness #

theorem MyReal.ex_approx_punctual (x : MyReal) (n : MyNat) :

∃ (r : MyRat), |x - k r| < k (MyRat.i (n + 1))⁻¹

theorem MyReal.ex_approx (f : MyNat → MyReal) :

∃ (g : MyNat → MyRat), ∀ (n : MyNat), |f n - k (g n)| < k (MyRat.i (n + 1))⁻¹

noncomputable def MyReal.approx (f : MyNat → MyReal) :

MyNat → MyRat

Equations

MyReal.approx f = ⋯.choose

Instances For

theorem MyReal.approx_spec (f : MyNat → MyReal) (n : MyNat) :

|f n - k (approx f n)| < k (MyRat.i (n + 1))⁻¹

theorem MyReal.archimedean (x : MyReal) :

∃ (n : MyNat), x ≤ k (MyRat.i (n + 1))

theorem MyReal.archimedean0 {x : MyReal} (hx : 0 < x) :

∃ (n : MyNat), k (MyRat.i (n + 1))⁻¹ ≤ x

theorem MyReal.approx_cauchy {f : MyNat → MyReal} (hf : IsCauchy f) :

_root_.IsCauchy (approx f)

noncomputable def MyReal.IsCauchy.approx {f : MyNat → MyReal} (hf : IsCauchy f) :

MyPrereal

Equations

hf.approx = ⟨MyReal.approx f, ⋯⟩

Instances For

theorem MyReal.IsCauchy.approx_spec {f : MyNat → MyReal} (hf : IsCauchy f) (n : MyNat) :

|f n - k (hf.approx n)| < k (MyRat.i (n + 1))⁻¹