Documentation

TauCeti.RingTheory.PowerSeries.Restricted.Taylor

Taylor translation of restricted power series #

Let R be a complete ultrametric normed commutative ring and f = ∑ aₖ Xᵏ a power series over R restricted at a radius c, so that ‖aₖ‖ cᵏ → 0 and f converges on the closed disc ‖x‖ ≤ c. For a point a of that disc, the Taylor translate taylor a f = ∑ₙ (Δⁿ f)(a) Xⁿ, whose coefficients are the values at a of the Hasse derivatives of f, is the expansion of f at a. This file shows that it is again restricted at c, with the same Gauss norm, and that it is the series f(X + a) on the whole closed disc:

‖(Δⁿ f)(a)‖ cⁿ ≤ ‖f‖_c,    ‖taylor a f‖_c = ‖f‖_c,    f(b + a) = ∑ₙ (Δⁿ f)(a) bⁿ  for ‖b‖ ≤ c.

Unlike the archimedean case there is no loss of radius: the expansion of f at any point of the closed disc of radius c converges on the same disc. Translation commutes with Hasse derivatives, is additive and multiplicative, and translations by a and b compose to the translation by b + a; in particular translation by -a inverts translation by a. No factorial is inverted, so all of this holds in every characteristic, for instance over finite extensions of ℚ_p with any ramification.

Splitting the expansion of f at a after its first T terms gives the Taylor remainder estimate: if ‖(Δᵗ f)(a)‖ ‖y‖ᵗ ≤ ε for t < T, then ‖f(y + a)‖ ≤ max ε (‖f‖_c (‖y‖ / c) ^ T) for ‖y‖ ≤ c. This is the local analytic estimate used to pass from small divided derivatives of an auxiliary function at one point to its size near that point in the method of linear forms in p-adic logarithms.

These are the one-variable counterparts, stated for PowerSeries and its Hasse derivatives, of the multivariable translation TauCeti.MvPowerSeries.restrictedTranslate of Tate algebras, and the restricted counterparts of the Taylor translation of entire series (PowerSeries.IsEntire.evalAt_taylor).

Main results #

References #

source
theorem PowerSeries.norm_evalAt_hasseDeriv_mul_pow_le_gaussNorm {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] {c : ℝ} {f : PowerSeries R} {a : R} (hc : 0 < c) (hf : HasGaussNorm norm c f) (ha : ‖a‖ ≤ c) (n : ℕ) :
‖((hasseDeriv n) f).evalAt a‖ * c ^ n ≤ gaussNorm norm c f

Coefficients of the expansion at a point. Over an ultrametric normed ring, for a series with a Gauss norm at a radius c > 0 and a point a with ‖a‖ ≤ c, the n-th coefficient (Δⁿ f)(a) of the expansion of f at a satisfies ‖(Δⁿ f)(a)‖ cⁿ ≤ ‖f‖_c.

source
theorem PowerSeries.gaussNorm_taylor_le {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] {c : ℝ} {f : PowerSeries R} {a : R} (hc : 0 < c) (hf : HasGaussNorm norm c f) (ha : ‖a‖ ≤ c) :
gaussNorm norm c (taylor a f) ≤ gaussNorm norm c f

Translation does not increase the Gauss norm. Over an ultrametric normed ring, for a series with a Gauss norm at a radius c > 0 and a point a with ‖a‖ ≤ c, ‖taylor a f‖_c ≤ ‖f‖_c.

source
theorem PowerSeries.IsRestricted.taylor {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] {c : ℝ} {f : PowerSeries R} {a : R} (hf : IsRestricted c f) (ha : ‖a‖ ≤ c) :
IsRestricted c (PowerSeries.taylor a f)

Translates of restricted series are restricted. Over an ultrametric normed ring, if f is restricted at the radius c and ‖a‖ ≤ c, then the expansion taylor a f of f at a is restricted at c: no radius is lost.

source
theorem PowerSeries.IsRestricted.evalAt_taylor {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] {c : ℝ} {f : PowerSeries R} {a b : R} [CompleteSpace R] (hf : IsRestricted c f) (ha : ‖a‖ ≤ c) (hb : ‖b‖ ≤ c) :
(PowerSeries.taylor a f).evalAt b = f.evalAt (b + a)

The Taylor identity for restricted series. Over a complete ultrametric normed ring, if f is restricted at the radius c and ‖a‖ ≤ c, ‖b‖ ≤ c, then the expansion of f at a evaluated at b is f(b + a).

source
theorem PowerSeries.IsRestricted.hasSum_taylor {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] {c : ℝ} {f : PowerSeries R} {a b : R} [CompleteSpace R] (hf : IsRestricted c f) (ha : ‖a‖ ≤ c) (hb : ‖b‖ ≤ c) :
HasSum (fun (k : ℕ) => ((PowerSeries.hasseDeriv k) f).evalAt a * b ^ k) (f.evalAt (b + a))

