Partial derivatives of multivariate power series

DefinitionIterated partial derivative of a multivariate power series#✓fully proved

Partial derivatives in list order, with the first entry applied first, as a linear map.

noncomputable def iteratedPDeriv (L : List σ) :
    MvPowerSeries σ R →ₗ[R] MvPowerSeries σ R :=
  L.foldr (fun i D => D.comp (pderiv i).toLinearMap) LinearMap.id

Used by 6

Used byFactorial times a coefficient is a constant term of an iterated derivative · Rational factorial coefficient as a constant term of an iterated derivative · Factorial-weighted coefficient of an iterated partial derivative · Rational factorial-weighted coefficient of an iterated derivative · Iterated partial derivatives along concatenated lists compose · A partial derivative commutes with iterated partial derivatives

TheoremIterated partial derivatives along concatenated lists compose#✓fully proved

Concatenating lists composes the second iterated derivative after the first.

theorem iteratedPDeriv_append (L K : List σ) :
    iteratedPDeriv (R := R) (L ++ K) = (iteratedPDeriv K).comp (iteratedPDeriv L)

Uses 1

Statement usesIterated partial derivative of a multivariate power series

TheoremFormal partial derivatives commute#✓fully proved

Two formal partial derivatives commute.

theorem pderiv_pderiv (i j : σ) (F : MvPowerSeries σ R) :
    pderiv i (pderiv j F) = pderiv j (pderiv i F)

Used by 1

Used byA partial derivative commutes with iterated partial derivatives

TheoremA partial derivative commutes with iterated partial derivatives#✓fully proved

A partial derivative commutes with any list of partial derivatives.

theorem pderiv_iteratedPDeriv (i : σ) (L : List σ) (F : MvPowerSeries σ R) :
    pderiv i (iteratedPDeriv L F) = iteratedPDeriv L (pderiv i F)

Uses 2

Statement usesIterated partial derivative of a multivariate power series

Proof usesFormal partial derivatives commute

TheoremVariable multiplicities of a list as a sum of singleton multi-indices#✓fully proved

List variable multiplicities equal the sum of singleton multi-indices.

theorem Multiset.toFinsupp_coe_list_eq_sum {σ : Type*} [DecidableEq σ] (L : List σ) :
    Multiset.toFinsupp (L : Multiset σ) = (L.map fun i => Finsupp.single i 1).sum

TheoremFactorial-weighted coefficient of an iterated partial derivative#✓fully proved

The factorial-weighted coefficient after iterated differentiation. No factorial is cancelled, so this identity also holds in positive characteristic.

theorem factorial_smul_coeff_iteratedPDeriv (L : List σ) (β : σ →₀ ℕ)
    (F : MvPowerSeries σ R) :
    (β + Multiset.toFinsupp (L : Multiset σ)).prod (fun _ n => n.factorial) •
        coeff (β + Multiset.toFinsupp (L : Multiset σ)) F =
      β.prod (fun _ n => n.factorial) • coeff β (iteratedPDeriv L F)

Uses 1 · Used by 2

Statement usesIterated partial derivative of a multivariate power series

Used byFactorial times a coefficient is a constant term of an iterated derivative · Rational factorial-weighted coefficient of an iterated derivative

TheoremFactorial times a coefficient is a constant term of an iterated derivative#✓fully proved

A monomial's factorial times its coefficient is the constant coefficient of the corresponding iterated partial derivative.

theorem factorial_smul_coeff_eq_constantCoeff_iteratedPDeriv (L : List σ)
    (F : MvPowerSeries σ R) :
    (Multiset.toFinsupp (L : Multiset σ)).prod (fun _ n => n.factorial) •
        coeff (Multiset.toFinsupp (L : Multiset σ)) F =
      constantCoeff (iteratedPDeriv L F)

Uses 2 · Used by 1

Statement usesIterated partial derivative of a multivariate power series

Proof usesFactorial-weighted coefficient of an iterated partial derivative

Used byRational factorial coefficient as a constant term of an iterated derivative

TheoremRational factorial-weighted coefficient of an iterated derivative#✓fully proved

The source rational-factorial scalar equation, obtained by casting the natural factorial product and its scalar action.

theorem factorial_smul_coeff_iteratedPDeriv_rat (L : List σ) (β : σ →₀ ℕ)
    (F : MvPowerSeries σ R) :
    (β + Multiset.toFinsupp (L : Multiset σ)).prod (fun _ n => (n.factorial : ℚ)) •
        coeff (β + Multiset.toFinsupp (L : Multiset σ)) F =
      β.prod (fun _ n => (n.factorial : ℚ)) • coeff β (iteratedPDeriv L F)

