iteratedFDerivWithin_cons — Mathlib

English

For hf, the iterated second derivative within obeys the swap symmetry with respect to v and w.

Русский

Для hf из второй производной внутри сохраняется симметрия при перестановке v и w.

LaTeX

$$$\\text{iteratedFDerivWithin 𝕜 2 f s x ![v,w]} = \\text{iteratedFDerivWithin 𝕜 2 f s x ![w,v]}$$$

Lean4

theorem iteratedFDerivWithin_cons {x v w : E} {hf : IsSymmSndFDerivWithinAt 𝕜 f s x} (hs : UniqueDiffOn 𝕜 s)
    (hx : x ∈ s) : iteratedFDerivWithin 𝕜 2 f s x ![v, w] = iteratedFDerivWithin 𝕜 2 f s x ![w, v] :=
  by
  simp_rw [isSymmSndFDerivWithinAt_iff_iteratedFDerivWithin hs hx, ContinuousMultilinearMap.ext_iff,
    ContinuousMultilinearMap.domDomCongr_apply] at hf
  convert hf ![w, v] using 2
  ext i
  fin_cases i <;> simp

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