English
The derivative along a fixed map is C^m when the base map is C^n: mfderivWithin_const gives a C^m derivative with respect to x in a fixed x₀, using a tangent coordinate change.
Русский
Производная по фиксированному отображению имеет гладкость C^m, когда базовое отображение C^n: mfderivWithin_const.
LaTeX
$$$\forall x_0\ f : M \to M',\ ContMDiffWithinAt I I' n f s x_0 \rightarrow m + 1 ≤ n \rightarrow x_0 ∈ s \rightarrow UniqueMDiffOn I s \rightarrow ContMDiffWithinAt I 𝓘(𝕜, E \toL[𝕜] E') m (inTangentCoordinates I I' id f (mfderivWithin I I' f s) x_0) s x_0$$$
Lean4
/-- The derivative `D_yf(y)` is `C^m` at `x₀`, where the derivative is taken as a continuous
linear map. We have to assume that `f` is `C^n` at `x₀` for some `n ≥ m + 1`.
We have to insert a coordinate change from `x₀` to `x` to make the derivative sensible.
This is a special case of `ContMDiffWithinAt.mfderivWithin` where `f` does not contain any
parameters and `g = id`.
-/
theorem mfderivWithin_const {x₀ : M} {f : M → M'} (hf : ContMDiffWithinAt I I' n f s x₀) (hmn : m + 1 ≤ n) (hx : x₀ ∈ s)
(hs : UniqueMDiffOn I s) :
ContMDiffWithinAt I 𝓘(𝕜, E →L[𝕜] E') m (inTangentCoordinates I I' id f (mfderivWithin I I' f s) x₀) s x₀ :=
by
have : ContMDiffWithinAt (I.prod I) I' n (fun x : M × M => f x.2) (s ×ˢ s) (x₀, x₀) :=
ContMDiffWithinAt.comp (x₀, x₀) hf contMDiffWithinAt_snd mapsTo_snd_prod
exact this.mfderivWithin contMDiffWithinAt_id hx (mapsTo_id _) hmn hs
