English
The y-derivative of f(x,y) at g(x) applied to g₂(x) is C^n at x₀, with appropriate smoothness assumptions on f and g; a coordinate change is inserted to align bases.
Русский
Производная по y функции f(x,y) в точке g(x) примененная к g₂(x) гладко зависит от x в точке x₀ при заданных условиях на гладкость f и g и координатном преобразовании.
LaTeX
$$$\forall x_0:\ N' \to M',\ f:\ N \to M \to M',\ g:\ N \to M,\ g_1 : N' \to N,\ g_2 : N' \to E,\ hf : ContMDiffAt (J.prod I) I' n (Function.uncurry f) (g_1 x_0, g (g_1 x_0)) (hf),\ hg : ContMDiffAt J I m g (g_1 x_0) \rightarrow ContMDiffAt J' J m g_1 x_0 \rightarrow ContMDiffAt J' 𝓘(𝕜, E) m g_2 x_0 \rightarrow m + 1 ≤ n \rightarrow ContMDiffAt J' 𝓘(𝕜, E') m (fun x => inTangentCoordinates I I' g (fun x => f x (g x)) (fun x => mfderivWithin I I' (f x) u (g x)) (g_1 x_0) (g_1 x) (g_2 x)) x_0$$$
Lean4
/-- The function that sends `x` to the `y`-derivative of `f(x,y)` at `g(x)` applied to `g₂(x)` is
`C^n` at `x₀`, where the derivative is taken as a continuous linear map.
We have to assume that `f` is `C^(n+1)` at `(x₀, g(x₀))` and `g` is `C^n` at `x₀`.
We have to insert a coordinate change from `x₀` to `g₁(x)` to make the derivative sensible.
This is similar to `ContMDiffWithinAt.mfderivWithin`, but where the continuous linear map is
applied to a (variable) vector.
-/
theorem mfderivWithin_apply {x₀ : N'} {f : N → M → M'} {g : N → M} {g₁ : N' → N} {g₂ : N' → E} {t : Set N} {u : Set M}
{v : Set N'} (hf : ContMDiffWithinAt (J.prod I) I' n (Function.uncurry f) (t ×ˢ u) (g₁ x₀, g (g₁ x₀)))
(hg : ContMDiffWithinAt J I m g t (g₁ x₀)) (hg₁ : ContMDiffWithinAt J' J m g₁ v x₀)
(hg₂ : ContMDiffWithinAt J' 𝓘(𝕜, E) m g₂ v x₀) (hmn : m + 1 ≤ n) (h'g₁ : MapsTo g₁ v t) (hg₁x₀ : g₁ x₀ ∈ t)
(h'g : MapsTo g t u) (hu : UniqueMDiffOn I u) :
ContMDiffWithinAt J' 𝓘(𝕜, E') m
(fun x =>
(inTangentCoordinates I I' g (fun x => f x (g x)) (fun x => mfderivWithin I I' (f x) u (g x)) (g₁ x₀) (g₁ x))
(g₂ x))
v x₀ :=
((hf.mfderivWithin hg hg₁x₀ h'g hmn hu).comp_of_eq hg₁ h'g₁ rfl).clm_apply hg₂
