Orders of vanishing of products #
If the derivatives of order less than a of f and those of order less than b of g vanish at
x, then the derivatives of order less than a + b of the product f * g vanish at x: orders
of vanishing add under multiplication. This follows from the Leibniz bound
norm_iteratedFDeriv_mul_le, since every term of the Leibniz expansion of a derivative of order
n < a + b contains a derivative of f of order less than a or one of g of order less than
b.
This is the analytic half of the description of the powers of the vanishing ideal of a point by vanishing derivatives.
theorem
TauCeti.iteratedFDeriv_mul_eq_zero_of_lt_add
{𝕜 : Type u_1}
{E : Type u_2}
{A : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedRing A]
[NormedAlgebra 𝕜 A]
{f g : E → A}
{n a b : ℕ}
(hf : ContDiff 𝕜 (↑n) f)
(hg : ContDiff 𝕜 (↑n) g)
{x : E}
(hfa : ∀ i < a, iteratedFDeriv 𝕜 i f x = 0)
(hgb : ∀ i < b, iteratedFDeriv 𝕜 i g x = 0)
(hn : n < a + b)
:
Orders of vanishing add. If the derivatives of f of order less than a and those of
g of order less than b vanish at x, then the derivative of order n < a + b of f * g
vanishes at x.