Documentation

TauCeti.RingTheory.PowerSeries.Weierstrass.Schwarz

The Schwarz lemma for restricted power series #

Let K be a complete ultrametric normed field and f = ∑ aₙ Xⁿ a power series over K restricted at a radius c > 0, so that ‖aₙ‖ cⁿ → 0 and f converges on the closed disc ‖x‖ ≤ c. A zero a of f in that disc splits off a linear factor without loss of norm:

f = (X - a) * q,    q restricted at c,    ‖f‖_c = c * ‖q‖_c

for the Gauss norm ‖·‖_c, by Weierstrass division by the distinguished polynomial X - a (TauCeti.PowerSeries.gaussNorm_X_sub_C_mul). Peeling off the zeros one at a time, counted with the multiplicity read off from the Hasse derivatives D⁽ᵗ⁾ f, gives the nonarchimedean Schwarz lemma: if the points b of a finite multiset Z in the closed disc of radius c satisfy (D⁽ᵗ⁾ f)(b) = 0 for every t less than the multiplicity of b in Z, then at every point x of the closed disc of radius c, in any complete normed field extension of K,

‖f(x)‖ ≤ ‖f‖_c * ∏_{b ∈ Z} ‖x - b‖ / c.

Unlike the archimedean Schwarz lemma there is no change of radius: every factor ‖x - b‖ / c is at most 1, and the bound is sharp for f = ∏ (X - b).

This is the analytic estimate behind the interpolation and extrapolation steps of the method of linear forms in p-adic logarithms: an auxiliary function with many zeros of high multiplicity at the points of a grid is small at every other point of the disc. For distinct points with prescribed multiplicities it takes the form ‖f(x)‖ ≤ ‖f‖_c * ∏_{b ∈ s} (‖x - b‖ / c) ^ T b. Since D⁽ᵏ⁾ f is again restricted at c, with ‖D⁽ᵏ⁾ f‖_c ≤ c⁻ᵏ ‖f‖_c, and vanishes at each b to order T b - k, the same bound with exponents T b - k and an extra factor c⁻ᵏ holds for the Hasse derivatives of f. This is the form the extrapolation steps use, where vanishing of f to high order on a grid controls the derivatives of lower order at new points.

Main results #

References #

source
theorem PowerSeries.IsRestricted.evalAt_eq_zero_iff {R : Type u_1} [NormedCommRing R] [NormOneClass R] [IsUltrametricDist R] [CompleteSpace R] {c : ℝ} {f : PowerSeries R} (hf : IsRestricted c f) (hc : 0 < c) {a : R} (ha : ‖a‖ ≤ c) :
f.evalAt a = 0 ↔ ∃ (q : PowerSeries R), IsRestricted c q ∧ f = (X - C a) * q

Factor theorem for restricted series. Over a complete ultrametric normed commutative ring, a series restricted at a radius c > 0 vanishes at a point a of the closed disc of radius c exactly when it is X - a times a series restricted at c.

source
theorem PowerSeries.IsRestricted.norm_evalAt_le_gaussNorm_mul_prod {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {c : ℝ} {f : PowerSeries K} [DecidableEq K] {L : Type u_2} [NormedField L] [NormedAlgebra K L] [CompleteSpace L] (hf : IsRestricted c f) (hc : 0 < c) {Z : Multiset K} (hZ : ∀ b ∈ Z, ‖b‖ ≤ c) (hzero : ∀ b ∈ Z, ∀ t < Multiset.count b Z, ((PowerSeries.hasseDeriv t) f).evalAt b = 0) {x : L} (hx : ‖x‖ ≤ c) :
‖f.evalAt x‖ ≤ gaussNorm norm c f * (Multiset.map (fun (b : K) => ‖x - (algebraMap K L) b‖ / c) Z).prod

The Schwarz lemma for restricted series. Let f be a power series over a complete ultrametric normed field K, restricted at a radius c > 0. Let Z be a finite multiset of points of the closed disc of radius c such that f vanishes at each b ∈ Z to at least the multiplicity of b in Z, in the sense that the Hasse derivatives (D⁽ᵗ⁾ f)(b) vanish for t below that multiplicity. Then at every point x of the closed disc of radius c in a complete normed field extension L of K,

‖f(x)‖ ≤ ‖f‖_c * ∏_{b ∈ Z} ‖x - b‖ / c,

where ‖f‖_c is the Gauss norm of f at c.

source
theorem PowerSeries.IsRestricted.norm_evalAt_le_gaussNorm_mul_prod_pow {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {c : ℝ} {f : PowerSeries K} {L : Type u_2} [NormedField L] [NormedAlgebra K L] [CompleteSpace L] (hf : IsRestricted c f) (hc : 0 < c) {s : Finset K} {T : K → ℕ} (hs : ∀ b ∈ s, ‖b‖ ≤ c) (hzero : ∀ b ∈ s, ∀ t < T b, ((PowerSeries.hasseDeriv t) f).evalAt b = 0) {x : L} (hx : ‖x‖ ≤ c) :
‖f.evalAt x‖ ≤ gaussNorm norm c f * ∏ b ∈ s, (‖x - (algebraMap K L) b‖ / c) ^ T b

The Schwarz lemma for distinct zeros with multiplicities. Let f be a power series over a complete ultrametric normed field K, restricted at a radius c > 0, and let s be a finite set of points of the closed disc of radius c at each of which the Hasse derivatives (D⁽ᵗ⁾ f)(b) vanish for t < T b. Then at every point x of the closed disc of radius c in a complete normed field extension L of K,

‖f(x)‖ ≤ ‖f‖_c * ∏_{b ∈ s} (‖x - b‖ / c) ^ T b.
source
theorem PowerSeries.IsRestricted.norm_evalAt_hasseDeriv_le_gaussNorm_mul_prod_pow {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {c : ℝ} {f : PowerSeries K} {L : Type u_2} [NormedField L] [NormedAlgebra K L] [CompleteSpace L] (hf : IsRestricted c f) (hc : 0 < c) {s : Finset K} {T : K → ℕ} (hs : ∀ b ∈ s, ‖b‖ ≤ c) (hzero : ∀ b ∈ s, ∀ t < T b, ((PowerSeries.hasseDeriv t) f).evalAt b = 0) (k : ℕ) {x : L} (hx : ‖x‖ ≤ c) :
‖((PowerSeries.hasseDeriv k) f).evalAt x‖ ≤ c⁻¹ ^ k * gaussNorm norm c f * ∏ b ∈ s, (‖x - (algebraMap K L) b‖ / c) ^ (T b - k)

The Schwarz lemma for Hasse derivatives. Let f be a power series over a complete ultrametric normed field K, restricted at a radius c > 0, and let s be a finite set of points of the closed disc of radius c at each of which the Hasse derivatives (D⁽ᵗ⁾ f)(b) vanish for t < T b. Then for every k and every point x of the closed disc of radius c in a complete normed field extension L of K,

‖(D⁽ᵏ⁾ f)(x)‖ ≤ c⁻ᵏ * ‖f‖_c * ∏_{b ∈ s} (‖x - b‖ / c) ^ (T b - k).

For k = 0 this is PowerSeries.IsRestricted.norm_evalAt_le_gaussNorm_mul_prod_pow.