English
Generalized result for iterated derivatives with right-linear structure.
Русский
Обобщённый результат для итерационных производных с правой линейной структураой.
LaTeX
$$$\operatorname{ContDiffWithinAt}_{\mathbb{K}} n (\text{iteratedFDerivWithin } 𝕜 i\ f)\ s x_0$$$
Lean4
theorem iteratedFDerivWithin_right {i : ℕ} (hf : ContDiffWithinAt 𝕜 n f s x₀) (hs : UniqueDiffOn 𝕜 s) (hmn : m + i ≤ n)
(hx₀s : x₀ ∈ s) : ContDiffWithinAt 𝕜 m (iteratedFDerivWithin 𝕜 i f s) s x₀ := by
induction i generalizing m with
| zero =>
simp only [CharP.cast_eq_zero, add_zero] at hmn
exact (hf.of_le hmn).continuousLinearMap_comp ((continuousMultilinearCurryFin0 𝕜 E F).symm : _ →L[𝕜] E [×0]→L[𝕜] F)
| succ i hi =>
rw [Nat.cast_succ, add_comm _ 1, ← add_assoc] at hmn
exact
((hi hmn).fderivWithin_right hs le_rfl hx₀s).continuousLinearMap_comp
((continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (i + 1) ↦ E) F).symm : _ →L[𝕜] E [×(i + 1)]→L[𝕜] F)
