Representation of reals in positional system

This file defines Real.ofDigits and Real.digits functions which allows to work with the representations of reals as sequences of digits in positional system.

Main Definitions

• ofDigits: takes a sequence of digits (d₀, d₁, ...) (as an ℕ → Fin b), and returns the real number 0.d₀d₁d₂....
• digits: takes a real number in $[0,1)$ and returns the sequence of its digits.

Main Statements

• ofDigits_digits states that ofDigits (digits x b) = x.

noncomputable def Real.ofDigitsTerm {b : ℕ} (digits : ℕ → Fin b) : ℕ → ℝ

ofDigits takes a sequence of digits (d₀, d₁, ...) in base b and returns the real number 0.d₀d₁d₂... = ∑ᵢ(dᵢ/bⁱ). This auxiliary definition ofDigitsTerm sends the sequence to the function sending i to dᵢ/bⁱ.

Equations

• Real.ofDigitsTerm digits i = ↑↑(digits i) * (↑b ^ (i + 1))⁻¹

theorem Real.ofDigitsTerm_nonneg {b : ℕ} {digits : ℕ → Fin b} {n : ℕ} : 0 ≤ ofDigitsTerm digits n

theorem Real.ofDigitsTerm_le {b : ℕ} {digits : ℕ → Fin b} {n : ℕ} : ofDigitsTerm digits n ≤ (↑b - 1) * (↑b ^ (n + 1))⁻¹

theorem Real.summable_ofDigitsTerm {b : ℕ} {digits : ℕ → Fin b} : Summable (ofDigitsTerm digits)

noncomputable def Real.ofDigits {b : ℕ} (digits : ℕ → Fin b) : ℝ

ofDigits d is the real number 0.d₀d₁d₂... in base b. We allow repeating representations like 0.999... here.

Equations

• Real.ofDigits digits = ∑' (n : ℕ), Real.ofDigitsTerm digits n

theorem Real.ofDigits_nonneg {b : ℕ} (digits : ℕ → Fin b) : 0 ≤ ofDigits digits

theorem Real.ofDigits_le_one {b : ℕ} (digits : ℕ → Fin b) : ofDigits digits ≤ 1

theorem Real.ofDigits_eq_sum_add_ofDigits {b : ℕ} (a : ℕ → Fin b) (n : ℕ) : ofDigits a = ∑ i ∈ Finset.range n, ofDigitsTerm a i + (↑b ^ n)⁻¹ * ofDigits fun (i : ℕ) => a (i + n)

theorem Real.abs_ofDigits_sub_ofDigits_le {b : ℕ} {x y : ℕ → Fin b} {n : ℕ} (hxy : ∀ i < n, x i = y i) : |ofDigits x - ofDigits y| ≤ (↑b ^ n)⁻¹

noncomputable def Real.digits (x : ℝ) (b : ℕ) [NeZero b] : ℕ → Fin b

Converts a real number x from the interval [0, 1) into sequence of its digits in base b.

Equations

• x.digits b i = Fin.ofNat b ⌊x * ↑b ^ (i + 1)⌋₊

theorem Real.ofDigits_digits_sum_eq {x : ℝ} {b : ℕ} [NeZero b] (hx : x ∈ Set.Ico 0 1) (n : ℕ) : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ n * x⌋₊

theorem Real.le_sum_ofDigitsTerm_digits {x : ℝ} {b : ℕ} [NeZero b] (hx : x ∈ Set.Ico 0 1) (n : ℕ) : x - (↑b)⁻¹ ^ n ≤ ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i

theorem Real.sum_ofDigitsTerm_digits_le {x : ℝ} {b : ℕ} [NeZero b] (hx : x ∈ Set.Ico 0 1) (n : ℕ) : ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i ≤ x

theorem Real.hasSum_ofDigitsTerm_digits (x : ℝ) {b : ℕ} [NeZero b] (hb : 1 < b) (hx : x ∈ Set.Ico 0 1) : HasSum (ofDigitsTerm (x.digits b)) x

theorem Real.ofDigits_digits {b : ℕ} [NeZero b] {x : ℝ} (hb : 1 < b) (hx : x ∈ Set.Ico 0 1) : ofDigits (x.digits b) = x

theorem Real.ofDigits_const_last_eq_one (b : ℕ) [NeZero b] : (ofDigits fun (x : ℕ) => Fin.last b) = 1

A generalization of the identity 0.(9) = 1 to arbitrary positional numeral systems.

theorem Real.ofDigits_const_last_eq_one' {b : ℕ} (hb : 1 < b) : (ofDigits fun (x : ℕ) => ⟨b - 1, ⋯⟩) = 1

A generalization of the identity 0.(9) = 1 to arbitrary positional numeral systems.

theorem Real.ofDigits_SurjOn {b : ℕ} (hb : 1 < b) : Set.SurjOn ofDigits Set.univ (Set.Icc 0 1)

theorem Real.continuous_ofDigits {b : ℕ} : Continuous ofDigits