English
A special case: the derivative D_y f(y) considered as a linear map is C^m when f is C^n; coordinate changes are used to move from x₀ to x.
Русский
Особый случай: производная по y как линейный оператор гладкая C^m, если f гладкая C^n; применяется координатное преобразование.
LaTeX
$$$\forall x_0:\; M, f: M \to M',\ hf : ContMDiffAt I I' n f x_0,\ hmn : m + 1 ≤ n,\ hx : x_0 ∈ s,\ hs : UniqueMDiffOn I s \Rightarrow ContMDiffAt I 𝓘(𝕜, E \toL[𝕜] E') m (inTangentCoordinates I I' id f (mfderivWithin I I' f s) x_0) x_0$$$
Lean4
/-- The function that sends `x` to the `y`-derivative of `f (x, y)` at `g (x)` 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₀, g(x₀))` for `n ≥ m + 1` and `g` is `C^m` at `x₀`.
We have to insert a coordinate change from `x₀` to `x` to make the derivative sensible.
This result is used to show that maps into the 1-jet bundle and cotangent bundle are `C^n`.
`ContMDiffAt.mfderiv_const` is a special case of this.
-/
protected theorem mfderiv {x₀ : N} (f : N → M → M') (g : N → M)
(hf : ContMDiffAt (J.prod I) I' n (Function.uncurry f) (x₀, g x₀)) (hg : ContMDiffAt J I m g x₀) (hmn : m + 1 ≤ n) :
ContMDiffAt J 𝓘(𝕜, E →L[𝕜] E') m
(inTangentCoordinates I I' g (fun x ↦ f x (g x)) (fun x ↦ mfderiv I I' (f x) (g x)) x₀) x₀ :=
by
rw [← contMDiffWithinAt_univ] at hf hg ⊢
rw [← univ_prod_univ] at hf
simp_rw [← mfderivWithin_univ]
exact ContMDiffWithinAt.mfderivWithin hf hg (mem_univ _) (mapsTo_univ _ _) hmn uniqueMDiffOn_univ
