isSymmSndFDerivAt_iff_iteratedFDeriv

English

Equivalence between IsSymmSndFDerivWithinAt and a symmetry condition on iteratedFDerivWithin.

Русский

Эквиваленция между IsSymmSndFDerivWithinAt и симметричностью на iteratedFDerivWithin.

LaTeX

$$$IsSymmSndFDerivWithinAt 𝕜 f s x \\iff (iteratedFDerivWithin 𝕜 2 f s x).domDomCongr Fin.revPerm = iteratedFDerivWithin 𝕜 2 f s x$$$

Lean4

theorem isSymmSndFDerivAt_iff_iteratedFDeriv :
    IsSymmSndFDerivAt 𝕜 f x ↔ (iteratedFDeriv 𝕜 2 f x).domDomCongr Fin.revPerm = iteratedFDeriv 𝕜 2 f x :=
  by
  simp only [← isSymmSndFDerivWithinAt_univ, ← iteratedFDerivWithin_univ]
  exact isSymmSndFDerivWithinAt_iff_iteratedFDerivWithin uniqueDiffOn_univ (mem_univ _)

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