isSymmSndFDerivWithinAt_iff_iteratedFDerivWithin

English

An IsSymmSndFDerivWithinAt condition is equivalent to an equality involving iteratedFDerivWithin.

Русский

Условие IsSymmSndFDerivWithinAt равноценно равенству, связанному с iteratedFDerivWithin.

LaTeX

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

Lean4

theorem isSymmSndFDerivWithinAt_iff_iteratedFDerivWithin (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
    IsSymmSndFDerivWithinAt 𝕜 f s x ↔
      (iteratedFDerivWithin 𝕜 2 f s x).domDomCongr Fin.revPerm = iteratedFDerivWithin 𝕜 2 f s x :=
  by
  simp_rw [IsSymmSndFDerivWithinAt, ContinuousMultilinearMap.ext_iff, Fin.forall_fin_succ_pi, Fin.forall_fin_zero_pi]
  simp [iteratedFDerivWithin_two_apply f hs hx, eq_comm]

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