Аналіз I, Додаток B.2: Десяткове подання дійсних чисел

Реалізація десяткового подання дійсних чисел ℝ з Mathlib.

Це відокремлено від способу, у який десяткові числівники вже представлені в Mathlib. Ми також подаємо цілу частину натуральних чисел просто як ℕ, уникаючи використання десяткового подання з попереднього розділу, хоча й зберігаємо клас Digit.

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)

Вправа 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 }

Твердження 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 }

Вправа B.2.2

@[reducible, inline]

abbrev AppendixB.TerminatingDecimal (x : ℝ) : Prop

Вправа 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