Analysis I, Appendix B.2: The decimal representation of real numbers

An implementation of the decimal representation of Mathlib's real numbers ℝ.

This is separate from the way decimal numerals are already represented in Mathlib. We also represent the integer part of the natural numbers just by ℕ, avoiding using the decimal representation from the previous section, although we still retain the Digit class.

structure AppendixB.NNRealDecimal : Type

• intPart : ℕ
• fracPart : ℕ → Digit

noncomputable def AppendixB.NNRealDecimal.toNNReal (d : NNRealDecimal) : NNReal

Equations

• ↑d = ↑d.intPart + ∑' (i : ℕ), ↑↑(d.fracPart i) * 10 ^ (-↑i - 1)

noncomputable instance AppendixB.NNRealDecimal.instCoeNNReal : Coe NNRealDecimal NNReal

Equations

• AppendixB.NNRealDecimal.instCoeNNReal = { coe := AppendixB.NNRealDecimal.toNNReal }

theorem AppendixB.NNRealDecimal.toNNReal_conv (d : NNRealDecimal) : Summable fun (i : ℕ) => ↑↑(d.fracPart i) * 10 ^ (-↑i - 1)

Exercise B.2.1

theorem AppendixB.NNRealDecimal.surj (x : NNReal) : ∃ (d : NNRealDecimal), x = ↑d

theorem AppendixB.NNRealDecimal.not_inj : 1 = ↑{ intPart := 1, fracPart := fun (x : ℕ) => 0 } ∧ 1 = ↑{ intPart := 0, fracPart := fun (x : ℕ) => 9 }

Proposition B.2.2

inductive AppendixB.RealDecimal : Type

• pos : NNRealDecimal → RealDecimal
• neg : NNRealDecimal → RealDecimal

noncomputable instance AppendixB.RealDecimal.instCoeReal : Coe RealDecimal ℝ

Equations

• AppendixB.RealDecimal.instCoeReal = { coe := fun (d : AppendixB.RealDecimal) => match d with | AppendixB.RealDecimal.pos d => ↑↑d | AppendixB.RealDecimal.neg d => -↑↑d }

theorem AppendixB.RealDecimal.surj (x : ℝ) : ∃ (d : RealDecimal), x = match d with | pos d => ↑↑d | neg d => -↑↑d

theorem AppendixB.RealDecimal.not_inj_one (d : RealDecimal) : (match d with | pos d => ↑↑d | neg d => -↑↑d) = 1 ↔ d = pos { intPart := 1, fracPart := fun (x : ℕ) => 0 } ∨ d = pos { intPart := 0, fracPart := fun (x : ℕ) => 9 }

Exercise B.2.2

@[reducible, inline]

abbrev AppendixB.TerminatingDecimal (x : ℝ) : Prop

Exercise B.2.3

Equations

• AppendixB.TerminatingDecimal x = ∃ (n : ℤ) (m : ℕ), x = ↑n / 10 ^ m

theorem AppendixB.RealDecimal.not_inj_terminating {x : ℝ} (hx : TerminatingDecimal x) : ∃ (d₁ : RealDecimal) (d₂ : RealDecimal), d₁ ≠ d₂ ∧ ∀ (d : RealDecimal), (match d with | pos d => ↑↑d | neg d => -↑↑d) = x ↔ d = d₁ ∨ d = d₂

theorem AppendixB.RealDecimal.inj_nonterminating {x : ℝ} (hx : ¬TerminatingDecimal x) : ∃! d : RealDecimal, (match d with | pos d => ↑↑d | neg d => -↑↑d) = x