English
The n-th iterated derivative of an analytic function on a set is symmetric with respect to the order of taking derivatives; permuting arguments yields the same result.
Русский
n-я итеративная производная аналитической функции симметрична при перестановке аргументов.
LaTeX
$$$$iteratedFDerivWithin 𝕜 n f s x (v\\circ \\sigma) = iteratedFDerivWithin 𝕜 n f s x v,$$ for any permutation σ of Fin n.$$
Lean4
theorem iteratedFDerivSeries_eq_zero {k n : ℕ} (h : p (n + k) = 0) : p.iteratedFDerivSeries k n = 0 := by
induction k generalizing n with
| zero =>
ext
have : p n = 0 := p.congr_zero rfl h
simp [FormalMultilinearSeries.iteratedFDerivSeries, this]
| succ k ih =>
ext
simp only [iteratedFDerivSeries, Nat.succ_eq_add_one, ContinuousLinearMap.compFormalMultilinearSeries_apply,
ContinuousLinearMap.compContinuousMultilinearMap_coe, ContinuousLinearEquiv.coe_coe,
LinearIsometryEquiv.coe_toContinuousLinearEquiv, Function.comp_apply,
continuousMultilinearCurryLeftEquiv_symm_apply, ContinuousMultilinearMap.zero_apply,
ContinuousLinearMap.zero_apply, derivSeries_eq_zero _ (ih (p.congr_zero (Nat.succ_add_eq_add_succ _ _).symm h))]
