The order of a convergent series over K = ℝ or ℂ, formally and at function level

The order μ(f) of a power series is Mathlib's MvPowerSeries.order (the least degree of a nonzero coefficient, ⊤ for 0); for K = ℝ it is the order μ_a(f) = max {k : f_a ∈ 𝔪_a^k} of a germ in [BM88, Definition 4.6, p. 23]. Orders add (MvPowerSeries.order_mul, the ring MvPowerSeries (Fin m) K having no zero divisors). At function level, μ(f) ≥ k iff every iterated derivative of order < k of the function evalSeries f vanishes at 0: the iterated derivative of order j is the symmetrization of the degree-j multilinear term (HasFPowerSeriesOnBall.iteratedFDeriv_eq_sum_of_completeSpace), which is zero when the degree-j coefficients vanish; conversely a vanishing derivative kills the homogeneous part of degree j as a function, hence as a polynomial (MvPolynomial.funext), hence coefficientwise. The function-level clause is what lets the order of a germ on a manifold be read off any convergent expansion (Hironaka/Manifold/IdealSheaf).

theorem Analytic.order_mul {K : Type u_1} [RCLike K] {m : ℕ} (f g : MvPowerSeries (Fin m) K) : (f * g).order = f.order + g.order

Orders add (Mathlib's MvPowerSeries.order_mul, order 0 = ⊤).

theorem Analytic.toFMS_eq_zero_of_coeff {K : Type u_1} [RCLike K] {m : ℕ} (f : MvPowerSeries (Fin m) K) {n : ℕ} (h : ∀ (ν : Fin m →₀ ℕ), Finsupp.degree ν = n → (MvPowerSeries.coeff ν) f = 0) : toFMS f n = 0

The degree-n term of toFMS f vanishes when the degree-n coefficients do.

theorem Analytic.le_order_iff_iteratedFDeriv_eq_zero {K : Type u_1} [RCLike K] {m : ℕ} {f : MvPowerSeries (Fin m) K} (hf : f ∈ Conv K m) (k : ℕ) : ↑k ≤ f.order ↔ ∀ j < k, iteratedFDeriv K j (evalSeries f) 0 = 0

At function level, μ(f) ≥ k iff all iterated derivatives of order < k of the function vanish at 0: the order of a germ in the sense of [BM88, Definition 4.6, p. 23].