English
A Lipschitz-type bound holds for polynomial evaluation in PadicInt p: the p-adic norm of F(a) − F(b) is controlled by the norm of a − b.
Русский
Для полинома F над R на p-адических целых числе справно неравенствоLipschitza: \|F(a) − F(b)\| ≤ \|a − b\|.
LaTeX
$$$\|F.aeval x - F.aeval y\| \le \|x - y\| \quad(x,y \in \mathbb{Z}_p).$$$
Lean4
theorem padic_polynomial_dist {p : ℕ} [Fact p.Prime] {R : Type*} [CommSemiring R] [Algebra R ℤ_[p]] (F : Polynomial R)
(x y : ℤ_[p]) : ‖F.aeval x - F.aeval y‖ ≤ ‖x - y‖ :=
by
let ⟨z, hz⟩ := (F.map (algebraMap R ℤ_[p])).evalSubFactor x y
simp only [Polynomial.eval_map_algebraMap] at hz
calc
‖F.aeval x - F.aeval y‖ = ‖z‖ * ‖x - y‖ := by simp [hz]
_ ≤ 1 * ‖x - y‖ := by gcongr; apply PadicInt.norm_le_one
_ = ‖x - y‖ := by simp
