Power series substitution: nilpotent series, orders, algebra maps, and the binomial series

Mathlib substitutes a power series b with nilpotent constant coefficient into a power series f through PowerSeries.subst b f, and records the side condition on b as PowerSeries.HasSubst b.

Over a ring without zero divisors, substituting a series φ of zero constant coefficient multiplies orders: ord (f (φ)) = ord φ * ord f. Mathlib records only the inequality PowerSeries.le_order_subst. The equality shows that substitution of a nonzero such φ is injective, which is what extends it to Laurent series by passing to fraction fields. Injectivity of polynomial evaluation means such a φ is transcendental; over a field K it follows that the power series algebraic over K are the constants.

Substitution of series of zero constant coefficient is compatible with congruences modulo powers of X, in both the substituted series and the series substituted into. This makes truncation modulo X ^ n compatible with composition of formal coordinates. Substituting a multivariate series φ of zero constant coefficient into f = c Xⁿ + ⋯ gives f (φ) = c φ₁ ^ n + ⋯ in lowest degree, where φ₁ is the linear part of φ. In one variable this reads [Xⁿ] f (a) = c a₁ ^ n, and symmetrically [Xⁿ] f (a) = f₁ c when a = c Xⁿ + ⋯ and f = f₁ X + ⋯ have no constant terms; together these compare the lowest terms of the two sides of an equation f ∘ g = h ∘ f. For a family of series substituted into a multivariate series G, a perturbation X ^ m * r of the entry a s is invisible below degree m and acts in degree m through the coefficient of Xₛ alone; this drives degree-by-degree solutions of equations such as G(f(X), X) = 0.

Substitution at a nilpotent series depends on only finitely many coefficients. The substituted series may be multivariate, with coefficients in an algebra over the coefficient ring. At a nilpotent constant it is the constant series obtained by evaluating a finite polynomial truncation. This connects formal identities with polynomial maps on nilpotent elements.

An algebra map on power series whose value at X has nilpotent constant coefficient is the corresponding substitution, without any continuity hypothesis. Over a field, every algebra endomorphism of the power series ring has this form. In particular, a perturbation X + h of X with h ^ 2 = 0 substitutes by the first-order Taylor formula f (X + h) = f + h f', since the right-hand side is multiplicative in f by the Leibniz rule.

The coefficients of f (X * M) satisfy a shift recurrence: the coefficient of degree n + 1 is [X^n](M * g (X * M)), the coefficient of degree n of the product of M with g (X * M), where g = (f - f(0)) / X is the shift of f. This proves functional equations of generating functions such as M = C (X * M) coefficientwise.

This file also records that the substitution X ↦ (1 + X) ^ u - 1, for a binomial series (1 + X) ^ u, is legitimate: it is the change of variable relating the power-series coordinates of a completed group algebra attached to two topological generators.

Main results

• PowerSeries.coeff_subst_eq_sum_range: a finite coefficient formula when the inner series has zero constant coefficient.

• Continuous.powerSeries_subst: substitution is jointly continuous in coefficientwise continuous families whose inner series have zero constant coefficient.

• PowerSeries.HasSubst.C: a nilpotent constant can be substituted.

• PowerSeries.subst_one: substitution preserves the constant series one.

• PowerSeries.subst_X_add_C_mul_X_pow: substituting a into X + e Xᵏ gives a + e aᵏ.

• PowerSeries.subst_eq_aeval_trunc_of_pow_eq_zero: substitution at a series with a vanishing power is evaluation of a finite truncation.

• PowerSeries.subst_C_eq_C_aeval_trunc: substitution at a nilpotent constant is the constant series obtained by evaluating a finite truncation.

• PowerSeries.order_subst: ord (f (φ)) = ord φ * ord f when φ has zero constant coefficient.

• PowerSeries.subst_eq_zero_iff: substitution of a nonzero φ of zero constant coefficient has trivial kernel.

• PowerSeries.toNat_order_ne_zero: such a φ has positive integer order.

• PowerSeries.transcendental_of_constantCoeff_eq_zero: such a φ is transcendental over the coefficients.

• PowerSeries.isIntegrallyClosedIn: a field K is integrally closed in K⟦X⟧.

• PowerSeries.coeff_one_subst: linear coefficients multiply under substitution.

• PowerSeries.coeff_succ_subst_X_mul: the (n + 1)-st coefficient of f (X * M) is [X^n](M * g (X * M)), where g is the shift of f.

