English
If f is C^n on a domain with unique derivatives, then the tangent map of f, considered as a map on tangent bundles, is C^m.
Русский
Если f гладко на области с уникальными производными, касательное отображение касательного отображения гладкое.
LaTeX
$$$\forall hf : ContMDiffOn I I' n f s,\ hmn : 1 ≤ n,\ hs : UniqueMDiffOn I s \Rightarrow ContMDiffOn I.tangent I'.tangent m (tangentMapWithin I I' f s) (π E(TangentSpace I)^{-1}' s)$$$
Lean4
/-- If a function is `C^n` on a domain with unique derivatives, then its bundled derivative
is `C^m` when `m+1 ≤ n`. -/
theorem contMDiffOn_tangentMapWithin (hf : ContMDiffOn I I' n f s) (hmn : m + 1 ≤ n) (hs : UniqueMDiffOn I s) :
ContMDiffOn I.tangent I'.tangent m (tangentMapWithin I I' f s) (π E(TangentSpace I) ⁻¹' s) :=
by
intro x₀ hx₀
let s' : Set (TangentBundle I M) := (π E(TangentSpace I) ⁻¹' s)
let b₁ : TangentBundle I M → M := fun p ↦ p.1
let v : Π (y : TangentBundle I M), TangentSpace I (b₁ y) := fun y ↦ y.2
have hv : ContMDiffWithinAt I.tangent I.tangent m (fun y ↦ (v y : TangentBundle I M)) s' x₀ := contMDiffWithinAt_id
let b₂ : TangentBundle I M → M' := f ∘ b₁
have hb₂ : ContMDiffWithinAt I.tangent I' m b₂ s' x₀ :=
((hf (b₁ x₀) hx₀).of_le (le_self_add.trans hmn)).comp _ (contMDiffWithinAt_proj (TangentSpace I)) (fun x h ↦ h)
let ϕ : Π (y : TangentBundle I M), TangentSpace I (b₁ y) →L[𝕜] TangentSpace I' (b₂ y) := fun y ↦
mfderivWithin I I' f s (b₁ y)
have hϕ :
ContMDiffWithinAt I.tangent 𝓘(𝕜, E →L[𝕜] E') m
(fun y ↦
ContinuousLinearMap.inCoordinates E (TangentSpace I (M := M)) E' (TangentSpace I' (M := M')) (b₁ x₀) (b₁ y)
(b₂ x₀) (b₂ y) (ϕ y))
s' x₀ :=
by
have A :
ContMDiffWithinAt I 𝓘(𝕜, E →L[𝕜] E') m
(fun y ↦
ContinuousLinearMap.inCoordinates E (TangentSpace I (M := M)) E' (TangentSpace I' (M := M')) (b₁ x₀) y (b₂ x₀)
(f y) (mfderivWithin I I' f s y))
s (b₁ x₀) :=
ContMDiffWithinAt.mfderivWithin_const (hf _ hx₀) hmn hx₀ hs
exact A.comp _ (contMDiffWithinAt_proj (TangentSpace I)) (fun x h ↦ h)
exact ContMDiffWithinAt.clm_apply_of_inCoordinates hϕ hv hb₂
