English
Bound for iterated forward differences of a continuous function between a compact space and a nonarchimedean seminormed group.
Русский
Граница для итерационных прямых разностей непрерывной функции между компактным пространством и ненормированным неархимедовым полугруппом.
LaTeX
$$$$ \\| \\Delta_h^{[n]} f(m) \\| \\le \\|f\\|. $$$$
Lean4
/-- Key lemma for Mahler's theorem: for `f` a continuous function on `ℤ_[p]`, the sequence
`n ↦ Δ^[n] f 0` tends to 0. See `PadicInt.fwdDiff_iter_le_of_forall_le` for an explicit
estimate of the decay rate. -/
theorem fwdDiff_tendsto_zero (f : C(ℤ_[p], E)) : Tendsto (Δ_[1]^[·] f 0) atTop (𝓝 0) := by
-- first extract an `s`
refine NormedAddCommGroup.tendsto_nhds_zero.mpr (fun ε hε ↦ ?_)
have : Tendsto (fun s ↦ ‖f‖ / p ^ s) _ _ :=
tendsto_const_nhds.div_atTop (tendsto_pow_atTop_atTop_of_one_lt (mod_cast hp.out.one_lt))
obtain ⟨s, hs⟩ := (this.eventually_lt_const hε).exists
refine
.mp ?_
(.of_forall fun x hx ↦ lt_of_le_of_lt hx hs)
-- use uniform continuity to find `t`
obtain ⟨t, ht⟩ : ∃ t : ℕ, ∀ x y, ‖x - y‖ ≤ p ^ (-t : ℤ) → ‖f x - f y‖ ≤ ‖f‖ / p ^ s :=
by
rcases eq_or_ne f 0 with rfl | hf
· -- silly case : f = 0
simp
have : 0 < ‖f‖ / p ^ s := div_pos (norm_pos_iff.mpr hf) (mod_cast pow_pos hp.out.pos _)
obtain ⟨δ, hδpos, hδf⟩ := f.uniform_continuity _ this
obtain ⟨t, ht⟩ := PadicInt.exists_pow_neg_lt p hδpos
exact ⟨t, fun x y hxy ↦ by simpa only [dist_eq_norm_sub] using (hδf (hxy.trans_lt ht)).le⟩
filter_upwards [eventually_ge_atTop (s * p ^ t)] with m hm
simpa only [Nat.sub_add_cancel hm] using fwdDiff_iter_le_of_forall_le ht (m - s * p ^ t)
