Differentiability of functions in vector bundles

theorem mdifferentiableWithinAt_totalSpace {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) {EM : Type u_10} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_11} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] (f : M → Bundle.TotalSpace F E) {s : Set M} {x₀ : M} : MDifferentiableWithinAt IM (IB.prod (modelWithCornersSelf 𝕜 F)) f s x₀ ↔ MDifferentiableWithinAt IM IB (fun (x : M) => (f x).proj) s x₀ ∧ MDifferentiableWithinAt IM (modelWithCornersSelf 𝕜 F) (fun (x : M) => (↑(trivializationAt F E (f x₀).proj) (f x)).2) s x₀

Characterization of differentiable functions into a smooth vector bundle.

theorem MDifferentiableWithinAt.clm_apply_of_inCoordinates {𝕜 : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {B₁ : Type u_4} {B₂ : Type u_5} {M : Type u_6} {E₁ : B₁ → Type u_7} {E₂ : B₂ → Type u_8} [NontriviallyNormedField 𝕜] [(x : B₁) → AddCommGroup (E₁ x)] [(x : B₁) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B₁) → TopologicalSpace (E₁ x)] [(x : B₂) → AddCommGroup (E₂ x)] [(x : B₂) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B₂) → TopologicalSpace (E₂ x)] {EB₁ : Type u_9} [NormedAddCommGroup EB₁] [NormedSpace 𝕜 EB₁] {HB₁ : Type u_10} [TopologicalSpace HB₁] {IB₁ : ModelWithCorners 𝕜 EB₁ HB₁} [TopologicalSpace B₁] [ChartedSpace HB₁ B₁] {EB₂ : Type u_11} [NormedAddCommGroup EB₂] [NormedSpace 𝕜 EB₂] {HB₂ : Type u_12} [TopologicalSpace HB₂] {IB₂ : ModelWithCorners 𝕜 EB₂ HB₂} [TopologicalSpace B₂] [ChartedSpace HB₂ B₂] {EM : Type u_13} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_14} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] {b₁ : M → B₁} {b₂ : M → B₂} {m₀ : M} {ϕ : (m : M) → E₁ (b₁ m) →L[𝕜] E₂ (b₂ m)} {v : (m : M) → E₁ (b₁ m)} {s : Set M} (hϕ : MDifferentiableWithinAt IM (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) (fun (m : M) => ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) s m₀) (hv : MDifferentiableWithinAt IM (IB₁.prod (modelWithCornersSelf 𝕜 F₁)) (fun (m : M) => { proj := b₁ m, snd := v m }) s m₀) (hb₂ : MDifferentiableWithinAt IM IB₂ b₂ s m₀) : MDifferentiableWithinAt IM (IB₂.prod (modelWithCornersSelf 𝕜 F₂)) (fun (m : M) => { proj := b₂ m, snd := (ϕ m) (v m) }) s m₀

Consider a smooth map v : M → E₁ to a vector bundle, over a basemap b₁ : M → B₁, and another basemap b₂ : M → B₂. Given linear maps ϕ m : E₁ (b₁ m) → E₂ (b₂ m) depending smoothly on m, one can apply ϕ m to g m, and the resulting map is smooth.

Note that the smoothness of ϕ can not be always be stated as smoothness of a map into a manifold, as the pullback bundles b₁ *ᵖ E₁ and b₂ *ᵖ E₂ only make sense when b₁ and b₂ are globally smooth, but we want to apply this lemma with only local information. Therefore, we formulate it using smoothness of ϕ read in coordinates.

Version for MDifferentiableWithinAt. We also give a version for MDifferentiableAt, but no version for MDifferentiableOn or MDifferentiable as our assumption, written in coordinates, only makes sense around a point.

theorem MDifferentiableAt.clm_apply_of_inCoordinates {𝕜 : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {B₁ : Type u_4} {B₂ : Type u_5} {M : Type u_6} {E₁ : B₁ → Type u_7} {E₂ : B₂ → Type u_8} [NontriviallyNormedField 𝕜] [(x : B₁) → AddCommGroup (E₁ x)] [(x : B₁) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B₁) → TopologicalSpace (E₁ x)] [(x : B₂) → AddCommGroup (E₂ x)] [(x : B₂) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B₂) → TopologicalSpace (E₂ x)] {EB₁ : Type u_9} [NormedAddCommGroup EB₁] [NormedSpace 𝕜 EB₁] {HB₁ : Type u_10} [TopologicalSpace HB₁] {IB₁ : ModelWithCorners 𝕜 EB₁ HB₁} [TopologicalSpace B₁] [ChartedSpace HB₁ B₁] {EB₂ : Type u_11} [NormedAddCommGroup EB₂] [NormedSpace 𝕜 EB₂] {HB₂ : Type u_12} [TopologicalSpace HB₂] {IB₂ : ModelWithCorners 𝕜 EB₂ HB₂} [TopologicalSpace B₂] [ChartedSpace HB₂ B₂] {EM : Type u_13} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_14} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] {b₁ : M → B₁} {b₂ : M → B₂} {m₀ : M} {ϕ : (m : M) → E₁ (b₁ m) →L[𝕜] E₂ (b₂ m)} {v : (m : M) → E₁ (b₁ m)} (hϕ : MDifferentiableAt IM (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) (fun (m : M) => ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀) (hv : MDifferentiableAt IM (IB₁.prod (modelWithCornersSelf 𝕜 F₁)) (fun (m : M) => { proj := b₁ m, snd := v m }) m₀) (hb₂ : MDifferentiableAt IM IB₂ b₂ m₀) : MDifferentiableAt IM (IB₂.prod (modelWithCornersSelf 𝕜 F₂)) (fun (m : M) => { proj := b₂ m, snd := (ϕ m) (v m) }) m₀

Consider a smooth map v : M → E₁ to a vector bundle, over a basemap b₁ : M → B₁, and another basemap b₂ : M → B₂. Given linear maps ϕ m : E₁ (b₁ m) → E₂ (b₂ m) depending smoothly on m, one can apply ϕ m to g m, and the resulting map is smooth.

Note that the smoothness of ϕ can not be always be stated as smoothness of a map into a manifold, as the pullback bundles b₁ *ᵖ E₁ and b₂ *ᵖ E₂ only make sense when b₁ and b₂ are globally smooth, but we want to apply this lemma with only local information. Therefore, we formulate it using smoothness of ϕ read in coordinates.

Version for MDifferentiableAt. We also give a version for MDifferentiableWithinAt, but no version for MDifferentiableOn or MDifferentiable as our assumption, written in coordinates, only makes sense around a point.