Taylor translation of entire power series

For a power series f and a point a, the Taylor translate taylor a f is the series whose n-th coefficient is the value (Δⁿ f)(a) of the n-th Hasse derivative of f at a (TauCeti.RingTheory.PowerSeries.Taylor). For an entire series f over a complete normed commutative ring, the translate is again entire and satisfies the Taylor identity (taylor a f)(b) = f(b + a). Writing f = ∑ cₖ Xᵏ, both sides are sums of the absolutely summable double series ∑ₙ,ₘ (n + m).choose n • cₙ₊ₘ aᵐ bⁿ: grouping its terms by n gives the translate at b, and grouping them by n + m gives f at b + a by the binomial theorem (PowerSeries.evalAt_taylor_of_summable). Since Hasse derivatives commute with translation, translations compose, taylor b (taylor a f) = taylor (b + a) f, so translation by -a inverts translation by a and Taylor translation is injective on entire series. These entire-series results invert no factorial and use no ultrametric hypothesis, so they hold in every characteristic and over ℂ as well as over nonarchimedean rings.

Injectivity is what controls the zeros of entire series over a field: a nonzero entire series has a nonvanishing Hasse derivative at every point, so each of its zeros has a finite order (PowerSeries.IsEntire.exists_isGoodZero).

Main results

• PowerSeries.IsEntire.taylor: the translate of an entire series is entire.
• PowerSeries.IsEntire.taylor_add, PowerSeries.IsEntire.taylor_smul: translation is linear on entire series.
• PowerSeries.IsEntire.taylor_mul: translation is multiplicative on entire series.
• PowerSeries.IsEntire.evalAt_taylor: the Taylor identity (taylor a f)(b) = f(b + a).
• PowerSeries.IsEntire.hasSum_taylor: the Taylor expansion f(b + a) = ∑ₖ (Δᵏ f)(a) bᵏ converges.
• PowerSeries.IsEntire.hasseDeriv_taylor: Hasse derivatives commute with translation.
• PowerSeries.IsEntire.taylor_taylor: taylor b (taylor a f) = taylor (b + a) f.
• PowerSeries.IsEntire.taylor_inj, PowerSeries.IsEntire.taylor_eq_zero_iff: translation is injective on entire series.

theorem PowerSeries.IsEntire.taylor_add {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} [CompleteSpace R] {g : PowerSeries R} (hf : f.IsEntire) (hg : g.IsEntire) (a : R) : PowerSeries.taylor a (f + g) = PowerSeries.taylor a f + PowerSeries.taylor a g

Taylor translation is additive on entire series.

theorem PowerSeries.IsEntire.taylor_smul {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} [CompleteSpace R] (hf : f.IsEntire) (c a : R) : PowerSeries.taylor a (c • f) = c • PowerSeries.taylor a f

Taylor translation commutes with scalar multiplication of entire series.

theorem PowerSeries.IsEntire.taylor_mul {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} [CompleteSpace R] {g : PowerSeries R} (hf : f.IsEntire) (hg : g.IsEntire) (a : R) : PowerSeries.taylor a (f * g) = PowerSeries.taylor a f * PowerSeries.taylor a g

Taylor translation is multiplicative on entire series, by the Leibniz rule for Hasse derivatives.

theorem PowerSeries.IsEntire.evalAt_taylor {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} [CompleteSpace R] (hf : f.IsEntire) (a b : R) : (PowerSeries.taylor a f).evalAt b = f.evalAt (b + a)

The Taylor identity. For an entire series f, the Taylor translate at a evaluated at b is f(b + a).

theorem PowerSeries.IsEntire.hasseDeriv_taylor {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} [CompleteSpace R] (hf : f.IsEntire) (a : R) (k : ℕ) : (PowerSeries.hasseDeriv k) (PowerSeries.taylor a f) = PowerSeries.taylor a ((PowerSeries.hasseDeriv k) f)

Hasse derivatives commute with Taylor translation of entire series.

theorem PowerSeries.IsEntire.taylor_taylor {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} [CompleteSpace R] (hf : f.IsEntire) (a b : R) : PowerSeries.taylor b (PowerSeries.taylor a f) = PowerSeries.taylor (b + a) f

Taylor translations compose: for an entire series f, taylor b (taylor a f) = taylor (b + a) f.

theorem PowerSeries.IsEntire.taylor_neg_taylor {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} [CompleteSpace R] (hf : f.IsEntire) (a : R) : PowerSeries.taylor (-a) (PowerSeries.taylor a f) = f

Translation by -a inverts translation by a on entire series.

theorem PowerSeries.IsEntire.taylor_inj {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} [CompleteSpace R] {g : PowerSeries R} (hf : f.IsEntire) (hg : g.IsEntire) (a : R) : PowerSeries.taylor a f = PowerSeries.taylor a g ↔ f = g

Taylor translation is injective on entire series.

theorem PowerSeries.IsEntire.taylor_eq_zero_iff {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} [CompleteSpace R] (hf : f.IsEntire) (a : R) : PowerSeries.taylor a f = 0 ↔ f = 0

An entire series has zero Taylor translate exactly when it is zero.

theorem PowerSeries.IsEntire.taylor {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} (hf : f.IsEntire) (a : R) : (PowerSeries.taylor a f).IsEntire

Taylor translates of entire series are entire.

theorem PowerSeries.IsEntire.hasSum_taylor {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} [CompleteSpace R] (hf : f.IsEntire) (a b : R) : HasSum (fun (k : ℕ) => ((PowerSeries.hasseDeriv k) f).evalAt a * b ^ k) (f.evalAt (b + a))

The Taylor expansion of an entire series converges: f(b + a) = ∑ₖ (Δᵏ f)(a) bᵏ.