iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition

English

AnalyticAt implies HasFPowerSeriesAt with a scalar-based formal multilinear series.

Русский

Аналитичность влечет HasFPowerSeriesAt с использованием скалярной формальной многочлена.

LaTeX

$$$\\forall {f} (h : AnalyticAt 𝕜 f x), HasFPowerSeriesAt f (FormalMultilinearSeries.ofScalars 𝕜 (fun n \\mapsto iteratedDeriv n f x / n.factorial.cast)) x$$$

Lean4

theorem iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition (hg : ContDiffWithinAt 𝕜 n g t (f x))
    (hf : ContDiffWithinAt 𝕜 n f s x) (ht : UniqueDiffOn 𝕜 t) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (hst : MapsTo f s t)
    (hi : i ≤ n) :
    iteratedDerivWithin i (g ∘ f) s x =
      ∑ c : OrderedFinpartition i,
        iteratedFDerivWithin 𝕜 c.length g t (f x) fun j ↦ iteratedDerivWithin (c.partSize j) f s x :=
  by
  simp only [iteratedDerivWithin, iteratedFDerivWithin_comp hg hf ht hs hx hst hi]
  simp [FormalMultilinearSeries.taylorComp, ftaylorSeriesWithin, OrderedFinpartition.applyOrderedFinpartition_apply,
    comp_def]

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