domDomCongr_iteratedFDerivWithin — Mathlib

English

If a function has a power series on a ball, then the nth iterated derivative equals the sum over permutations of p_n.

Русский

Если функция имеет степенной ряд на шаре, то n-я итеративная производная равна сумме перестановок p_n.

LaTeX

$$$$ HasFPowerSeriesOnBall f p x r \\Rightarrow \\forall n\\ \\forall v: Fin n \\to E, \\ iteratedFDeriv 𝕜 n f x v = \\sum_{\\sigma \\in Perm(Fin n)} p n (v(\\sigma(1)),\\dots,v(\\sigma(n))). $$$$

Lean4

theorem domDomCongr_iteratedFDerivWithin (h : AnalyticOn 𝕜 f s) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) {n : ℕ}
    (σ : Perm (Fin n)) : (iteratedFDerivWithin 𝕜 n f s x).domDomCongr σ = iteratedFDerivWithin 𝕜 n f s x :=
  by
  ext
  exact h.iteratedFDerivWithin_comp_perm hs hx _ _

Похожие утверждения