English
Bound for norms of ascending Pochhammer polynomials: for k ∈ ℕ and x ∈ ℤ_p, the norm of (ascPochhammer p k).eval(x) is ≤ the norm of k!.
Русский
Границы нормы возростающих полиномов Pochhammer: для k и x не равны, норма оценивает ≤ норма факториала.
LaTeX
$$$\| (\mathrm{ascPochhammer}_{\mathbb{Z}_p} k).\mathrm{eval}(x) \| \le \| (k! : \mathbb{Z}_p) \|.$$$
Lean4
/-- Bound for norms of ascending Pochhammer symbols. -/
theorem norm_ascPochhammer_le (k : ℕ) (x : ℤ_[p]) : ‖(ascPochhammer ℤ_[p] k).eval x‖ ≤ ‖(k.factorial : ℤ_[p])‖ :=
by
let f := (ascPochhammer ℤ_[p] k).eval
change ‖f x‖ ≤ ‖_‖
have hC : (k.factorial : ℤ_[p]) ≠ 0 := Nat.cast_ne_zero.mpr k.factorial_ne_zero
have hf : ContinuousAt f x :=
Polynomial.continuousAt
_
-- find `n : ℕ` such that `‖f x - f n‖ ≤ ‖k!‖`
obtain ⟨n, hn⟩ : ∃ n : ℕ, ‖f x - f n‖ ≤ ‖(k.factorial : ℤ_[p])‖ :=
by
obtain ⟨δ, hδp, hδ⟩ := Metric.continuousAt_iff.mp hf _ (norm_pos_iff.mpr hC)
obtain ⟨n, hn'⟩ := PadicInt.denseRange_natCast.exists_dist_lt x hδp
simpa only [← dist_eq_norm_sub'] using
⟨n, (hδ (dist_comm x n ▸ hn')).le⟩
-- use ultrametric property to show that `‖f n‖ ≤ ‖k!‖` implies `‖f x‖ ≤ ‖k!‖`
refine
sub_add_cancel (f x) _ ▸
(IsUltrametricDist.norm_add_le_max _ (f n)).trans
(max_le hn ?_)
-- finish using the fact that `n.multichoose k ∈ ℤ`
simp_rw [f, ← ascPochhammer_eval_cast, Polynomial.eval_eq_smeval, ← Ring.factorial_nsmul_multichoose_eq_ascPochhammer,
smul_eq_mul, Nat.cast_mul, norm_mul]
exact mul_le_of_le_one_right (norm_nonneg _) (norm_le_one _)
