Formal partial derivatives of multivariate power series

MvPowerSeries.pderiv s is the formal partial derivative with respect to the variable s, as an R-linear map. Beyond the basic calculus (MvPowerSeries.pderiv_C, MvPowerSeries.pderiv_X, compatibility with polynomials MvPowerSeries.pderiv_coe), the Leibniz rule (MvPowerSeries.pderiv_mul) and the chain rule for substitution (MvPowerSeries.pderiv_subst) are proved by continuity and density from the polynomial case: both sides are continuous for the product topologies with any ring topology, so the proofs instal the discrete topology and the statements remain topology-free.

Also provides MvPowerSeries.continuous_subst: substitution is continuous for the product topologies over a topological ring of coefficients — each coefficient of subst a f is a fixed finite linear combination of coefficients of f.

theorem MvPowerSeries.continuous_subst' {σ : Type u_1} {R : Type u_2} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] {τ : Type u_3} {a : τ → MvPowerSeries σ R} (ha : HasSubst a) : Continuous (subst a)

Substitution of power series is continuous, coefficientwise: each coefficient of subst a f is a fixed finite linear combination of coefficients of f. This generalizes MvPowerSeries.continuous_subst from discrete coefficients to any topological ring of coefficients.

theorem MvPowerSeries.constantCoeff_subst_of_constantCoeff_zero {σ : Type u_1} {R : Type u_2} [CommRing R] {τ : Type u_3} {a : τ → MvPowerSeries σ R} (ha : HasSubst a) (ha' : ∀ (s : τ), constantCoeff (a s) = 0) (f : MvPowerSeries τ R) : constantCoeff (subst a f) = constantCoeff f

Substitution along families with vanishing constant coefficients preserves the constant coefficient.

noncomputable def MvPowerSeries.pderiv {σ : Type u_1} {R : Type u_2} [CommRing R] (s : σ) : MvPowerSeries σ R →ₗ[R] MvPowerSeries σ R

The formal partial derivative of a multivariate power series.

Equations

• MvPowerSeries.pderiv s = { toFun := fun (h : MvPowerSeries σ R) (d : σ →₀ ℕ) => ↑(d s + 1) * (MvPowerSeries.coeff (d + Finsupp.single s 1)) h, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem MvPowerSeries.coeff_pderiv {σ : Type u_1} {R : Type u_2} [CommRing R] (s : σ) (h : MvPowerSeries σ R) (d : σ →₀ ℕ) : (coeff d) ((pderiv s) h) = ↑(d s + 1) * (coeff (d + Finsupp.single s 1)) h

theorem MvPowerSeries.pderiv_coe {σ : Type u_1} {R : Type u_2} [CommRing R] (s : σ) (p : MvPolynomial σ R) : (pderiv s) ↑p = ↑((MvPolynomial.pderiv s) p)

@[simp]

theorem MvPowerSeries.pderiv_C {σ : Type u_1} {R : Type u_2} [CommRing R] (s : σ) (c : R) : (pderiv s) (C c) = 0

@[simp]

theorem MvPowerSeries.pderiv_one {σ : Type u_1} {R : Type u_2} [CommRing R] (s : σ) : (pderiv s) 1 = 0

theorem MvPowerSeries.continuous_pderiv {σ : Type u_1} {R : Type u_2} [CommRing R] [TopologicalSpace R] [IsTopologicalSemiring R] (s : σ) : Continuous ⇑(pderiv s)

theorem MvPowerSeries.pderiv_mul {σ : Type u_1} {R : Type u_2} [CommRing R] (s : σ) (f g : MvPowerSeries σ R) : (pderiv s) (f * g) = f * (pderiv s) g + (pderiv s) f * g

The Leibniz rule for formal partial derivatives of power series.

@[simp]

theorem MvPowerSeries.pderiv_X {σ : Type u_1} {R : Type u_2} [CommRing R] [DecidableEq σ] (s t : σ) : (pderiv s) (X t) = if t = s then 1 else 0

theorem MvPowerSeries.pderiv_subst {σ : Type u_1} {R : Type u_2} [CommRing R] {τ : Type u_3} [Fintype τ] {a : τ → MvPowerSeries σ R} (ha : HasSubst a) (s : σ) (f : MvPowerSeries τ R) : (pderiv s) (subst a f) = ∑ t : τ, subst a ((pderiv t) f) * (pderiv s) (a t)

The chain rule for formal partial derivatives of a substitution.

theorem MvPowerSeries.pderiv_comm {σ : Type u_1} {R : Type u_2} [CommRing R] (s t : σ) (h : MvPowerSeries σ R) : (pderiv s) ((pderiv t) h) = (pderiv t) ((pderiv s) h)

Formal partial derivatives commute.

theorem MvPowerSeries.pderiv_subst_eq_zero {σ : Type u_1} {R : Type u_2} [CommRing R] {τ : Type u_3} [Finite τ] {a : τ → MvPowerSeries σ R} (ha : HasSubst a) (s : σ) (hz : ∀ (t : τ), (pderiv s) (a t) = 0) (f : MvPowerSeries τ R) : (pderiv s) (subst a f) = 0

A substitution whose family is annihilated by ∂_s is annihilated by ∂_s.

theorem MvPowerSeries.coeff_X_mul_pderiv {σ : Type u_1} {R : Type u_2} [CommRing R] (s : σ) (f : MvPowerSeries σ R) (d : σ →₀ ℕ) : (coeff d) (X s * (pderiv s) f) = ↑(d s) * (coeff d) f

theorem MvPowerSeries.coeff_sum_X_mul_pderiv {σ : Type u_1} {R : Type u_2} [CommRing R] [Fintype σ] (f : MvPowerSeries σ R) (d : σ →₀ ℕ) : (coeff d) (∑ s : σ, X s * (pderiv s) f) = ↑(Finsupp.degree d) * (coeff d) f

The Euler identity for formal power series: the operator ∑ s, X s * ∂/∂X s acts on the degree-n homogeneous part as multiplication by n.

theorem MvPowerSeries.eq_zero_of_pderiv_eq_zero {σ : Type u_1} {R : Type u_2} [CommRing R] [NoZeroSMulDivisors ℕ R] {f : MvPowerSeries σ R} (h : ∀ (s : σ), (pderiv s) f = 0) (h0 : constantCoeff f = 0) : f = 0

A power series with zero constant term all of whose partial derivatives vanish is zero, provided the coefficient ring has no additive torsion (e.g. characteristic zero domains).

theorem MvPowerSeries.coeff_rename_equiv {σ : Type u_1} {R : Type u_2} [CommRing R] {τ : Type u_3} (e : σ ≃ τ) (f : MvPowerSeries σ R) (d : τ →₀ ℕ) : (coeff d) ((rename ⇑e) f) = (coeff (Finsupp.equivMapDomain e.symm d)) f

theorem MvPowerSeries.rename_pderiv {σ : Type u_1} {R : Type u_2} [CommRing R] {τ : Type u_3} (e : σ ≃ τ) (s : σ) (f : MvPowerSeries σ R) : (rename ⇑e) ((pderiv s) f) = (pderiv (e s)) ((rename ⇑e) f)

Formal partial derivatives commute with variable renaming along an equivalence.

theorem MvPowerSeries.map_pderiv {σ : Type u_1} {R : Type u_2} [CommRing R] {S : Type u_3} [CommRing S] (f : R →+* S) (s : σ) (g : MvPowerSeries σ R) : (map f) ((pderiv s) g) = (pderiv s) ((map f) g)

Formal partial derivatives commute with a coefficient ring homomorphism.