The Taylor expansion of a restricted series. Over a complete ultrametric normed ring, if f is restricted at the radius c and ‖a‖ ≤ c, ‖b‖ ≤ c, then f(b + a) = ∑ₖ (Δᵏ f)(a) bᵏ.

source
theorem PowerSeries.IsRestricted.taylor_add {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] {c : ℝ} {f g : PowerSeries R} {a : R} [CompleteSpace R] (hf : IsRestricted c f) (hg : IsRestricted c g) (ha : ‖a‖ ≤ c) :
PowerSeries.taylor a (f + g) = PowerSeries.taylor a f + PowerSeries.taylor a g

Translation is additive on restricted series.

source
theorem PowerSeries.IsRestricted.taylor_smul {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] {c : ℝ} {f : PowerSeries R} {a : R} [CompleteSpace R] (hf : IsRestricted c f) (r : R) (ha : ‖a‖ ≤ c) :
PowerSeries.taylor a (r • f) = r • PowerSeries.taylor a f

Translation commutes with scalar multiplication of restricted series.

source
theorem PowerSeries.IsRestricted.taylor_mul {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] {c : ℝ} {f g : PowerSeries R} {a : R} [CompleteSpace R] (hf : IsRestricted c f) (hg : IsRestricted c g) (ha : ‖a‖ ≤ c) :
PowerSeries.taylor a (f * g) = PowerSeries.taylor a f * PowerSeries.taylor a g

Translation is multiplicative on restricted series, by the Leibniz rule for Hasse derivatives.

source
theorem PowerSeries.IsRestricted.hasseDeriv_taylor {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] {c : ℝ} {f : PowerSeries R} {a : R} [CompleteSpace R] (hf : IsRestricted c f) (ha : ‖a‖ ≤ c) (k : ℕ) :
(PowerSeries.hasseDeriv k) (PowerSeries.taylor a f) = PowerSeries.taylor a ((PowerSeries.hasseDeriv k) f)

Hasse derivatives commute with translation of restricted series.

source
theorem PowerSeries.IsRestricted.taylor_taylor {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] {c : ℝ} {f : PowerSeries R} {a b : R} [CompleteSpace R] (hf : IsRestricted c f) (ha : ‖a‖ ≤ c) (hb : ‖b‖ ≤ c) :
PowerSeries.taylor b (PowerSeries.taylor a f) = PowerSeries.taylor (b + a) f

Translations compose: for a series f restricted at c and ‖a‖ ≤ c, ‖b‖ ≤ c, taylor b (taylor a f) = taylor (b + a) f.

source
theorem PowerSeries.IsRestricted.taylor_neg_taylor {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] {c : ℝ} {f : PowerSeries R} {a : R} [CompleteSpace R] (hf : IsRestricted c f) (ha : ‖a‖ ≤ c) :
PowerSeries.taylor (-a) (PowerSeries.taylor a f) = f

Translation by -a inverts translation by a on series restricted at c ≥ ‖a‖.

source
theorem PowerSeries.IsRestricted.gaussNorm_taylor {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] {c : ℝ} {f : PowerSeries R} {a : R} [CompleteSpace R] (hf : IsRestricted c f) (hc : 0 < c) (ha : ‖a‖ ≤ c) :
gaussNorm norm c (PowerSeries.taylor a f) = gaussNorm norm c f

Translation is an isometry. Over a complete ultrametric normed ring, for a series f restricted at a radius c > 0 and a point a with ‖a‖ ≤ c, ‖taylor a f‖_c = ‖f‖_c.

source
theorem PowerSeries.IsRestricted.norm_evalAt_add_le_max {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] {c : ℝ} {f : PowerSeries R} {a : R} [CompleteSpace R] (hf : IsRestricted c f) (hc : 0 < c) (ha : ‖a‖ ≤ c) {y : R} (hy : ‖y‖ ≤ c) {T : ℕ} {ε : ℝ} (h : ∀ t < T, ‖((PowerSeries.hasseDeriv t) f).evalAt a‖ * ‖y‖ ^ t ≤ ε) :
‖f.evalAt (y + a)‖ ≤ max ε (gaussNorm norm c f * (‖y‖ / c) ^ T)

The Taylor remainder estimate. Over a complete ultrametric normed ring, let f be restricted at a radius c > 0 and let ‖a‖ ≤ c, ‖y‖ ≤ c. If ε bounds the first T terms ‖(Δᵗ f)(a)‖ ‖y‖ᵗ, t < T, of the expansion of f at a, then

‖f(y + a)‖ ≤ max ε (‖f‖_c * (‖y‖ / c) ^ T).

For ε = 0 this is the Schwarz lemma at a single zero of order T.