• PowerSeries.X_pow_dvd_subst: substitution preserves divisibility by X ^ n.

• PowerSeries.X_pow_dvd_subst_sub_subst: substitution respects congruence modulo X ^ n of the substituted series.

• PowerSeries.homogeneousComponent_subst_of_le_order: if f has order at least n, the degree-n homogeneous component of f (φ) is c φ₁ ^ n, for c the coefficient of Xⁿ in f and φ₁ the linear part of φ.

• PowerSeries.coeff_subst_eq_sum_range_degree: the coefficient of X^d in f (a), for a of zero constant coefficient, is the finite sum ∑_{n ≤ |d|} fₙ [X^d] aⁿ.

• PowerSeries.coeff_subst_mem: if f and a have coefficients in a subring, so does f (a).

• PowerSeries.homogeneousComponent_subst_left_eq_C_mul_X_pow, PowerSeries.homogeneousComponent_subst_right_eq_C_mul_X_pow: for φ = X + ⋯, the degree-n parts of f (φ) and of φ (f) are c Xⁿ when f has order at least n (and n ≥ 1 for φ (f)), for c the coefficient of Xⁿ in f.

• PowerSeries.coeff_subst_update_add_X_pow_mul: perturbing one entry a s of a substituted family by X ^ m * r changes coefficients only from degree m on, and in degree m only through the linear term Xₛ of the multivariate series.

• PowerSeries.exists_subst_add_X_pow_mul: perturbing a zero-constant input by X ^ m * r gives a difference X ^ m * s with s(0) = f₁ r(0).

• PowerSeries.algHom_eq_substAlgHom: an algebra map R⟦X⟧ → S⟦X⟧ sending X to a substitutable series is a substitution.

• PowerSeries.subst_add_of_sq_eq_zero: f (a + h) = f (a) + h f' (a) when h ^ 2 = 0, and its special case PowerSeries.subst_X_add_of_sq_eq_zero, f (X + h) = f + h f'.

• AlgHom.apply_eq_subst: over a field, every algebra endomorphism of K⟦X⟧ is substitution by its value at X.

• TauCeti.hasSubst_binomialSeries_sub_one: (1 + X) ^ u - 1 can be substituted.

