Theorems · Theorem · number theory

Rat.AbsoluteValue.apply_le_sum_digits

∀ {f : AbsoluteValue ℚ ℝ} (n : ℕ) {m : ℕ}, 1 < m → f ↑n ≤ (List.mapIdx (fun i x => ↑m * f ↑m ^ i) (m.digits n)).sum

Given any two integers n, m with m > 1, the absolute value of n is bounded by m + m * f m + m * (f m) ^ 2 + ... + m * (f m) ^ d where d is the number of digits of the expansion of n in base m.

Defined in

Mathlib.NumberTheory.Ostrowski

Cited by

1 results in Mathlib

Foundations

Depth 110 from the axioms · uses propext, Classical.choice, Quot.sound