English
One can differentiate iteratedly with respect to x on the right and obtain contDiff.
Русский
Можно по правому члену итеративно дифференцировать и получить ContDiff.
LaTeX
$$$\operatorname{ContDiffWithinAt}_{\mathbb{K}} n (\text{iteratedFDerivWithin } 𝕜 i\ f)\ s x_0$$$
Lean4
/-- `x ↦ fderivWithin 𝕜 f s x (k x)` is smooth at `x₀` within `s`. -/
theorem fderivWithin_right_apply {f : F → G} {k : F → F} {s : Set F} {x₀ : F} (hf : ContDiffWithinAt 𝕜 n f s x₀)
(hk : ContDiffWithinAt 𝕜 m k s x₀) (hs : UniqueDiffOn 𝕜 s) (hmn : m + 1 ≤ n) (hx₀s : x₀ ∈ s) :
ContDiffWithinAt 𝕜 m (fun x => fderivWithin 𝕜 f s x (k x)) s x₀ :=
ContDiffWithinAt.fderivWithin_apply
(ContDiffWithinAt.comp (x₀, x₀) hf contDiffWithinAt_snd <| prod_subset_preimage_snd s s) contDiffWithinAt_id hk hs
hmn hx₀s
(by rw [preimage_id'])
-- TODO: can we make a version of `ContDiffWithinAt.fderivWithin` for iterated derivatives?
