• Introduce ofDigits {b : ℕ} (digits : ℕ → Fin b) : ℝ, representing a real number of the form 0.d₀d₁d₂... (where dᵢ = digits i) as an infinite sum.
• Prove that this sum converges to a number in the interval [0, 1].
• Prove ofDigits_close_of_common_prefix: if the first n digits of two numbers are equal, then their difference is bounded by b⁻ⁿ.
• Introduce Real.digits, which converts a real number into its sequence of digits.
• Prove that ofDigits (toDigits x b) = x.

Zulip threads:

• Zulip thread where this was proposed
• #PR reviews > representation of reals in [0, 1] in positional system

• depends on: [Merged by Bors] - feat(Algebra/Order/Floor): ⌊n * x⌋₊ / n = ⌊x⌋₊ #26004