English
For any natural n and m>1, f(n) ≤ sum of m · f(m)^i over the digits expansion of n.
Русский
Для любого натурального n и m>1, f(n) не больше суммы по цифрам в основание m: сумма m·f(m)^i.
LaTeX
$$f(n) ≤ (Digits_m(n) mapIdx (i ↦ m · f(m)^i)).sum$$
Lean4
/-- 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`. -/
theorem apply_le_sum_digits (n : ℕ) {m : ℕ} (hm : 1 < m) :
f n ≤ ((Nat.digits m n).mapIdx fun i _ ↦ m * (f m) ^ i).sum :=
by
set L := Nat.digits m n
set L' : List ℚ := List.map Nat.cast (L.mapIdx fun i a ↦ (a * m ^ i)) with hL'
have hcoef {c : ℕ} (hc : c ∈ Nat.digits m n) : f c < m :=
lt_of_le_of_lt (f.apply_nat_le_self c) (mod_cast Nat.digits_lt_base hm hc)
calc
f n = f ((Nat.ofDigits m L : ℕ) : ℚ) := by rw [Nat.ofDigits_digits m n]
_ = f L'.sum := by rw [Nat.ofDigits_eq_sum_mapIdx]; norm_cast
_ ≤ (L'.map f).sum := (listSum_le f L')
_ ≤ (L.mapIdx fun i _ ↦ m * (f m) ^ i).sum := ?_
simp only [hL', List.mapIdx_eq_zipIdx_map, List.map_map]
refine List.sum_le_sum fun ⟨a, i⟩ hia ↦ ?_
dsimp only [Function.comp_apply, Function.uncurry_apply_pair]
replace hia := List.mem_zipIdx hia
push_cast
rw [map_mul, map_pow]
refine mul_le_mul_of_nonneg_right ?_ <| pow_nonneg (f.nonneg _) i
simp only [zero_le, zero_add, tsub_zero, true_and] at hia
exact (hcoef (List.mem_iff_get.mpr ⟨⟨i, hia.1⟩, hia.2.symm⟩)).le
