-- Mathlib/NumberTheory/Ostrowski.lean
/-- 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`. -/
lemma apply_le_sum_digits (n : ℕ) {m : ℕ} (hm : 1 < m) :
    f n ≤ ((Nat.digits m n).mapIdx fun i _ ↦ m * (f m) ^ i).sum

Proof state:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun i a => a * m ^ i) L)
hL' : L' = List.map Nat.cast (List.mapIdx (fun i a => a * m ^ i) L)
hcoef : ∀ {c : ℕ}, c ∈ m.digits n → f ↑c < ↑m
x✝ : ℕ × ℕ
a i : ℕ
hia : (a, i) ∈ L.zipIdx
⊢ (⇑f ∘ Nat.cast ∘ fun x => x.1 * m ^ x.2) (a, i) ≤ ↑m * f ↑m ^ (a, i).2

Tactic:
dsimp only [Function.comp_apply, Function.uncurry_apply_pair]

Result:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun i a => a * m ^ i) L)
hL' : L' = List.map Nat.cast (List.mapIdx (fun i a => a * m ^ i) L)
hcoef : ∀ {c : ℕ}, c ∈ m.digits n → f ↑c < ↑m
x✝ : ℕ × ℕ
a i : ℕ
hia : (a, i) ∈ L.zipIdx
⊢ f ↑(a * m ^ i) ≤ ↑m * f ↑m ^ i

Proof state:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun i a => a * m ^ i) L)
hL' : L' = List.map Nat.cast (List.mapIdx (fun i a => a * m ^ i) L)
hcoef : ∀ {c : ℕ}, c ∈ m.digits n → f ↑c < ↑m
⊢ f ↑n = f ↑(ofDigits m L)

Tactic:
rw [Nat.ofDigits_digits m n]

Result:
no goals

Proof state:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun i a => a * m ^ i) L)
hL' : L' = List.map Nat.cast (List.mapIdx (fun i a => a * m ^ i) L)
hcoef : ∀ {c : ℕ}, c ∈ m.digits n → f ↑c < ↑m
⊢ (List.map (⇑f) L').sum ≤ (List.mapIdx (fun i x => ↑m * f ↑m ^ i) L).sum

Tactic:
simp only [hL', List.mapIdx_eq_zipIdx_map, List.map_map]

Result:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun i a => a * m ^ i) L)
hL' : L' = List.map Nat.cast (List.mapIdx (fun i a => a * m ^ i) L)
hcoef : ∀ {c : ℕ}, c ∈ m.digits n → f ↑c < ↑m
⊢ (List.map (⇑f ∘ Nat.cast ∘ fun x => x.1 * m ^ x.2) L.zipIdx).sum ≤ (List.map (fun x => ↑m * f ↑m ^ x.2) L.zipIdx).sum

Proof state:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun i a => a * m ^ i) L)
hL' : L' = List.map Nat.cast (List.mapIdx (fun i a => a * m ^ i) L)
hcoef : ∀ {c : ℕ}, c ∈ m.digits n → f ↑c < ↑m
x✝ : ℕ × ℕ
a i : ℕ
hia✝ : (a, i) ∈ L.zipIdx
hia : 0 ≤ i ∧ i < 0 + L.length ∧ a = L[i - 0]
⊢ f ↑(a * m ^ i) ≤ ↑m * f ↑m ^ i

Tactic:
push_cast

Result:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun i a => a * m ^ i) L)
hL' : L' = List.map Nat.cast (List.mapIdx (fun i a => a * m ^ i) L)
hcoef : ∀ {c : ℕ}, c ∈ m.digits n → f ↑c < ↑m
x✝ : ℕ × ℕ
a i : ℕ
hia✝ : (a, i) ∈ L.zipIdx
hia : 0 ≤ i ∧ i < 0 + L.length ∧ a = L[i - 0]
⊢ f (↑a * ↑m ^ i) ≤ ↑m * f ↑m ^ i

Proof state:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun i a => a * m ^ i) L)
hL' : L' = List.map Nat.cast (List.mapIdx (fun i a => a * m ^ i) L)
hcoef : ∀ {c : ℕ}, c ∈ m.digits n → f ↑c < ↑m
⊢ (List.map (⇑f ∘ Nat.cast ∘ fun x => x.1 * m ^ x.2) L.zipIdx).sum ≤ (List.map (fun x => ↑m * f ↑m ^ x.2) L.zipIdx).sum

Tactic:
refine List.sum_le_sum fun ⟨a, i⟩ hia ↦ ?_

Result:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun i a => a * m ^ i) L)
hL' : L' = List.map Nat.cast (List.mapIdx (fun i a => a * m ^ i) L)
hcoef : ∀ {c : ℕ}, c ∈ m.digits n → f ↑c < ↑m
x✝ : ℕ × ℕ
a i : ℕ
hia : (a, i) ∈ L.zipIdx
⊢ (⇑f ∘ Nat.cast ∘ fun x => x.1 * m ^ x.2) (a, i) ≤ ↑m * f ↑m ^ (a, i).2