-- 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
⊢ f ↑(ofDigits m L) = f L'.sum

Tactic:
rw [Nat.ofDigits_eq_sum_mapIdx]

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
⊢ f ↑(List.mapIdx (fun i a => a * m ^ i) L).sum = f L'.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 * f ↑m ^ i ≤ ↑m * f ↑m ^ i

Tactic:
refine mul_le_mul_of_nonneg_right ?_ <| pow_nonneg (f.nonneg _) i

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

Proof state:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
⊢ f ↑n ≤ (List.mapIdx (fun i x => ↑m * f ↑m ^ i) (m.digits n)).sum

Tactic:
set L := Nat.digits m n

Result:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
⊢ f ↑n ≤ (List.mapIdx (fun i x => ↑m * f ↑m ^ i) L).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
⊢ f ↑(List.mapIdx (fun i a => a * m ^ i) L).sum = f L'.sum

Tactic:
norm_cast

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
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:
rw [map_mul, map_pow]

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 * f ↑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
x✝ : ℕ × ℕ
a i : ℕ
hia✝ : (a, i) ∈ L.zipIdx
hia : i < L.length ∧ a = L[i]
⊢ f ↑a ≤ ↑m

Tactic:
exact (hcoef (List.mem_iff_get.mpr ⟨⟨i, hia.1⟩, hia.2.symm⟩)).le

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
x✝ : ℕ × ℕ
a i : ℕ
hia✝ : (a, i) ∈ L.zipIdx
hia : 0 ≤ i ∧ i < 0 + L.length ∧ a = L[i - 0]
⊢ f ↑a ≤ ↑m

Tactic:
simp only [zero_le, zero_add, tsub_zero, true_and] at 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
hia : i < L.length ∧ a = L[i]
⊢ f ↑a ≤ ↑m

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)
⊢ f ↑n ≤ (List.mapIdx (fun i x => ↑m * f ↑m ^ i) L).sum

Tactic:
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)

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
⊢ f ↑n ≤ (List.mapIdx (fun i x => ↑m * f ↑m ^ i) L).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 ↑(a * m ^ i) ≤ ↑m * f ↑m ^ i

Tactic:
replace hia := List.mem_zipIdx 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
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
⊢ f ↑n ≤ (List.mapIdx (fun i x => ↑m * f ↑m ^ i) L).sum

Tactic:
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 := ?_

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) L').sum ≤ (List.mapIdx (fun i x => ↑m * f ↑m ^ i) L).sum

Proof state:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
⊢ f ↑n ≤ (List.mapIdx (fun i x => ↑m * f ↑m ^ i) L).sum

Tactic:
set L' : List ℚ := List.map Nat.cast (L.mapIdx fun i a ↦ (a * m ^ i)) with hL'

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)
⊢ f ↑n ≤ (List.mapIdx (fun i x => ↑m * f ↑m ^ i) L).sum