English
Let f be defined on E and s a set with UniqueDiffOn. Then for every i, iteratedFDerivWithin 𝕜 i (-f) s x = - iteratedFDerivWithin 𝕜 i f s x.
Русский
Пусть f определена на E, а s удовлетворяет UniqueDiffOn. Тогда для каждого i выполняется: D^iWithin(-f) = - D^iWithin f.
LaTeX
$$$\text{UniqueDiffOn } 𝕜 s \to iteratedFDerivWithin 𝕜 i (-f) s x = - iteratedFDerivWithin 𝕜 i f s x$$$
Lean4
theorem iteratedFDerivWithin_neg_apply {f : E → F} (hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
iteratedFDerivWithin 𝕜 i (-f) s x = -iteratedFDerivWithin 𝕜 i f s x := by
induction i generalizing x with ext h
| zero => simp
| succ i hi =>
calc
iteratedFDerivWithin 𝕜 (i + 1) (-f) s x h =
fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (-f) s) s x (h 0) (Fin.tail h) :=
iteratedFDerivWithin_succ_apply_left _
_ = fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x (h 0) (Fin.tail h) := by
rw [fderivWithin_congr' (@hi) hx, Pi.neg_def]
_ = -(fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s) x (h 0) (Fin.tail h) := by
rw [fderivWithin_neg (hu x hx), ContinuousLinearMap.neg_apply, ContinuousMultilinearMap.neg_apply]
_ = -(iteratedFDerivWithin 𝕜 (i + 1) f s) x h := by rw [iteratedFDerivWithin_succ_apply_left]
