iteratedDerivWithin_comp_eq_sum_orderedFinpartition

English

A simplified two-term Faà di Bruno-like expression for second order inside sets.

Русский

Упрощённое выражение типа Фаàди Бруно для второго порядка внутри множеств.

LaTeX

$$$\\forall {g,f}{x},\\ ContDiffWithinAt 𝕜 2 g (f x) \\to ContDiffWithinAt 𝕜 2 f x \\Rightarrow \n iteratedDerivWithin 2 (g \\circ f) s x = iteratedDerivWithin 2 g (f x) * derivWithin f s x ^ 2 + derivWithin g (f x) * iteratedDerivWithin 2 f s x$$$

Lean4

theorem iteratedDerivWithin_comp_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,
        iteratedDerivWithin c.length g t (f x) * ∏ j, iteratedDerivWithin (c.partSize j) f s x :=
  by
  rw [iteratedDerivWithin_scomp_eq_sum_orderedFinpartition hg hf ht hs hx hst hi]
  simp only [smul_eq_mul, mul_comm]

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