Taylor translation of power series

For a power series f over a commutative topological ring 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. On polynomials it is Polynomial.taylor a, the substitution X ↦ X + a.

Writing f = ∑ cₖ Xᵏ, both (taylor a f)(b) and f(b + a) are sums of the 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. So the Taylor identity (taylor a f)(b) = f(b + a) holds as soon as that double series is summable and its rows converge to (Δⁿ f)(a). This is shared by the Taylor theories of entire series (PowerSeries.IsEntire.evalAt_taylor) and of restricted series (PowerSeries.IsRestricted.evalAt_taylor), which supply the convergence.

Main definitions

• taylor a f: the Taylor translate of f at a, with coefficients (Δⁿ f)(a).

Main results

• constantCoeff_taylor: the constant term of the translate is f(a).
• order_taylor_ne_zero_iff: the translate at a has positive order exactly when f(a) = 0.
• taylor_coe: on polynomials, the translate is Polynomial.taylor.
• taylor_zero: translation by 0 is the identity.
• taylor_one: the translate of 1 is 1.
• evalAt_taylor_of_summable: the Taylor identity (taylor a f)(b) = f(b + a) for any series whose double series at (a, b) is summable with rows converging to (Δⁿ f)(a).
• taylor_add_of_summable_norm, taylor_mul_of_summable_norm: translation is additive and multiplicative when all Hasse derivatives have absolutely summable terms at the centre.

noncomputable def PowerSeries.taylor {R : Type u_1} [CommSemiring R] [TopologicalSpace R] (a : R) (f : PowerSeries R) : PowerSeries R

The Taylor translate of a power series f at a: the series ∑ₙ (Δⁿ f)(a) Xⁿ, whose coefficients are the values at a of the Hasse derivatives of f. For an entire series over a complete normed ring it is the series f(X + a) (PowerSeries.IsEntire.evalAt_taylor); in general the values (Δⁿ f)(a) are the junk value of PowerSeries.evalAt when they diverge.

@[simp]

theorem PowerSeries.coeff_taylor {R : Type u_1} [CommSemiring R] [TopologicalSpace R] (a : R) (f : PowerSeries R) (n : ℕ) : (coeff n) (taylor a f) = ((hasseDeriv n) f).evalAt a

The coefficients of the Taylor translate are the values of the Hasse derivatives.

@[simp]

theorem PowerSeries.constantCoeff_taylor {R : Type u_1} [CommSemiring R] [TopologicalSpace R] (a : R) (f : PowerSeries R) : constantCoeff (taylor a f) = f.evalAt a

The constant term of the Taylor translate at a is the value at a.

theorem PowerSeries.order_taylor_ne_zero_iff {R : Type u_1} [CommSemiring R] [TopologicalSpace R] {a : R} {f : PowerSeries R} : (taylor a f).order ≠ 0 ↔ f.evalAt a = 0

The Taylor translate at a has positive order exactly when a is a zero: the order of the translate is the multiplicity of the zero.

@[simp]

theorem PowerSeries.taylor_coe {R : Type u_1} [CommSemiring R] [TopologicalSpace R] (a : R) (p : Polynomial R) : taylor a ↑p = ↑((Polynomial.taylor a) p)

On polynomials, Taylor translation is Polynomial.taylor.

@[simp]

theorem PowerSeries.taylor_zero {R : Type u_1} [CommSemiring R] [TopologicalSpace R] (f : PowerSeries R) : taylor 0 f = f

Translation by 0 is the identity.

@[simp]

theorem PowerSeries.taylor_zero_right {R : Type u_1} [CommSemiring R] [TopologicalSpace R] (a : R) : taylor a 0 = 0

The translate of the zero series is zero.

@[simp]

theorem PowerSeries.taylor_one {R : Type u_1} [CommSemiring R] [TopologicalSpace R] (a : R) : taylor a 1 = 1

The translate of the constant series 1 is 1.

theorem PowerSeries.evalAt_taylor_of_summable {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [T2Space R] {f : PowerSeries R} {a b : R} (hF : Summable fun (p : ℕ × ℕ) => (coeff p.2) ((hasseDeriv p.1) f) * a ^ p.2 * b ^ p.1) (hrow : ∀ (n : ℕ), HasSum (fun (m : ℕ) => (coeff m) ((hasseDeriv n) f) • a ^ m) (((hasseDeriv n) f).evalAt a)) : (taylor a f).evalAt b = f.evalAt (b + a)

The Taylor identity from the double series. If the double series ∑ₙ,ₘ coeff m (Δⁿ f) aᵐ bⁿ is summable and each of its rows ∑ₘ coeff m (Δⁿ f) aᵐ converges to (Δⁿ f)(a), then the Taylor translate at a evaluated at b is f(b + a). Grouping the terms by n gives the translate at b, and grouping them by n + m gives f at b + a, by the binomial theorem.

theorem PowerSeries.taylor_add_of_summable_norm {R : Type u_1} [NormedCommRing R] [CompleteSpace R] {f g : PowerSeries R} {a : R} (hf : ∀ (n : ℕ), Summable fun (m : ℕ) => ‖(coeff m) ((hasseDeriv n) f) • a ^ m‖) (hg : ∀ (n : ℕ), Summable fun (m : ℕ) => ‖(coeff m) ((hasseDeriv n) g) • a ^ m‖) : taylor a (f + g) = taylor a f + taylor a g

Taylor translation is additive when all Hasse derivatives have absolutely summable terms at the translation point.

theorem PowerSeries.taylor_mul_of_summable_norm {R : Type u_1} [NormedCommRing R] [CompleteSpace R] {f g : PowerSeries R} {a : R} (hf : ∀ (n : ℕ), Summable fun (m : ℕ) => ‖(coeff m) ((hasseDeriv n) f) • a ^ m‖) (hg : ∀ (n : ℕ), Summable fun (m : ℕ) => ‖(coeff m) ((hasseDeriv n) g) • a ^ m‖) : taylor a (f * g) = taylor a f * taylor a g

Taylor translation is multiplicative when all Hasse derivatives have absolutely summable terms at the translation point.