English
The iterated derivative within is symmetric under swapping the last two arguments.
Русский
Итерационная производная внутри симметрична при смене последних двух аргументов.
LaTeX
$$$\\forall x,v,w,\\; iteratedFDerivWithin 𝕜 2 f s x ![v,w] = iteratedFDerivWithin 𝕜 2 f s x ![w,v]$$$
Lean4
theorem fderivWithin_fderivWithin_eq_of_mem_nhdsWithin (h : t ∈ 𝓝[s] x) (hf : ContDiffWithinAt 𝕜 2 f t x)
(hs : UniqueDiffOn 𝕜 s) (ht : UniqueDiffOn 𝕜 t) (hx : x ∈ s) :
fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x :=
by
have A : ∀ᶠ y in 𝓝[s] x, fderivWithin 𝕜 f s y = fderivWithin 𝕜 f t y :=
by
have : ∀ᶠ y in 𝓝[s] x, ContDiffWithinAt 𝕜 2 f t y :=
nhdsWithin_le_iff.2 h (nhdsWithin_mono _ (subset_insert x t) (hf.eventually (by simp)))
filter_upwards [self_mem_nhdsWithin, this, eventually_eventually_nhdsWithin.2 h] with y hy h'y h''y
exact fderivWithin_of_mem_nhdsWithin h''y (hs y hy) (h'y.differentiableWithinAt one_le_two)
have : fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderivWithin 𝕜 (fderivWithin 𝕜 f t) s x :=
by
apply Filter.EventuallyEq.fderivWithin_eq A
exact fderivWithin_of_mem_nhdsWithin h (hs x hx) (hf.differentiableWithinAt one_le_two)
rw [this]
apply fderivWithin_of_mem_nhdsWithin h (hs x hx)
exact (hf.fderivWithin_right (m := 1) ht le_rfl (mem_of_mem_nhdsWithin hx h)).differentiableWithinAt le_rfl
