second_derivative_symmetric — Mathlib

English

Over a real or more generally IsRCLike field, the second derivative is symmetric under differentiability assumptions.

Русский

Для вещественного поля (или более общо для IsRCLike поля) вторая производная симметрична при соответствующих предположениях дифференцируемости.

LaTeX

$$$$ f''(v,w) = f''(w,v). $$$$

Lean4

/-- If a function is differentiable, and has two derivatives at `x`, then the second
derivative is symmetric. -/
theorem second_derivative_symmetric [IsRCLikeNormedField 𝕜] {f' : E → E →L[𝕜] F} {f'' : E →L[𝕜] E →L[𝕜] F} {x : E}
    (hf : ∀ y, HasFDerivAt f (f' y) y) (hx : HasFDerivAt f' f'' x) (v w : E) : f'' v w = f'' w v :=
  second_derivative_symmetric_of_eventually (Filter.Eventually.of_forall hf) hx v w

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