theorem DifferentialOperators.pderiv_eq_zero_of_totalDegree_zero {σ : Type u_1} {R : Type u_2} [CommRing R] {p : MvPolynomial σ R} {j : σ} (h : p.totalDegree = 0) : (MvPolynomial.pderiv j) p = 0

A polynomial of total degree zero has zero partial derivative with respect to any variable.

theorem DifferentialOperators.totalDegree_pderiv_le {σ : Type u_1} {R : Type u_2} [CommRing R] {i : σ} {p : MvPolynomial σ R} : ((MvPolynomial.pderiv i) p).totalDegree ≤ p.totalDegree - 1

The total degree of a partial derivative ∂ᵢ p is at most p.totalDegree - 1.

theorem DifferentialOperators.totalDegree_nsmul_le {σ : Type u_1} {R : Type u_2} [CommRing R] (k : ℕ) (p : MvPolynomial σ R) : (k • p).totalDegree ≤ p.totalDegree

The natural-number scalar multiple k • p has total degree at most p.totalDegree.

noncomputable def DifferentialOperators.iteratedPartialDeriv {n : ℕ} (js : List (Fin n)) (f : EuclideanSpace ℝ (Fin n) → ℂ) : EuclideanSpace ℝ (Fin n) → ℂ

Iterated partial derivative of a complex-valued function on ℝⁿ along the list of coordinate directions js, applied left-to-right via List.foldl.

@[simp]

theorem DifferentialOperators.iteratedPartialDeriv_cons {n : ℕ} (j : Fin n) (rest : List (Fin n)) (f : EuclideanSpace ℝ (Fin n) → ℂ) : iteratedPartialDeriv (j :: rest) f = iteratedPartialDeriv rest fun (ξ : EuclideanSpace ℝ (Fin n)) => (fderiv ℝ f ξ) (EuclideanSpace.single j 1)

Unfolding iteratedPartialDeriv on a cons list: differentiating along j :: rest is differentiating along rest the function obtained by taking one partial derivative along j.

def DifferentialOperators.reciprocalNumerator {n : ℕ} (P : MvPolynomial (Fin n) ℂ) : List (Fin n) → MvPolynomial (Fin n) ℂ

Recursive definition of the numerator polynomial obtained when differentiating 1 / P along the list of directions js; see Lemma 11.14 of Melrose for the resulting structural identity.

@[simp]

theorem DifferentialOperators.reciprocalNumerator_totalDegree {n : ℕ} (P : MvPolynomial (Fin n) ℂ) (m : ℕ) (hm : 1 ≤ m) (hdeg : P.totalDegree ≤ m) (js : List (Fin n)) : (reciprocalNumerator P js).totalDegree ≤ (m - 1) * js.length

The total degree of reciprocalNumerator P js is bounded by (m - 1) * js.length whenever P.totalDegree ≤ m and m ≥ 1.

def DifferentialOperators.foldNumerator {n : ℕ} (P : MvPolynomial (Fin n) ℂ) : MvPolynomial (Fin n) ℂ → ℕ → List (Fin n) → MvPolynomial (Fin n) ℂ

Left-fold version of the reciprocal numerator construction, threading a running numerator Q and a running power index k along the list of differentiation directions.

@[simp]

theorem DifferentialOperators.foldNumerator_cons {n : ℕ} (P Q : MvPolynomial (Fin n) ℂ) (k : ℕ) (j : Fin n) (rest : List (Fin n)) : foldNumerator P Q k (j :: rest) = foldNumerator P (P * (MvPolynomial.pderiv j) Q - k • (Q * (MvPolynomial.pderiv j) P)) (k + 1) rest

Cons-unfolding lemma for foldNumerator: prepending a direction performs one quotient-rule step on the running numerator and increments the power index.

theorem DifferentialOperators.pderiv_pderiv_comm {σ : Type u_3} {R : Type u_4} [CommSemiring R] (i j : σ) (p : MvPolynomial σ R) : (MvPolynomial.pderiv i) ((MvPolynomial.pderiv j) p) = (MvPolynomial.pderiv j) ((MvPolynomial.pderiv i) p)

Partial derivatives on a multivariate polynomial commute: ∂ᵢ ∂ⱼ p = ∂ⱼ ∂ᵢ p.

