English
A continuous multilinear map f admits a Taylor series expansion up to infinity (top), with coefficients given by iteratedFDeriv, i.e., HasFTaylorSeriesUpTo ⊤ f (v ↦ f.iteratedFDeriv n v).
Русский
У непрерывной мультиленейной карты f существует разложение Тейлора до бесконечности, коэффициенты которого заданы через iteratedFDeriv.
LaTeX
$$$\text{HasFTaylorSeriesUpTo }\top f (v, n) = f.iteratedFDeriv(n, v).$$$
Lean4
theorem derivSeries_apply_diag (n : ℕ) (x : E) : derivSeries p n (fun _ ↦ x) x = (n + 1) • p (n + 1) fun _ ↦ x :=
by
simp only [derivSeries, compFormalMultilinearSeries_apply, changeOriginSeries, compContinuousMultilinearMap_coe,
ContinuousLinearEquiv.coe_coe, LinearIsometryEquiv.coe_coe, Function.comp_apply, ContinuousMultilinearMap.sum_apply,
map_sum, coe_sum', Finset.sum_apply, continuousMultilinearCurryFin1_apply, Matrix.zero_empty]
convert Finset.sum_const _
· rw [Fin.snoc_zero, changeOriginSeriesTerm_apply, Finset.piecewise_same, add_comm]
·
rw [← card, card_subtype, ← Finset.powerset_univ, ← Finset.powersetCard_eq_filter, Finset.card_powersetCard, ← card,
card_fin, eq_comm, add_comm, Nat.choose_succ_self_right]
