fst' — Mathlib

English

The iterated derivative of a composition equals the Taylor composition of the two Taylor series at the appropriate order.

Русский

Производная до порядка i композиции равна композиции ряда Тейлора каждого из компонентов.

LaTeX

$$$\forall i,\; \operatorname{iteratedFDeriv} 𝕜 i (g \circ f) x = (\ftaylorSeries 𝕜 g (f x)).taylorComp (\ftaylorSeries 𝕜 f x) i$$$

Lean4

/-- Precomposing `f` with `Prod.fst` is `C^n` at `(x, y)` -/
theorem fst' {f : E → G} {x : E} {y : F} (hf : ContDiffAt 𝕜 n f x) : ContDiffAt 𝕜 n (fun x : E × F => f x.1) (x, y) :=
  ContDiffAt.comp (x, y) hf contDiffAt_fst

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