IteratedDerivative.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.iterate_pderiv_monomial line 14

Source documentation

Repeated partial differentiation acts by a falling factorial on each monomial.

theorem iterate_pderiv_monomial (i : σ) (r : ℕ) (d : σ →₀ ℕ) (a : K) :
    (pderiv i)^[r] (monomial d a) =
      monomial (d - Finsupp.single i r) (a * (d i).descFactorial r) := by
…

theorem OAI.Problem335.iterate_pderiv_monomial_eq_zero line 30

Source documentation

Derivatives beyond a monomial's exponent vanish, in any characteristic.

theorem iterate_pderiv_monomial_eq_zero (i : σ) (r : ℕ) (d : σ →₀ ℕ)
    (a : K) (h : d i < r) :
    (pderiv i)^[r] (monomial d a) = 0 := by
…

theorem OAI.Problem335.coeff_iterate_pderiv line 37

Source documentation

Coefficients of a repeated derivative are shifted coefficients times a rising factorial.

theorem coeff_iterate_pderiv (i : σ) (r : ℕ) (p : MvPolynomial σ K)
    (m : σ →₀ ℕ) :
    ((pderiv i)^[r] p).coeff m =
      p.coeff (m + Finsupp.single i r) * (m i + 1).ascFactorial r := by
…