English
If a function has a power series on a ball, then its nth iterated derivative equals the sum over all permutations of p n applied to permuted arguments.
Русский
Если функция имеет степенной ряд на шаре, то ее n-я итеративная производная равна сумме по всем перестановкам p_n по переставленным аргументам.
LaTeX
$$$$ iteratedFDerivWithin 𝕜 n f s x v = \\sum_{\\sigma \\in Perm(Fin n)} p n (v(\\sigma(1)),\\dots, v(\\sigma(n))). $$$$
Lean4
theorem iteratedFDeriv_comp_diagonal {n : ℕ} (f : E [×n]→L[𝕜] F) (x : E) (v : Fin n → E) :
iteratedFDeriv 𝕜 n (fun x ↦ f (fun _ ↦ x)) x v = ∑ σ : Perm (Fin n), f (fun i ↦ v (σ i)) :=
by
rw [← sum_comp (Equiv.inv (Perm (Fin n)))]
let g : E →L[𝕜] (Fin n → E) := ContinuousLinearMap.pi (fun i ↦ ContinuousLinearMap.id 𝕜 E)
change iteratedFDeriv 𝕜 n (f ∘ g) x v = _
rw [ContinuousLinearMap.iteratedFDeriv_comp_right _ f.contDiff _ le_rfl, f.iteratedFDeriv_eq]
simp only [ContinuousMultilinearMap.iteratedFDeriv, ContinuousMultilinearMap.compContinuousLinearMap_apply,
ContinuousMultilinearMap.sum_apply, ContinuousMultilinearMap.iteratedFDerivComponent_apply, Set.mem_range,
Pi.compRightL_apply]
rw [← sum_comp (Equiv.embeddingEquivOfFinite (Fin n))]
congr with σ
congr with i
have A : ∃ y, σ y = i :=
by
have : Function.Bijective σ := (Fintype.bijective_iff_injective_and_card _).2 ⟨σ.injective, rfl⟩
exact this.surjective i
rcases A with ⟨y, rfl⟩
simp only [EmbeddingLike.apply_eq_iff_eq, exists_eq, ↓reduceDIte, Function.Embedding.toEquivRange_symm_apply_self,
ContinuousLinearMap.coe_pi', ContinuousLinearMap.coe_id', id_eq, g]
congr 1
symm
simp [inv_apply, Perm.inv_def, ofBijective_symm_apply_apply, Function.Embedding.equivOfFiniteSelfEmbedding]
