Formal partial derivatives of multivariate power series

This file defines MvPowerSeries.pderiv R i, the formal partial derivative of a multivariate power series with respect to variable i, as a Derivation R (MvPowerSeries σ R) (MvPowerSeries σ R).

See also PowerSeries.derivative for the univariate setting.

Main definitions

• MvPowerSeries.pderiv R i: the formal partial derivative with respect to i, as a derivation.

Main results

• MvPowerSeries.coeff_pderiv: coefficient formula coeff n (pderiv R i f) = coeff (n + single i 1) f * (n i + 1).
• MvPowerSeries.pderiv_coe: compatibility with MvPolynomial.pderiv.
• MvPowerSeries.trunc_pderiv: truncation commutes with partial differentiation.
• MvPowerSeries.pderiv.ext: a power series is determined by its constant term and its partial derivatives.
• MvPowerSeries.pderiv_pow: power rule.
• MvPowerSeries.pderiv_inv, MvPowerSeries.pderiv_inv': derivative of an inverse.

noncomputable def MvPowerSeries.pderivFun {σ : Type u_1} {R : Type u_2} [Semiring R] (i : σ) (f : MvPowerSeries σ R) : MvPowerSeries σ R

The underlying function of the formal partial derivative with respect to variable i. This is packaged as a derivation in MvPowerSeries.pderiv.

Equations

• MvPowerSeries.pderivFun i f d = (MvPowerSeries.coeff (d + Finsupp.single i 1)) f * (↑(d i) + 1)

theorem MvPowerSeries.coeff_pderivFun {σ : Type u_1} {R : Type u_2} [Semiring R] {i : σ} (f : MvPowerSeries σ R) (d : σ →₀ ℕ) : (coeff d) (pderivFun i f) = (coeff (d + Finsupp.single i 1)) f * (↑(d i) + 1)

theorem MvPowerSeries.pderivFun_add {σ : Type u_1} {R : Type u_2} [Semiring R] {i : σ} (f g : MvPowerSeries σ R) : pderivFun i (f + g) = pderivFun i f + pderivFun i g

theorem MvPowerSeries.pderivFun_C {σ : Type u_1} {R : Type u_2} [Semiring R] {i : σ} (r : R) : pderivFun i (C r) = 0

theorem MvPowerSeries.pderivFun_one {σ : Type u_1} {R : Type u_2} [Semiring R] {i : σ} : pderivFun i 1 = 0

noncomputable def MvPowerSeries.pderiv {σ : Type u_1} (R : Type u_2) [CommSemiring R] (i : σ) : Derivation R (MvPowerSeries σ R) (MvPowerSeries σ R)

The formal partial derivative of a multivariate formal power series with respect to variable i, as an R-derivation on MvPowerSeries σ R.

Equations

• MvPowerSeries.pderiv R i = { toFun := MvPowerSeries.pderivFun i, map_add' := ⋯, map_smul' := ⋯, map_one_eq_zero' := ⋯, leibniz' := ⋯ }

@[simp]

theorem MvPowerSeries.pderiv_C {σ : Type u_1} {R : Type u_2} [CommSemiring R] {i : σ} {r : R} : (pderiv R i) (C r) = 0

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

theorem MvPowerSeries.coeff_pderiv {σ : Type u_1} {R : Type u_2} [CommSemiring R] {i : σ} (f : MvPowerSeries σ R) (n : σ →₀ ℕ) : (coeff n) ((pderiv R i) f) = (coeff (n + Finsupp.single i 1)) f * (↑(n i) + 1)

theorem MvPowerSeries.pderiv_coe {σ : Type u_1} {R : Type u_2} [CommSemiring R] {i : σ} (f : MvPolynomial σ R) : (pderiv R i) ↑f = ↑((MvPolynomial.pderiv i) f)

@[simp]

theorem MvPowerSeries.pderiv_X_self {σ : Type u_1} {R : Type u_2} [CommSemiring R] {i : σ} : (pderiv R i) (X i) = 1

@[simp]

theorem MvPowerSeries.pderiv_X_of_ne {σ : Type u_1} {R : Type u_2} [CommSemiring R] {i j : σ} (h : j ≠ i) : (pderiv R i) (X j) = 0

theorem MvPowerSeries.pderiv_X {σ : Type u_1} {R : Type u_2} [CommSemiring R] [DecidableEq σ] (i j : σ) : (pderiv R i) (X j) = Pi.single i 1 j

theorem MvPowerSeries.trunc_pderiv {σ : Type u_1} {R : Type u_2} [CommSemiring R] [DecidableEq σ] {i : σ} (f : MvPowerSeries σ R) (n : σ →₀ ℕ) : (trunc R n) ((pderiv R i) f) = (MvPolynomial.pderiv i) ((trunc R (n + Finsupp.single i 1)) f)

theorem MvPowerSeries.pderiv_pow {σ : Type u_1} {R : Type u_2} [CommSemiring R] {i : σ} (g : MvPowerSeries σ R) (n : ℕ) : (pderiv R i) (g ^ n) = ↑n * g ^ (n - 1) * (pderiv R i) g

The partial derivative of g^n equals n * g^(n-1) * g'.

theorem MvPowerSeries.pderiv.ext {σ : Type u_1} {R : Type u_2} [CommRing R] [IsAddTorsionFree R] {f g : MvPowerSeries σ R} (hD : ∀ (i : σ), (pderiv R i) f = (pderiv R i) g) (hc : constantCoeff f = constantCoeff g) : f = g

If f and g have the same constant term and all partial derivatives, then they are equal.

The CommRing assumption is needed because the proof uses smul_right_inj, which requires cancellation of addition in R; IsAddTorsionFree alone does not suffice.

@[simp]

theorem MvPowerSeries.pderiv_inv {σ : Type u_1} {R : Type u_2} {i : σ} [CommRing R] (f : (MvPowerSeries σ R)ˣ) : (pderiv R i) ↑f⁻¹ = -↑f⁻¹ ^ 2 * (pderiv R i) ↑f

@[simp]

theorem MvPowerSeries.pderiv_invOf {σ : Type u_1} {R : Type u_2} {i : σ} [CommRing R] (f : MvPowerSeries σ R) [Invertible f] : (pderiv R i) ⅟f = -⅟f ^ 2 * (pderiv R i) f

@[simp]

theorem MvPowerSeries.pderiv_inv' {σ : Type u_1} {R : Type u_2} {i : σ} [Field R] (f : MvPowerSeries σ R) : (pderiv R i) f⁻¹ = -f⁻¹ ^ 2 * (pderiv R i) f