English
The function mapping a sequence of base-b digits to a real number is given by i ↦ digits(i) · b^{-(i+1)}.
Русский
Функция, сопоставляющая последовательность цифр в основание b вещественному числу, задаётся как i ↦ digits(i) · b^{-(i+1)}.
LaTeX
$${b : Nat} → (Nat → Fin b) → Nat → \mathbb{R} \\; ; \\; i \mapsto (digits i) \cdot (b : \mathbb{R})^{-(i+1)}$$
Lean4
/-- `ofDigits` takes a sequence of digits `(d₀, d₁, ...)` in base `b` and returns the
real numnber `0.d₀d₁d₂... = ∑ᵢ(dᵢ/bⁱ)`. This auxiliary definition `ofDigitsTerm` sends the
sequence to the function sending `i` to `dᵢ/bⁱ`. -/
noncomputable def ofDigitsTerm {b : ℕ} (digits : ℕ → Fin b) : ℕ → ℝ := fun i ↦ (digits i) * ((b : ℝ) ^ (i + 1))⁻¹
