English
If a continuous f: ℤ_p → E has a Lipschitz-type bound ∥f(x) − f(y)∥ ≤ ∥f∥/p^s whenever ∥x − y∥ ≤ p^{−t}, then ∥Δ^{n+s p^t} f(0)∥ ≤ ∥f∥/p^s for all n.
Русский
Если непрерывная функция f: ℤ_p → E удовлетворяет лиспшицевскому неравенству ∥f(x) − f(y)∥ ≤ ∥f∥/p^s при ∥x − y∥ ≤ p^{−t}, то ∥Δ^{n+s p^t} f(0)∥ ≤ ∥f∥/p^s для всех n.
LaTeX
$$$$ \\forall f: C(\\mathbb{Z}_p,E),\\ s,t,n \\in \\mathbb{N},\\; (\\forall x,y \\in \\mathbb{Z}_p,\\ \\|x-y\\| \\\\le p^{-t} \\Rightarrow \\|f(x)-f(y)\\| \\\\le \\|f\\|/p^s) \\Rightarrow \\\\| \\Delta^{n+s p^t} f(0) \\| \\\\le \\|f\\|/p^s. $$$$
Lean4
/-- 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.
-/
theorem 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 := by
-- We show the following more general statement by induction on `k`:
suffices ∀ {k : ℕ}, k ≤ s → ‖Δ_[1]^[n + k * p ^ t] f 0‖ ≤ ‖f‖ / p ^ k from this le_rfl
intro k hk
induction k generalizing n with
| zero => -- base case just says that `‖Δ^[·] (⇑f) 0‖` is bounded by `‖f‖`
simpa only [zero_mul, pow_zero, add_zero, div_one] using norm_fwdDiff_iter_apply_le 1 f 0 n
| succ k IH => -- induction is the "step 2" lemma above
rw [add_mul, one_mul, ← add_assoc]
refine (bojanic_mahler_step2 hst (n + k * p ^ t)).trans (max_le ?_ ?_)
· rw [← coe_nnnorm, ← NNReal.coe_natCast, ← NNReal.coe_pow, ← NNReal.coe_div, NNReal.coe_le_coe]
refine Finset.sup_le fun j _ ↦ ?_
rw [pow_succ, ← div_div, div_le_div_iff_of_pos_right (mod_cast hp.out.pos), add_right_comm]
exact_mod_cast IH (n + (j + 1)) (by cutsat)
·
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)
