English
In a charted vector space, scalar multiplication is ContMDiffWithinAt: if f,g are ContMDiffWithinAt, then the product is ContMDiffWithinAt.
Русский
Векторное пространство: умножение на скаляр гладко внутри ContMDiffWithinAt.
LaTeX
$$$\forall {f : M \to 𝕜} {g : M \to V},\ ContMDiffWithinAt (I := (modelWithCornersSelf 𝕜 𝕜)) n f s x \rightarrow ContMDiffWithinAt I 𝓘(𝕜, V) n g s x \rightarrow ContMDiffWithinAt I 𝓘(𝕜, V) n (fun p => f p • g p) s x$$$
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.
Version within a set.
-/
protected theorem mfderivWithin {x₀ : N} {f : N → M → M'} {g : N → M} {t : Set N} {u : Set M}
(hf : ContMDiffWithinAt (J.prod I) I' n (Function.uncurry f) (t ×ˢ u) (x₀, g x₀))
(hg : ContMDiffWithinAt J I m g t x₀) (hx₀ : x₀ ∈ t) (hu : MapsTo g t u) (hmn : m + 1 ≤ n)
(h'u : UniqueMDiffOn I u) :
ContMDiffWithinAt J 𝓘(𝕜, E →L[𝕜] E') m
(inTangentCoordinates I I' g (fun x => f x (g x)) (fun x => mfderivWithin I I' (f x) u (g x)) x₀) t x₀ :=
by
-- first localize the result to a smaller set, to make sure everything happens in chart domains
let t' := t ∩ g ⁻¹' ((extChartAt I (g x₀)).source)
have ht't : t' ⊆ t := inter_subset_left
suffices
ContMDiffWithinAt J 𝓘(𝕜, E →L[𝕜] E') m
(inTangentCoordinates I I' g (fun x ↦ f x (g x)) (fun x ↦ mfderivWithin I I' (f x) u (g x)) x₀) t' x₀
by
apply ContMDiffWithinAt.mono_of_mem_nhdsWithin this
apply inter_mem self_mem_nhdsWithin
exact
hg.continuousWithinAt.preimage_mem_nhdsWithin
(extChartAt_source_mem_nhds (g x₀))
-- register a few basic facts that maps send suitable neighborhoods to suitable neighborhoods,
-- by continuity
have hx₀gx₀ : (x₀, g x₀) ∈ t ×ˢ u := by simp [hx₀, hu hx₀]
have h4f : ContinuousWithinAt (fun x => f x (g x)) t x₀ :=
by
change ContinuousWithinAt ((Function.uncurry f) ∘ (fun x ↦ (x, g x))) t x₀
refine ContinuousWithinAt.comp hf.continuousWithinAt ?_ (fun y hy ↦ by simp [hy, hu hy])
exact (continuousWithinAt_id.prodMk hg.continuousWithinAt)
have h4f := h4f.preimage_mem_nhdsWithin (extChartAt_source_mem_nhds (I := I') (f x₀ (g x₀)))
have h3f :=
(contMDiffWithinAt_iff_contMDiffWithinAt_nhdsWithin (by simp)).mp (hf.of_le <| (self_le_add_left 1 m).trans hmn)
simp only [hx₀gx₀, insert_eq_of_mem] at h3f
have h2f : ∀ᶠ x₂ in 𝓝[t] x₀, ContMDiffWithinAt I I' 1 (f x₂) u (g x₂) :=
by
have : MapsTo (fun x ↦ (x, g x)) t (t ×ˢ u) := fun y hy ↦ by simp [hy, hu hy]
filter_upwards [((continuousWithinAt_id.prodMk hg.continuousWithinAt) |>.tendsto_nhdsWithin this).eventually h3f,
self_mem_nhdsWithin] with x hx h'x
apply hx.comp (g x) (contMDiffWithinAt_const.prodMk contMDiffWithinAt_id)
exact fun y hy ↦ by simp [h'x, hy]
have h2g : g ⁻¹' (extChartAt I (g x₀)).source ∈ 𝓝[t] x₀ :=
hg.continuousWithinAt.preimage_mem_nhdsWithin
(extChartAt_source_mem_nhds (g x₀))
-- key point: the derivative of `f` composed with extended charts, at the point `g x` read in the
-- chart, is `C^n` in the vector space sense. This follows from `ContDiffWithinAt.fderivWithin`,
-- which is the vector space analogue of the result we are proving.
have :
ContDiffWithinAt 𝕜 m
(fun x ↦
fderivWithin 𝕜 (extChartAt I' (f x₀ (g x₀)) ∘ f ((extChartAt J x₀).symm x) ∘ (extChartAt I (g x₀)).symm)
((extChartAt I (g x₀)).target ∩ (extChartAt I (g x₀)).symm ⁻¹' u)
(extChartAt I (g x₀) (g ((extChartAt J x₀).symm x))))
((extChartAt J x₀).symm ⁻¹' t' ∩ range J) (extChartAt J x₀ x₀) :=
by
have hf' := hf.mono (prod_mono_left ht't)
have hg' := hg.mono (show t' ⊆ t from inter_subset_left)
rw [contMDiffWithinAt_iff] at hf' hg'
simp_rw [Function.comp_def, uncurry, extChartAt_prod, PartialEquiv.prod_coe_symm,
ModelWithCorners.range_prod] at hf' ⊢
apply ContDiffWithinAt.fderivWithin _ _ _ (show (m : WithTop ℕ∞) + 1 ≤ n from mod_cast hmn)
· simp [hx₀, t']
· apply inter_subset_left.trans
rw [preimage_subset_iff]
intro a ha
refine ⟨PartialEquiv.map_source _ (inter_subset_right ha :), ?_⟩
rw [mem_preimage, PartialEquiv.left_inv (extChartAt I (g x₀))]
· exact hu (inter_subset_left ha)
· exact (inter_subset_right ha :)
· have :
((fun p ↦ ((extChartAt J x₀).symm p.1, (extChartAt I (g x₀)).symm p.2)) ⁻¹' t' ×ˢ u ∩
range J ×ˢ (extChartAt I (g x₀)).target) ⊆
((fun p ↦ ((extChartAt J x₀).symm p.1, (extChartAt I (g x₀)).symm p.2)) ⁻¹' t' ×ˢ u ∩ range J ×ˢ range I) :=
by
apply inter_subset_inter_right
exact Set.prod_mono_right (extChartAt_target_subset_range (g x₀))
convert hf'.2.mono this
· ext y; simp; tauto
· simp
· exact hg'.2
·
exact
UniqueMDiffOn.uniqueDiffOn_target_inter h'u
(g x₀)
-- reformulate the previous point as `C^n` in the manifold sense (but still for a map between
-- vector spaces)
have :
ContMDiffWithinAt J 𝓘(𝕜, E →L[𝕜] E') m
(fun x =>
fderivWithin 𝕜 (extChartAt I' (f x₀ (g x₀)) ∘ f x ∘ (extChartAt I (g x₀)).symm)
((extChartAt I (g x₀)).target ∩ (extChartAt I (g x₀)).symm ⁻¹' u) (extChartAt I (g x₀) (g x)))
t' x₀ :=
by
simp_rw [contMDiffWithinAt_iff_source (x := x₀), contMDiffWithinAt_iff_contDiffWithinAt, Function.comp_def]
exact this
apply this.congr_of_eventuallyEq_of_mem _ (by simp [t', hx₀])
apply nhdsWithin_mono _ ht't
filter_upwards [h2f, h4f, h2g, self_mem_nhdsWithin] with x hx h'x h2 hxt
have h1 : g x ∈ u := hu hxt
have h3 :
UniqueMDiffWithinAt 𝓘(𝕜, E) ((extChartAt I (g x₀)).target ∩ (extChartAt I (g x₀)).symm ⁻¹' u)
((extChartAt I (g x₀)) (g x)) :=
by
apply UniqueDiffWithinAt.uniqueMDiffWithinAt
apply UniqueMDiffOn.uniqueDiffOn_target_inter h'u
refine ⟨PartialEquiv.map_source _ h2, ?_⟩
rwa [mem_preimage, PartialEquiv.left_inv _ h2]
have A :
mfderivWithin 𝓘(𝕜, E) I ((extChartAt I (g x₀)).symm) (range I) ((extChartAt I (g x₀)) (g x)) =
mfderivWithin 𝓘(𝕜, E) I ((extChartAt I (g x₀)).symm)
((extChartAt I (g x₀)).target ∩ (extChartAt I (g x₀)).symm ⁻¹' u) ((extChartAt I (g x₀)) (g x)) :=
by
apply (MDifferentiableWithinAt.mfderivWithin_mono _ h3 _).symm
· apply mdifferentiableWithinAt_extChartAt_symm
exact PartialEquiv.map_source (extChartAt I (g x₀)) h2
· exact inter_subset_left.trans (extChartAt_target_subset_range (g x₀))
rw [inTangentCoordinates_eq_mfderiv_comp, A, ← mfderivWithin_comp_of_eq, ← mfderiv_comp_mfderivWithin_of_eq]
· exact mfderivWithin_eq_fderivWithin
· exact mdifferentiableAt_extChartAt (by simpa using h'x)
· apply MDifferentiableWithinAt.comp (I' := I) (u := u) _ _ _ inter_subset_right
· convert hx.mdifferentiableWithinAt le_rfl
exact PartialEquiv.left_inv (extChartAt I (g x₀)) h2
· apply (mdifferentiableWithinAt_extChartAt_symm _).mono
· exact inter_subset_left.trans (extChartAt_target_subset_range (g x₀))
· exact PartialEquiv.map_source (extChartAt I (g x₀)) h2
· exact h3
· simp only [Function.comp_def, PartialEquiv.left_inv (extChartAt I (g x₀)) h2]
· exact hx.mdifferentiableWithinAt le_rfl
· apply (mdifferentiableWithinAt_extChartAt_symm _).mono
· exact inter_subset_left.trans (extChartAt_target_subset_range (g x₀))
· exact PartialEquiv.map_source (extChartAt I (g x₀)) h2
· exact inter_subset_right
· exact h3
· exact PartialEquiv.left_inv (extChartAt I (g x₀)) h2
· simpa using h2
· simpa using h'x
