isSymmSndFDerivAt_of_omega — Mathlib

English

If a function is analytic at a point, then its second derivative is symmetric at that point.

Русский

Если функция аналитична в точке, её вторая производная симметрична в этой точке.

LaTeX

$$$\\text{ContDiffAt}_{\\mathbb{K}}(\\omega,f,x) \\Rightarrow \\text{IsSymmSndFDerivAt}_{\\mathbb{K}}(f,x)$$$

Lean4

/-- If a function is analytic at a point, then its second derivative is symmetric. -/
theorem isSymmSndFDerivAt_of_omega (hf : ContDiffAt 𝕜 ω f x) : IsSymmSndFDerivAt 𝕜 f x :=
  by
  simp only [← isSymmSndFDerivWithinAt_univ, ← contDiffWithinAt_univ] at hf ⊢
  exact hf.isSymmSndFDerivWithinAt_of_omega uniqueDiffOn_univ (mem_univ _)

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