-- Mathlib/NumberTheory/Padics/MahlerBasis.lean
/--
Explicit bound for the decay rate of the Mahler coefficients of a continuous function on `ℤ_[p]`.
This will be used to prove Mahler's theorem.
-/
lemma fwdDiff_iter_le_of_forall_le {f : C(ℤ_[p], E)} {s t : ℕ}
    (hst : ∀ x y : ℤ_[p], ‖x - y‖ ≤ p ^ (-t : ℤ) → ‖f x - f y‖ ≤ ‖f‖ / p ^ s) (n : ℕ) :
    ‖Δ_[1]^[n + s * p ^ t] f 0‖ ≤ ‖f‖ / p ^ s

Proof state:
case zero
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n : ℕ
hk : 0 ≤ s
⊢ ‖Δ_[1]^[n + 0 * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ 0

Tactic:
simpa only [zero_mul, pow_zero, add_zero, div_one] using norm_fwdDiff_iter_apply_le 1 f 0 n

Result:
no goals

Proof state:
case succ.refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
k : ℕ
IH : ∀ (n : ℕ), k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k
n : ℕ
hk : k + 1 ≤ s
⊢ ↑((range (p ^ t - 1)).sup fun j => ‖Δ_[1]^[n + k * p ^ t + (j + 1)] (⇑f) 0‖₊ / ↑p) ≤ ‖f‖ / ↑p ^ (k + 1)

Tactic:
rw [← coe_nnnorm, ← NNReal.coe_natCast, ← NNReal.coe_pow, ← NNReal.coe_div, NNReal.coe_le_coe]

Result:
case succ.refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
k : ℕ
IH : ∀ (n : ℕ), k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k
n : ℕ
hk : k + 1 ≤ s
⊢ ((range (p ^ t - 1)).sup fun j => ‖Δ_[1]^[n + k * p ^ t + (j + 1)] (⇑f) 0‖₊ / ↑p) ≤ ‖f‖₊ / ↑p ^ (k + 1)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n : ℕ
⊢ ∀ {k : ℕ}, k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k

Tactic:
intro k hk

Result:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n k : ℕ
hk : k ≤ s
⊢ ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k

Proof state:
case succ.refine_2
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
k : ℕ
IH : ∀ (n : ℕ), k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k
n : ℕ
hk : k + 1 ≤ s
⊢ ‖f‖ / ↑p ^ s ≤ ‖f‖ / ↑p ^ (k + 1)

Tactic:
exact div_le_div_of_nonneg_left (norm_nonneg _)
  (mod_cast pow_pos hp.out.pos _) (mod_cast pow_le_pow_right₀ hp.out.one_le hk)

Result:
no goals

Proof state:
case succ
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
k : ℕ
IH : ∀ (n : ℕ), k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k
n : ℕ
hk : k + 1 ≤ s
⊢ ‖Δ_[1]^[n + k * p ^ t + p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ (k + 1)

Tactic:
refine (bojanic_mahler_step2 hst (n + k * p ^ t)).trans (max_le ?_ ?_)

Result:
case succ.refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
k : ℕ
IH : ∀ (n : ℕ), k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k
n : ℕ
hk : k + 1 ≤ s
⊢ ↑((range (p ^ t - 1)).sup fun j => ‖Δ_[1]^[n + k * p ^ t + (j + 1)] (⇑f) 0‖₊ / ↑p) ≤ ‖f‖ / ↑p ^ (k + 1)

case succ.refine_2
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
k : ℕ
IH : ∀ (n : ℕ), k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k
n : ℕ
hk : k + 1 ≤ s
⊢ ‖f‖ / ↑p ^ s ≤ ‖f‖ / ↑p ^ (k + 1)

Proof state:
case succ.refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
k : ℕ
IH : ∀ (n : ℕ), k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k
n : ℕ
hk : k + 1 ≤ s
⊢ ((range (p ^ t - 1)).sup fun j => ‖Δ_[1]^[n + k * p ^ t + (j + 1)] (⇑f) 0‖₊ / ↑p) ≤ ‖f‖₊ / ↑p ^ (k + 1)

Tactic:
refine Finset.sup_le fun j _ ↦ ?_

Result:
case succ.refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
k : ℕ
IH : ∀ (n : ℕ), k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k
n : ℕ
hk : k + 1 ≤ s
j : ℕ
x✝ : j ∈ range (p ^ t - 1)
⊢ ‖Δ_[1]^[n + k * p ^ t + (j + 1)] (⇑f) 0‖₊ / ↑p ≤ ‖f‖₊ / ↑p ^ (k + 1)

Proof state:
case succ.refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
k : ℕ
IH : ∀ (n : ℕ), k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k
n : ℕ
hk : k + 1 ≤ s
j : ℕ
x✝ : j ∈ range (p ^ t - 1)
⊢ ‖Δ_[1]^[n + k * p ^ t + (j + 1)] (⇑f) 0‖₊ / ↑p ≤ ‖f‖₊ / ↑p ^ (k + 1)

Tactic:
rw [pow_succ, ← div_div, div_le_div_iff_of_pos_right (mod_cast hp.out.pos), add_right_comm]

Result:
case succ.refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
k : ℕ
IH : ∀ (n : ℕ), k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k
n : ℕ
hk : k + 1 ≤ s
j : ℕ
x✝ : j ∈ range (p ^ t - 1)
⊢ ‖Δ_[1]^[n + (j + 1) + k * p ^ t] (⇑f) 0‖₊ ≤ ‖f‖₊ / ↑p ^ k

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
k : ℕ
IH : ∀ (n : ℕ), k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k
n : ℕ
hk : k + 1 ≤ s
j : ℕ
x✝ : j ∈ range (p ^ t - 1)
⊢ k ≤ s

Tactic:
omega

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n : ℕ
⊢ ‖Δ_[1]^[n + s * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ s

Tactic:
suffices ∀ {k : ℕ}, k ≤ s → ‖Δ_[1]^[n + k * p ^ t] f 0‖ ≤ ‖f‖ / p ^ k from this le_rfl

Result:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n : ℕ
⊢ ∀ {k : ℕ}, k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k