theorem DifferentialOperators.foldNumerator_append {n : ℕ} (P Q : MvPolynomial (Fin n) ℂ) (k : ℕ) (js₁ js₂ : List (Fin n)) : foldNumerator P Q k (js₁ ++ js₂) = foldNumerator P (foldNumerator P Q k js₁) (k + js₁.length) js₂

Concatenation lemma: folding along js₁ ++ js₂ equals folding along js₂ starting from the result of folding along js₁, with the running index shifted by js₁.length.

theorem DifferentialOperators.reciprocalNumerator_append_singleton {n : ℕ} (P : MvPolynomial (Fin n) ℂ) (js : List (Fin n)) (j : Fin n) : reciprocalNumerator P (js ++ [j]) = P * (MvPolynomial.pderiv j) (reciprocalNumerator P js) - (1 + js.length) • (reciprocalNumerator P js * (MvPolynomial.pderiv j) P)

Append-singleton recursion for reciprocalNumerator: appending a single direction j to js applies one more quotient-rule step.

theorem DifferentialOperators.foldNumerator_eq_reciprocalNumerator {n : ℕ} (P : MvPolynomial (Fin n) ℂ) (js : List (Fin n)) : foldNumerator P 1 1 js = reciprocalNumerator P js

The fold form foldNumerator P 1 1 js agrees with the recursive form reciprocalNumerator P js.

theorem DifferentialOperators.iteratedPartialDeriv_eventuallyEq_nhds {n : ℕ} {g₁ g₂ : EuclideanSpace ℝ (Fin n) → ℂ} {ξ : EuclideanSpace ℝ (Fin n)} (js : List (Fin n)) (heq : g₁ =ᶠ[nhds ξ] g₂) : iteratedPartialDeriv js g₁ ξ = iteratedPartialDeriv js g₂ ξ

If two functions agree on a neighborhood of ξ, then their iterated partial derivatives along js agree at ξ.

theorem DifferentialOperators.foldNumerator_identity {n : ℕ} (P Q : MvPolynomial (Fin n) ℂ) (k : ℕ) (js : List (Fin n)) (ξ : EuclideanSpace ℝ (Fin n)) : evalAtReal P ξ ≠ 0 → iteratedPartialDeriv js (fun (ξ' : EuclideanSpace ℝ (Fin n)) => evalAtReal Q ξ' / evalAtReal P ξ' ^ k) ξ = evalAtReal (foldNumerator P Q k js) ξ / evalAtReal P ξ ^ (k + js.length)

Identity matching repeated partial differentiation of Q / Pᵏ (in a neighborhood where P ≠ 0) with foldNumerator P Q k js divided by P^(k + js.length).

theorem DifferentialOperators.reciprocal_poly_analytic_identity {n : ℕ} (P : MvPolynomial (Fin n) ℂ) (js : List (Fin n)) (ξ : EuclideanSpace ℝ (Fin n)) : evalAtReal P ξ ≠ 0 → iteratedPartialDeriv js (polyReciprocal P) ξ = evalAtReal (reciprocalNumerator P js) ξ / evalAtReal P ξ ^ (1 + js.length)

Analytic identity for the reciprocal polynomial: where P ≠ 0, the iterated partial derivative of 1 / P equals reciprocalNumerator P js divided by P^(1 + js.length).

theorem DifferentialOperators.reciprocal_poly_structural {n : ℕ} (P : MvPolynomial (Fin n) ℂ) (m : ℕ) (hm : 1 ≤ m) (hdeg : P.totalDegree ≤ m) (js : List (Fin n)) : ∃ (L : MvPolynomial (Fin n) ℂ), L.totalDegree ≤ (m - 1) * js.length ∧ ∀ (ξ : EuclideanSpace ℝ (Fin n)), evalAtReal P ξ ≠ 0 → iteratedPartialDeriv js (polyReciprocal P) ξ = evalAtReal L ξ / evalAtReal P ξ ^ (1 + js.length)

Structural form of Melrose Lemma 11.14: there exists a polynomial L of total degree at most (m - 1) * js.length such that the iterated partial derivative of 1 / P (where P ≠ 0) equals L / P^(1 + js.length).