English
For a compact space M, a continuous map f: M → G into a non-archimedean seminormed group G satisfies ∥Δ_h^n f(m)∥ ≤ ∥f∥ for all h,m,n.
Русский
Для компактного пространства M и непрерывного отображения f: M → G, в ненормированном полугруппе G выполняется ∥Δ_h^n f(m)∥ ≤ ∥f∥ для всех h,m,n.
LaTeX
$$$$ \| \Delta_{h}^{[n]} f(m) \| \le \| f \| \quad \\text{for all } h \in M, m \in M, n \in \\mathbb{N}, $$$$
Lean4
/-- Bound for iterated forward differences of a continuous function from a compact space to a
nonarchimedean seminormed group. -/
theorem norm_fwdDiff_iter_apply_le [TopologicalSpace M] [CompactSpace M] [AddCommMonoid M] [SeminormedAddCommGroup G]
[IsUltrametricDist G] (h : M) (f : C(M, G)) (m : M) (n : ℕ) : ‖Δ_[h]^[n] f m‖ ≤ ‖f‖ := by
-- A proof by induction on `n` would be possible but would involve some messing around to
-- define `Δ_[h]` as an operator on continuous maps (not just on bare functions). So instead we
-- use the formula for `Δ_[h]^[n] f` as a sum.
rw [fwdDiff_iter_eq_sum_shift]
refine norm_sum_le_of_forall_le_of_nonneg (norm_nonneg f) fun i _ ↦ ?_
exact (norm_zsmul_le _ _).trans (f.norm_coe_le_norm _)
