iteratedFDerivWithin_two_apply' — Mathlib

English

If f1 ≈ f in a punctured neighborhood of x, then their second iterated derivatives agree at z along vectors v,w.

Русский

Если f1 эквивалентна f в просветке вокруг x, вторые повторные производные по z и направлениям v,w совпадают.

LaTeX

$$$\operatorname{iteratedFDerivWithin}_{\mathbb{K}}^{(2)} f_{1} s z ![v,w] = fderivWithin_{\mathbb{K}} (fderivWithin_{\mathbb{K}} f s z) v w$$$

Lean4

/-- On a set of unique differentiability, the second derivative is obtained by taking the
derivative of the derivative. -/
theorem iteratedFDerivWithin_two_apply' (f : E → F) {z : E} (hs : UniqueDiffOn 𝕜 s) (hz : z ∈ s) (v w : E) :
    iteratedFDerivWithin 𝕜 2 f s z ![v, w] = fderivWithin 𝕜 (fderivWithin 𝕜 f s) s z v w :=
  iteratedFDerivWithin_two_apply f hs hz _

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