theorem PowerSeries.coeff_subst_eq_sum_range {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (f : PowerSeries R) {g : PowerSeries S} (hg : constantCoeff g = 0) (n : ℕ) : (coeff n) (subst g f) = ∑ k ∈ Finset.range (n + 1), (coeff k) f • (coeff n) (g ^ k)

When the inner series has zero constant coefficient, the coefficient of degree n of a substitution depends only on the first n + 1 coefficients of the outer series.

theorem PowerSeries.HasSubst.C {R : Type u_1} [CommRing R] {x : R} (hx : IsNilpotent x) : HasSubst (PowerSeries.C x)

A nilpotent constant can be substituted into a power series.

@[simp]

theorem PowerSeries.subst_zero {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {τ : Type u_3} (a : MvPowerSeries τ S) : subst a 0 = 0

Substituting into the zero series gives zero, even without a substitutability hypothesis.

@[simp]

theorem PowerSeries.subst_one {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {τ : Type u_3} (a : MvPowerSeries τ S) : subst a 1 = 1

Substitution preserves the constant series one.

theorem PowerSeries.subst_X_pow_X_pow {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (a : ℕ) {b : ℕ} (hb : b ≠ 0) : subst (X ^ b) (X ^ a) = X ^ (a * b)

Substituting X ^ b into X ^ a multiplies the exponents.

theorem PowerSeries.subst_X_add_C_mul_X_pow {R : Type u_1} {τ : Type u_2} [CommRing R] {a : MvPowerSeries τ R} (ha : HasSubst a) (e : R) (k : ℕ) : subst a (X + C e * X ^ k) = a + MvPowerSeries.C e * a ^ k

Substituting a into X + e Xᵏ gives a + e aᵏ.

theorem PowerSeries.coeff_succ_subst_X_mul {R : Type u_1} [CommRing R] (M f : PowerSeries R) (n : ℕ) : (coeff (n + 1)) (subst (X * M) f) = (coeff n) (M * subst (X * M) (mk fun (p : ℕ) => (coeff (p + 1)) f))

The (n + 1)-st coefficient of f (X * M) is the n-th coefficient of M * g (X * M), where g = (f - f(0)) / X is the shift of f.

theorem PowerSeries.subst_eq_aeval_trunc_of_pow_eq_zero {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {τ : Type u_3} {a : MvPowerSeries τ S} {n : ℕ} (hn : a ^ n = 0) (f : PowerSeries R) : subst a f = (Polynomial.aeval a) ((trunc n) f)

Substituting a possibly multivariate series over an R-algebra whose nth power vanishes uses only the coefficients below n.

theorem PowerSeries.subst_C_eq_C_aeval_trunc {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} {n : ℕ} (hn : x ^ n = 0) (f : PowerSeries R) : subst (C x) f = C ((Polynomial.aeval x) ((trunc n) f))

A nilpotent constant in an R-algebra substitutes by algebra evaluation of a finite truncation.

theorem PowerSeries.toNat_order_ne_zero {R : Type u_1} [Semiring R] {φ : PowerSeries R} (hφ : constantCoeff φ = 0) (hφ₀ : φ ≠ 0) : φ.order.toNat ≠ 0

A nonzero power series of zero constant coefficient has positive integer order, so it multiplies orders under substitution by a positive integer.

theorem PowerSeries.order_subst {R : Type u_1} [CommRing R] [NoZeroDivisors R] {φ : PowerSeries R} (hφ : constantCoeff φ = 0) (f : PowerSeries R) : order (subst φ f) = φ.order * f.order

Substituting a power series φ of zero constant coefficient multiplies orders: ord (f (φ)) = ord φ * ord f.

theorem PowerSeries.subst_eq_zero_iff {R : Type u_1} [CommRing R] [NoZeroDivisors R] {φ : PowerSeries R} (hφ : constantCoeff φ = 0) (hφ₀ : φ ≠ 0) {f : PowerSeries R} : subst φ f = 0 ↔ f = 0

Substituting a nonzero power series φ of zero constant coefficient sends only 0 to 0.

theorem PowerSeries.transcendental_of_constantCoeff_eq_zero {R : Type u_1} [CommRing R] [NoZeroDivisors R] {φ : PowerSeries R} (hφ : constantCoeff φ = 0) (hφ₀ : φ ≠ 0) : Transcendental R φ

A nonzero power series φ of zero constant coefficient is transcendental over the coefficients: evaluating a polynomial at φ is substituting φ into it, which is injective.

theorem PowerSeries.coeff_one_subst {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] {a : PowerSeries S} (ha : constantCoeff a = 0) (f : PowerSeries R) : (coeff 1) (subst a f) = (algebraMap R S) ((coeff 1) f) * (coeff 1) a

The linear coefficient of f (a), for a of zero constant coefficient, is the product of the linear coefficients of f and a.

theorem PowerSeries.coeff_subst_eq_mul_pow {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] {a : PowerSeries S} (ha : constantCoeff a = 0) {f : PowerSeries R} {n : ℕ} (hn : ↑n ≤ f.order) : (coeff n) (subst a f) = (algebraMap R S) ((coeff n) f) * (coeff 1) a ^ n

The lowest coefficient of a substitution into a series of large order. If f has order at least n and a has zero constant coefficient, then the coefficient of Xⁿ in f (a) is c a₁ ^ n, where c is the coefficient of Xⁿ in f and a₁ is the linear coefficient of a.

theorem PowerSeries.coeff_subst_eq_mul {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] {a : PowerSeries S} (ha : constantCoeff a = 0) {f : PowerSeries R} (hf : constantCoeff f = 0) {n : ℕ} (hn : ↑n ≤ a.order) : (coeff n) (subst a f) = (algebraMap R S) ((coeff 1) f) * (coeff n) a

The lowest coefficient of a substitution of a series of large order. If f and a have zero constant coefficient and a has order at least n, then the coefficient of Xⁿ in f (a) is f₁ c, where f₁ is the linear coefficient of f and c is the coefficient of Xⁿ in a.

theorem PowerSeries.algHom_eq_substAlgHom {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] {σ : PowerSeries R →ₐ[R] PowerSeries S} (hσ : HasSubst (σ X)) : σ = substAlgHom hσ

An R-algebra map σ : R⟦X⟧ → S⟦X⟧ such that σ X can be substituted is the substitution f ↦ f (σ X). No continuity hypothesis is needed.

theorem PowerSeries.subst_add_of_sq_eq_zero {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] {a h : PowerSeries S} (ha : HasSubst a) (hh : h ^ 2 = 0) (f : PowerSeries R) : subst (a + h) f = subst a f + h * subst a (derivative f)

The first-order Taylor formula: substituting a square-zero perturbation a + h of a substitutable series a gives f (a + h) = f (a) + h f' (a).

theorem PowerSeries.subst_X_add_of_sq_eq_zero {S : Type u_3} [CommRing S] {h : PowerSeries S} (hh : h ^ 2 = 0) (f : PowerSeries S) : subst (X + h) f = f + h * derivative f

The first-order Taylor formula at X: substituting a square-zero perturbation X + h of X gives f (X + h) = f + h f'.

theorem PowerSeries.X_pow_dvd_subst {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] {a : PowerSeries S} (ha : constantCoeff a = 0) {n : ℕ} {f : PowerSeries R} (hf : X ^ n ∣ f) : X ^ n ∣ subst a f

Substituting a series of zero constant coefficient preserves divisibility by X ^ n.

theorem PowerSeries.X_pow_dvd_subst_sub_subst {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] {a b : PowerSeries S} (ha : constantCoeff a = 0) {n : ℕ} (hab : X ^ n ∣ a - b) (f : PowerSeries R) : X ^ n ∣ subst a f - subst b f

Substitution respects congruence modulo X ^ n of the substituted series: if a ≡ b modulo X ^ n, then f (a) ≡ f (b) modulo X ^ n. For n ≠ 0 the congruence forces b to have zero constant coefficient as well, so only a needs it.

theorem PowerSeries.homogeneousComponent_subst_of_le_order {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] {σ : Type u_4} {φ : MvPowerSeries σ S} (hφ : MvPowerSeries.constantCoeff φ = 0) {f : PowerSeries R} {n : ℕ} (hn : ↑n ≤ f.order) : (MvPowerSeries.homogeneousComponent n) (subst φ f) = MvPowerSeries.C ((algebraMap R S) ((coeff n) f)) * (MvPowerSeries.homogeneousComponent 1) φ ^ n

The lowest homogeneous component of a substitution. If φ is a multivariate power series of zero constant coefficient and f has order at least n, then the degree-n homogeneous component of f (φ) is c φ₁ ^ n, where c is the coefficient of Xⁿ in f and φ₁ is the linear part of φ.

theorem PowerSeries.coeff_subst_eq_sum_range_degree {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] {τ : Type u_4} {a : MvPowerSeries τ S} (ha : MvPowerSeries.constantCoeff a = 0) (f : PowerSeries R) (d : τ →₀ ℕ) : (MvPowerSeries.coeff d) (subst a f) = ∑ n ∈ Finset.range (Finsupp.degree d + 1), (coeff n) f • (MvPowerSeries.coeff d) (a ^ n)

The coefficient of X^d in f (a), for a of zero constant coefficient, is the finite sum ∑_{n ≤ |d|} fₙ [X^d] aⁿ: the powers aⁿ with n > |d| have order greater than |d|. This is the finite form of Mathlib's PowerSeries.coeff_subst.

theorem PowerSeries.coeff_subst_mem {S : Type u_3} [CommRing S] {τ : Type u_4} {A : Subring S} {a : MvPowerSeries τ S} (ha : HasSubst a) (ha' : ∀ (d : τ →₀ ℕ), (MvPowerSeries.coeff d) a ∈ A) {f : PowerSeries S} (hf : ∀ (n : ℕ), (coeff n) f ∈ A) (d : τ →₀ ℕ) : (MvPowerSeries.coeff d) (subst a f) ∈ A

If f and the substitutable series a have coefficients in a subring A, then so does f (a): it is the image of the substitution computed over A.

theorem PowerSeries.homogeneousComponent_subst_left_eq_C_mul_X_pow {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] {f : PowerSeries R} {φ : PowerSeries S} {n : ℕ} (hn : ↑n ≤ f.order) (hφ : constantCoeff φ = 0) (hφ₁ : (coeff 1) φ = 1) : (MvPowerSeries.homogeneousComponent n) (subst φ f) = MvPowerSeries.C ((algebraMap R S) ((coeff n) f)) * MvPowerSeries.X () ^ n

The degree-n part of f (φ) is a Xⁿ when f has order at least n and coefficient a of Xⁿ, and φ = X + ⋯.

theorem PowerSeries.homogeneousComponent_subst_right_eq_C_mul_X_pow {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] {f : PowerSeries S} {φ : PowerSeries R} {n : ℕ} (hn₀ : n ≠ 0) (hn : ↑n ≤ f.order) (hφ₁ : (coeff 1) φ = 1) : (MvPowerSeries.homogeneousComponent n) (subst f φ) = MvPowerSeries.C ((coeff n) f) * MvPowerSeries.X () ^ n

The degree-n part of φ (f) is a Xⁿ when f has order at least n ≥ 1 and coefficient a of Xⁿ, and φ = c + X + ⋯: the constant term c only contributes in degree 0, and the terms of φ of degree at least two contribute in degree at least 2 n.

theorem PowerSeries.hasSubst_pair {S : Type u_3} [CommRing S] {f g : PowerSeries S} (hf : constantCoeff f = 0) (hg : constantCoeff g = 0) : MvPowerSeries.HasSubst ![f, g]

Two series of zero constant coefficient can be substituted as a pair.

theorem PowerSeries.coeff_subst_update_add_X_pow_mul {R : Type u_2} {S : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [DecidableEq σ] (G : MvPowerSeries σ R) {a : σ → PowerSeries S} (ha : MvPowerSeries.HasSubst a) (ha₀ : ∀ (t : σ), constantCoeff (a t) = 0) (s : σ) (r : PowerSeries S) {m n : ℕ} (hm : m ≠ 0) (hn : n ≤ m) : (coeff n) (MvPowerSeries.subst (Function.update a s (a s + X ^ m * r)) G) = (coeff n) (MvPowerSeries.subst a G) + if n = m then (algebraMap R S) ((MvPowerSeries.coeff (Finsupp.single s 1)) G) * constantCoeff r else 0

Perturbing the entry a s of a substituted family a by X ^ m * r leaves the coefficients of degree below m unchanged, and changes the coefficient of degree m by r(0) times the coefficient of Xₛ in G. This is the one-variable case of MvPowerSeries.le_order_subst_update_add_sub.

theorem PowerSeries.exists_subst_add_X_pow_mul {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] (f : PowerSeries R) {a : PowerSeries S} (ha : constantCoeff a = 0) (r : PowerSeries S) {m : ℕ} (hm : m ≠ 0) : ∃ (s : PowerSeries S), subst (a + X ^ m * r) f = subst a f + X ^ m * s ∧ constantCoeff s = (algebraMap R S) ((coeff 1) f) * constantCoeff r

Perturbing an input of zero constant coefficient by X ^ m * r, for m ≠ 0, changes f by X ^ m * s, where s(0) is the linear coefficient of f times r(0).

theorem Continuous.powerSeries_subst {A : Type u_1} {R : Type u_2} {S : Type u_3} [TopologicalSpace A] [CommRing R] [TopologicalSpace R] [CommRing S] [TopologicalSpace S] [IsTopologicalRing S] [Algebra R S] [ContinuousSMul R S] {f : A → PowerSeries R} {g : A → PowerSeries S} (hf : Continuous f) (hg : Continuous g) (hg₀ : ∀ (a : A), PowerSeries.constantCoeff (g a) = 0) : Continuous fun (a : A) => PowerSeries.subst (g a) (f a)

Substitution is jointly continuous for coefficientwise continuous families, provided the inner series always has zero constant coefficient. No discrete coefficient topology is needed.

theorem AlgHom.constantCoeff_apply_X {K : Type u_1} [Field K] (σ : PowerSeries K →ₐ[K] PowerSeries K) : PowerSeries.constantCoeff (σ PowerSeries.X) = 0

Over a field K, every K-algebra endomorphism of K⟦X⟧ sends X to a series of zero constant coefficient.

theorem AlgHom.apply_eq_subst {K : Type u_1} [Field K] (σ : PowerSeries K →ₐ[K] PowerSeries K) (f : PowerSeries K) : σ f = PowerSeries.subst (σ PowerSeries.X) f

Over a field K, every K-algebra endomorphism σ of K⟦X⟧ is the substitution f ↦ f (σ X).

instance PowerSeries.isIntegrallyClosedIn (K : Type u_1) [Field K] : IsIntegrallyClosedIn K (PowerSeries K)

A field K is integrally closed in K⟦X⟧: the power series algebraic over K are the constants. A series f algebraic over K gives the algebraic series f - C (constantCoeff f) of zero constant coefficient, which therefore vanishes.

theorem TauCeti.hasSubst_binomialSeries_sub_one {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [BinomialRing R] (u : R) : PowerSeries.HasSubst (PowerSeries.binomialSeries S u - 1)

The binomial series (1 + X) ^ u - 1 has constant coefficient zero, so power series can be substituted into it.