English
For a regular analytic function, the nth iterated derivative commutes with permutations of the coordinates; domCongr equivalence holds.
Русский
Для аналитической функции производная n-го порядка коммутирует с перестановками координат.
LaTeX
$$$$ (\\iteratedFDerivWithin 𝕜 n f s x)\\!\\!\\!\\mathrm{domDomCongr} \\sigma = \\iteratedFDerivWithin 𝕜 n f s x, $$$$
Lean4
/-- If the `n`-th term in a power series is zero, then the `n`-th derivative of the corresponding
function vanishes. -/
theorem iteratedFDerivWithin_eq_zero (h : HasFPowerSeriesWithinOnBall f p s x r) (h' : AnalyticOn 𝕜 f s)
(hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) {n : ℕ} (hn : p n = 0) : iteratedFDerivWithin 𝕜 n f s x = 0 :=
by
have : iteratedFDerivWithin 𝕜 n f s x = p.iteratedFDerivSeries n 0 (fun _ ↦ 0) :=
((h.iteratedFDerivWithin h' n hu hx).coeff_zero _).symm
rw [this, p.iteratedFDerivSeries_eq_zero (p.congr_zero (Nat.zero_add n).symm hn), ContinuousMultilinearMap.zero_apply]
