English
For complete codomains, the domCongr property holds for iterated derivatives under permutations.
Русский
Для полного пространства отображения сохраняется свойство domCongr для итеративных производных под перестановками.
LaTeX
$$$$ (\\iteratedFDerivWithin 𝕜 n f s x)\\mathrm{domDomCongr} \\sigma = \\iteratedFDerivWithin 𝕜 n f s x $$$$
Lean4
/-- The `n`-th iterated derivative of an analytic function on a set is symmetric. -/
theorem iteratedFDerivWithin_comp_perm (h : AnalyticOn 𝕜 f s) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) {n : ℕ}
(v : Fin n → E) (σ : Perm (Fin n)) : iteratedFDerivWithin 𝕜 n f s x (v ∘ σ) = iteratedFDerivWithin 𝕜 n f s x v :=
by
rcases h x hx with ⟨p, r, hp⟩
rw [hp.iteratedFDerivWithin_eq_sum h hs hx, hp.iteratedFDerivWithin_eq_sum h hs hx]
conv_rhs => rw [← Equiv.sum_comp (Equiv.mulLeft σ)]
simp only [coe_mulLeft, Perm.coe_mul, Function.comp_apply]