Uses 2

Statement usesIterated partial derivative of a multivariate power series

Proof usesFactorial-weighted coefficient of an iterated partial derivative

TheoremRational factorial coefficient as a constant term of an iterated derivative#✓fully proved

The source rational-factorial constant coefficient equation.

theorem factorial_smul_coeff_eq_constantCoeff_iteratedPDeriv_rat (L : List σ)
    (F : MvPowerSeries σ R) :
    (Multiset.toFinsupp (L : Multiset σ)).prod (fun _ n => (n.factorial : ℚ)) •
        coeff (Multiset.toFinsupp (L : Multiset σ)) F =
      constantCoeff (iteratedPDeriv L F)

Uses 2

Statement usesIterated partial derivative of a multivariate power series

Proof usesFactorial times a coefficient is a constant term of an iterated derivative

DefinitionFormal linear form in multivariate power series#✓fully proved

The formal linear form with variable coefficient family b : σ → R.

Its coefficient at d is the sum of b i over the support of d when d has total degree one, and zero otherwise.

MvPowerSeries.linearForm · 18 lines

noncomputable def linearForm {σ R : Type*} [CommSemiring R] :
    (σ → R) →ₗ[R] MvPowerSeries σ R where
  toFun b d := if d.degree = 1 then ∑ i ∈ d.support, b i else 0
  map_add' b c := by
    ext d
    change (if d.degree = 1 then ∑ i ∈ d.support, (b i + c i) else 0) =
      (if d.degree = 1 then ∑ i ∈ d.support, b i else 0) +
        if d.degree = 1 then ∑ i ∈ d.support, c i else 0
    by_cases h : d.degree = 1
    · simp only [ite_eq_left h, Finset.sum_add_distrib]
    · simp only [ite_eq_right h, zero_add]
  map_smul' r b := by
    ext d
    change (if d.degree = 1 then ∑ i ∈ d.support, r * b i else 0) =
      r * if d.degree = 1 then ∑ i ∈ d.support, b i else 0
    by_cases h : d.degree = 1
    · simp only [ite_eq_left h, Finset.mul_sum]
    · simp only [ite_eq_right h, mul_zero]

Used by 5

Used byCoefficient formula for a formal linear form · Coefficient of a single variable in a formal linear form · A formal linear form has zero constant coefficient · Coefficient ring maps commute with formal linear forms · Partial derivative of a formal linear form

TheoremCoefficient formula for a formal linear form#✓fully proved

The coefficient formula defining a formal linear form.

@[simp] theorem coeff_linearForm {σ R : Type*} [CommSemiring R]
    (b : σ → R) (d : σ →₀ ℕ) :
    coeff d (linearForm b) =
      if d.degree = 1 then ∑ i ∈ d.support, b i else 0

Uses 1 · Used by 3

Statement usesFormal linear form in multivariate power series

Used byA formal linear form has zero constant coefficient · Coefficient ring maps commute with formal linear forms · Partial derivative of a formal linear form

TheoremCoefficient of a single variable in a formal linear form#✓fully proved

The coefficient of variable i is the prescribed coefficient b i.

@[simp] theorem coeff_linearForm_single {σ R : Type*} [CommSemiring R]
    (b : σ → R) (i : σ) :
    coeff (Finsupp.single i 1) (linearForm b) = b i

Uses 1

Statement usesFormal linear form in multivariate power series

TheoremA formal linear form has zero constant coefficient#✓fully proved

A formal linear form has zero constant coefficient.

@[simp] theorem constantCoeff_linearForm {σ R : Type*} [CommSemiring R]
    (b : σ → R) : constantCoeff (linearForm b) = 0

Uses 2

Statement usesFormal linear form in multivariate power series

Proof usesCoefficient formula for a formal linear form

TheoremPartial derivative of a formal linear form#✓fully proved

The partial derivative of a formal linear form is its corresponding constant coefficient.

@[simp] theorem pderiv_linearForm {σ R : Type*} [CommSemiring R]
    (b : σ → R) (i : σ) : pderiv i (linearForm b) = C (b i)

Uses 2

Statement usesFormal linear form in multivariate power series

Proof usesCoefficient formula for a formal linear form

TheoremCoefficient ring maps commute with formal linear forms#✓fully proved

Mapping the coefficient ring commutes with forming a formal linear form.

theorem map_linearForm {σ R S : Type*} [CommSemiring R] [CommSemiring S]
    (f : R →+* S) (b : σ → R) :
    map f (linearForm b) = linearForm (fun i => f (b i))

Uses 2

Statement usesFormal linear form in multivariate power series

Proof usesCoefficient formula for a formal linear form

15 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.