Mixed partial derivatives of polynomials

DefinitionMixed differential operator#✓fully proved

Let \(R\) be a commutative ring, let \(\sigma\) be an index type, and write \(\partial_s\) for the partial derivative with respect to \(x_s\) on the polynomial ring \(R[x_s : s \in \sigma]\). For a finite list \((i_1, \dots, i_k)\) of indices in \(\sigma\) (repetitions allowed) and a polynomial \(p \in R[x_s : s \in \sigma]\), the mixed differential of \(p\) along the list is \((1 - \partial_{i_k}) \cdots (1 - \partial_{i_1})\, p\): the operator \(1 - \partial_{i_1}\) is applied first and \(1 - \partial_{i_k}\) last. Along the empty list it is \(p\).

public noncomputable def mixedDifferential {σ R : Type*} [CommRing R]
    (indices : List σ) (p : MvPolynomial σ R) : MvPolynomial σ R :=
  indices.foldl (fun q i ↦ q - pderiv i q) p

Used by 15

Used byMixed differential along a concatenated list · Mixed differential along a list with a given first index · The mixed differential ignores the order of the indices · Mixed differential along the empty list · Partial derivatives commute with the mixed differential · The mixed differential preserves stability · The mixed differential preserves real stability · Mixed characteristic polynomial · Mixed characteristic polynomials of outer products · Mixed characteristic polynomial of a single \(1 \times 1\) matrix · Mixed characteristic polynomials of positive semidefinite matrices are real-rooted · Marcus--Spielman--Srivastava barrier bound · Mixed characteristic polynomials are monic · Degree of a mixed characteristic polynomial · The mixed characteristic polynomial is affine in each matrix

TheoremMixed differential along the empty list#✓fully proved

Let \(R\) be a commutative ring, let \(\sigma\) be an index type, and let \(p \in R[x_s : s \in \sigma]\). The mixed differential of \(p\) along the empty list of indices is \(p\) itself.

@[simp]
public theorem mixedDifferential_nil {σ R : Type*} [CommRing R]
    (p : MvPolynomial σ R) : mixedDifferential [] p = p

Uses 1 · Used by 3

Statement usesMixed differential operator

Used byThe mixed differential preserves stability · The mixed differential preserves real stability · Mixed characteristic polynomials of outer products

TheoremMixed differential along a list with a given first index#✓fully proved

Let \(R\) be a commutative ring, let \(\sigma\) be an index type, let \(i \in \sigma\), let \(L\) be a finite list of indices in \(\sigma\), and let \(p \in R[x_s : s \in \sigma]\). The mixed differential of \(p\) along the list that starts with \(i\) and continues with \(L\) equals the mixed differential along \(L\) of \(p - \partial_i p\), where \(\partial_i\) is the partial derivative with respect to \(x_i\).

public theorem mixedDifferential_cons {σ R : Type*} [CommRing R]
    (i : σ) (is : List σ) (p : MvPolynomial σ R) :
    mixedDifferential (i :: is) p = mixedDifferential is (p - pderiv i p)

Uses 1 · Used by 10

Statement usesMixed differential operator

Used byThe mixed differential ignores the order of the indices · Partial derivatives commute with the mixed differential · The mixed differential preserves stability · The mixed differential preserves real stability · Mixed characteristic polynomials of outer products · Mixed characteristic polynomials of positive semidefinite matrices are real-rooted · Marcus--Spielman--Srivastava barrier bound · Mixed characteristic polynomials are monic · Degree of a mixed characteristic polynomial · The mixed characteristic polynomial is affine in each matrix

TheoremThe mixed differential ignores the order of the indices#✓fully proved

Let \(R\) be a commutative ring, let \(\sigma\) be an index type, and let \(p \in R[x_s : s \in \sigma]\). If two finite lists \(L\) and \(L'\) of indices in \(\sigma\) are permutations of each other, then the mixed differentials of \(p\) along \(L\) and along \(L'\) are equal.

public theorem mixedDifferential_eq_of_perm {σ R : Type*} [CommRing R]
    {is js : List σ} (h : is.Perm js) (p : MvPolynomial σ R) :
    mixedDifferential is p = mixedDifferential js p

Uses 2 · Used by 2

Statement usesMixed differential operator

Proof usesMixed differential along a list with a given first index

Used byMixed characteristic polynomials of outer products · The mixed characteristic polynomial is affine in each matrix

TheoremMixed differential along a concatenated list#✓fully proved

Let \(R\) be a commutative ring, let \(\sigma\) be an index type, let \(p \in R[x_s : s \in \sigma]\), and let \(L\) and \(L'\) be finite lists of indices in \(\sigma\). The mixed differential of \(p\) along the concatenation of \(L\) followed by \(L'\) equals the mixed differential along \(L'\) of the mixed differential of \(p\) along \(L\).

public theorem mixedDifferential_append {σ R : Type*} [CommRing R]
    (is js : List σ) (p : MvPolynomial σ R) :
    mixedDifferential (is ++ js) p = mixedDifferential js (mixedDifferential is p)

Uses 1 · Used by 1

Statement usesMixed differential operator

Used byMixed characteristic polynomials of outer products

TheoremPartial derivatives commute with the mixed differential#✓fully proved

Let \(R\) be a commutative ring, let \(i \in \sigma\), let \(L\) be a finite list of indices in \(\sigma\), and let \(p \in R[x_s : s \in \sigma]\). Writing \(\partial_i\) for the partial derivative with respect to \(x_i\), the partial derivative \(\partial_i\) of the mixed differential of \(p\) along \(L\) equals the mixed differential along \(L\) of \(\partial_i p\).

public theorem pderiv_mixedDifferential {σ R : Type*} [CommRing R]
    (i : σ) (is : List σ) (p : MvPolynomial σ R) :
    pderiv i (mixedDifferential is p) = mixedDifferential is (pderiv i p)

Uses 2 · Used by 1

Statement usesMixed differential operator

Proof usesMixed differential along a list with a given first index

Used byMixed characteristic polynomials of outer products

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.