Partial derivatives and the order of a multivariate power series

A partial derivative lowers the order of a multivariate power series by at most one. Over a ring without additive torsion the order is in turn detected by the partial derivatives: f has order at least n + 1 exactly when its constant coefficient vanishes and each of its partial derivatives has order at least n.

Applied to the Taylor expansion of a polynomial at a point, this is the characterization of the order of vanishing of the polynomial at the point by its partial derivatives (MvPolynomial.le_orderAt_iff_eval_foldl_pderiv).

Main results

• MvPowerSeries.le_order_pderiv: if n + 1 ≤ f.order then n ≤ (pderiv i f).order.
• MvPowerSeries.succ_le_order_iff: n + 1 ≤ f.order if and only if the constant coefficient of f vanishes and n ≤ (pderiv i f).order for every i.

theorem MvPowerSeries.le_order_pderiv {σ : Type u_1} {R : Type u_2} [CommSemiring R] {f : MvPowerSeries σ R} {n : ℕ} (h : ↑(n + 1) ≤ f.order) (i : σ) : ↑n ≤ ((pderiv i) f).order

theorem MvPowerSeries.succ_le_order_iff {σ : Type u_1} {R : Type u_2} [CommRing R] [IsAddTorsionFree R] {f : MvPowerSeries σ R} {n : ℕ} : ↑(n + 1) ≤ f.order ↔ constantCoeff f = 0 ∧ ∀ (i : σ), ↑n ≤ ((pderiv i) f).order

Over a ring without additive torsion, f has order at least n + 1 if and only if its constant coefficient vanishes and each of its partial derivatives has order at least n.