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 vector bundle. Version at a point within a set

theorem mdifferentiableAt_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) {x₀ : M} : MDifferentiableAt IM (IB.prod (modelWithCornersSelf 𝕜 F)) f x₀ ↔ MDifferentiableAt IM IB (fun (x : M) => (f x).proj) x₀ ∧ MDifferentiableAt IM (modelWithCornersSelf 𝕜 F) (fun (x : M) => (↑(trivializationAt F E (f x₀).proj) (f x)).2) x₀

Characterization of differentiable functions into a vector bundle. Version at a point

theorem mdifferentiableWithinAt_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {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) [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] (s : (b : B) → E b) {u : Set B} {b₀ : B} : MDifferentiableWithinAt IB (IB.prod (modelWithCornersSelf 𝕜 F)) (fun (b : B) => Bundle.TotalSpace.mk' F b (s b)) u b₀ ↔ MDifferentiableWithinAt IB (modelWithCornersSelf 𝕜 F) (fun (b : B) => (↑(trivializationAt F E b₀) { proj := b, snd := s b }).2) u b₀

Characterization of differentiable sections of a vector bundle at a point within a set in terms of the preferred trivialization at that point.

theorem mdifferentiableAt_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {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) [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] (s : (b : B) → E b) {b₀ : B} : MDifferentiableAt IB (IB.prod (modelWithCornersSelf 𝕜 F)) (fun (b : B) => Bundle.TotalSpace.mk' F b (s b)) b₀ ↔ MDifferentiableAt IB (modelWithCornersSelf 𝕜 F) (fun (b : B) => (↑(trivializationAt F E b₀) { proj := b, snd := s b }).2) b₀

Characterization of differentiable sections of a vector bundle at a point within a set in terms of the preferred trivialization at that point.

theorem Bundle.mdifferentiable_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (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} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] : MDifferentiable (IB.prod (modelWithCornersSelf 𝕜 F)) IB TotalSpace.proj

theorem Bundle.mdifferentiableOn_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (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} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] {s : Set (TotalSpace F E)} : MDifferentiableOn (IB.prod (modelWithCornersSelf 𝕜 F)) IB TotalSpace.proj s

theorem Bundle.mdifferentiableAt_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (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} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] {p : TotalSpace F E} : MDifferentiableAt (IB.prod (modelWithCornersSelf 𝕜 F)) IB TotalSpace.proj p

theorem Bundle.mdifferentiableWithinAt_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (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} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] {s : Set (TotalSpace F E)} {p : TotalSpace F E} : MDifferentiableWithinAt (IB.prod (modelWithCornersSelf 𝕜 F)) IB TotalSpace.proj s p

theorem Bundle.mdifferentiable_zeroSection (𝕜 : Type u_1) {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (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} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] : MDifferentiable IB (IB.prod (modelWithCornersSelf 𝕜 F)) (zeroSection F E)

theorem Bundle.mdifferentiableOn_zeroSection (𝕜 : Type u_1) {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (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} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {t : Set B} : MDifferentiableOn IB (IB.prod (modelWithCornersSelf 𝕜 F)) (zeroSection F E) t

theorem Bundle.mdifferentiableAt_zeroSection (𝕜 : Type u_1) {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (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} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {x : B} : MDifferentiableAt IB (IB.prod (modelWithCornersSelf 𝕜 F)) (zeroSection F E) x

theorem Bundle.mdifferentiableWithinAt_zeroSection (𝕜 : Type u_1) {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (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} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {t : Set B} {x : B} : MDifferentiableWithinAt IB (IB.prod (modelWithCornersSelf 𝕜 F)) (zeroSection F E) t x

theorem mdifferentiableOn_coordChangeL {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {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} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] (e e' : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] [MemTrivializationAtlas e'] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] : MDifferentiableOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) (fun (b : B) => ↑(Trivialization.coordChangeL 𝕜 e e' b)) (e.baseSet ∩ e'.baseSet)

theorem mdifferentiableOn_symm_coordChangeL {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {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} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] (e e' : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] [MemTrivializationAtlas e'] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] : MDifferentiableOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) (fun (b : B) => ↑(Trivialization.coordChangeL 𝕜 e e' b).symm) (e.baseSet ∩ e'.baseSet)

theorem mdifferentiableAt_coordChangeL {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {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} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] {x : B} (h : x ∈ e.baseSet) (h' : x ∈ e'.baseSet) : MDifferentiableAt IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) (fun (b : B) => ↑(Trivialization.coordChangeL 𝕜 e e' b)) x

theorem MDifferentiableWithinAt.coordChangeL {𝕜 : 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] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] {s : Set M} {f : M → B} {x : M} (hf : MDifferentiableWithinAt IM IB f s x) (he : f x ∈ e.baseSet) (he' : f x ∈ e'.baseSet) : MDifferentiableWithinAt IM (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) (fun (y : M) => ↑(Trivialization.coordChangeL 𝕜 e e' (f y))) s x

theorem MDifferentiableAt.coordChangeL {𝕜 : 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] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] {f : M → B} {x : M} (hf : MDifferentiableAt IM IB f x) (he : f x ∈ e.baseSet) (he' : f x ∈ e'.baseSet) : MDifferentiableAt IM (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) (fun (y : M) => ↑(Trivialization.coordChangeL 𝕜 e e' (f y))) x

theorem MDifferentiableOn.coordChangeL {𝕜 : 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] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] {s : Set M} {f : M → B} (hf : MDifferentiableOn IM IB f s) (he : Set.MapsTo f s e.baseSet) (he' : Set.MapsTo f s e'.baseSet) : MDifferentiableOn IM (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) (fun (y : M) => ↑(Trivialization.coordChangeL 𝕜 e e' (f y))) s

theorem MDifferentiable.coordChangeL {𝕜 : 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] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] {f : M → B} (hf : MDifferentiable IM IB f) (he : ∀ (x : M), f x ∈ e.baseSet) (he' : ∀ (x : M), f x ∈ e'.baseSet) : MDifferentiable IM (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) fun (y : M) => ↑(Trivialization.coordChangeL 𝕜 e e' (f y))

theorem MDifferentiableWithinAt.coordChange {𝕜 : 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] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] {s : Set M} {f : M → B} {g : M → F} {x : M} (hf : MDifferentiableWithinAt IM IB f s x) (hg : MDifferentiableWithinAt IM (modelWithCornersSelf 𝕜 F) g s x) (he : f x ∈ e.baseSet) (he' : f x ∈ e'.baseSet) : MDifferentiableWithinAt IM (modelWithCornersSelf 𝕜 F) (fun (y : M) => e.coordChange e' (f y) (g y)) s x

theorem MDifferentiableAt.coordChange {𝕜 : 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] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] {f : M → B} {g : M → F} {x : M} (hf : MDifferentiableAt IM IB f x) (hg : MDifferentiableAt IM (modelWithCornersSelf 𝕜 F) g x) (he : f x ∈ e.baseSet) (he' : f x ∈ e'.baseSet) : MDifferentiableAt IM (modelWithCornersSelf 𝕜 F) (fun (y : M) => e.coordChange e' (f y) (g y)) x

theorem MDifferentiableOn.coordChange {𝕜 : 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] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] {s : Set M} {f : M → B} {g : M → F} (hf : MDifferentiableOn IM IB f s) (hg : MDifferentiableOn IM (modelWithCornersSelf 𝕜 F) g s) (he : Set.MapsTo f s e.baseSet) (he' : Set.MapsTo f s e'.baseSet) : MDifferentiableOn IM (modelWithCornersSelf 𝕜 F) (fun (y : M) => e.coordChange e' (f y) (g y)) s

theorem MDifferentiable.coordChange {𝕜 : 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] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] {f : M → B} {g : M → F} (hf : MDifferentiable IM IB f) (hg : MDifferentiable IM (modelWithCornersSelf 𝕜 F) g) (he : ∀ (x : M), f x ∈ e.baseSet) (he' : ∀ (x : M), f x ∈ e'.baseSet) : MDifferentiable IM (modelWithCornersSelf 𝕜 F) fun (y : M) => e.coordChange e' (f y) (g y)

theorem MDifferentiableWithinAt.change_section_trivialization {𝕜 : 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] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] {e : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e'] {f : M → Bundle.TotalSpace F E} {s : Set M} {x₀ : M} (hf : MDifferentiableWithinAt IM IB (Bundle.TotalSpace.proj ∘ f) s x₀) (he'f : MDifferentiableWithinAt IM (modelWithCornersSelf 𝕜 F) (fun (x : M) => (↑e (f x)).2) s x₀) (he : f x₀ ∈ e.source) (he' : f x₀ ∈ e'.source) : MDifferentiableWithinAt IM (modelWithCornersSelf 𝕜 F) (fun (x : M) => (↑e' (f x)).2) s x₀

theorem Trivialization.mdifferentiableWithinAt_snd_comp_iff₂ {𝕜 : 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] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {f : M → Bundle.TotalSpace F E} {s : Set M} {x₀ : M} (hex₀ : f x₀ ∈ e.source) (he'x₀ : f x₀ ∈ e'.source) (hf : MDifferentiableWithinAt IM IB (Bundle.TotalSpace.proj ∘ f) s x₀) : MDifferentiableWithinAt IM (modelWithCornersSelf 𝕜 F) (fun (x : M) => (↑e (f x)).2) s x₀ ↔ MDifferentiableWithinAt IM (modelWithCornersSelf 𝕜 F) (fun (x : M) => (↑e' (f x)).2) s x₀

theorem Trivialization.mdifferentiableAt_snd_comp_iff₂ {𝕜 : 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] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {f : M → Bundle.TotalSpace F E} {x₀ : M} (he : f x₀ ∈ e.source) (he' : f x₀ ∈ e'.source) (hf : MDifferentiableAt IM IB (fun (x : M) => (f x).proj) x₀) : MDifferentiableAt IM (modelWithCornersSelf 𝕜 F) (fun (x : M) => (↑e (f x)).2) x₀ ↔ MDifferentiableAt IM (modelWithCornersSelf 𝕜 F) (fun (x : M) => (↑e' (f x)).2) x₀

theorem Trivialization.mdifferentiableWithinAt_totalSpace_iff {𝕜 : 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] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] (e : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] (f : M → Bundle.TotalSpace F E) {s : Set M} {x₀ : M} (he : f x₀ ∈ e.source) : 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) => (↑e (f x)).2) s x₀

Characterization of differentiable functions into a vector bundle in terms of any trivialization. Version at a point within at set.

theorem Trivialization.mdifferentiableAt_totalSpace_iff {𝕜 : 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] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] (e : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] (f : M → Bundle.TotalSpace F E) {x₀ : M} (he : f x₀ ∈ e.source) : MDifferentiableAt IM (IB.prod (modelWithCornersSelf 𝕜 F)) f x₀ ↔ MDifferentiableAt IM IB (fun (x : M) => (f x).proj) x₀ ∧ MDifferentiableAt IM (modelWithCornersSelf 𝕜 F) (fun (x : M) => (↑e (f x)).2) x₀

Characterization of differentiable functions into a vector bundle in terms of any trivialization. Version at a point.

theorem Trivialization.mdifferentiableWithinAt_section_iff {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {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) [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] (e : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] (s : (b : B) → E b) {u : Set B} {b₀ : B} (hex₀ : b₀ ∈ e.baseSet) : MDifferentiableWithinAt IB (IB.prod (modelWithCornersSelf 𝕜 F)) (fun (b : B) => Bundle.TotalSpace.mk' F b (s b)) u b₀ ↔ MDifferentiableWithinAt IB (modelWithCornersSelf 𝕜 F) (fun (x : B) => (↑e { proj := x, snd := s x }).2) u b₀

Characterization of differentiable sections a vector bundle in terms of any trivialization. Version at a point within at set.

theorem Trivialization.mdifferentiableAt_section_iff {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {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) [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] (e : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] (s : (b : B) → E b) {b₀ : B} (hex₀ : b₀ ∈ e.baseSet) : MDifferentiableAt IB (IB.prod (modelWithCornersSelf 𝕜 F)) (fun (b : B) => Bundle.TotalSpace.mk' F b (s b)) b₀ ↔ MDifferentiableAt IB (modelWithCornersSelf 𝕜 F) (fun (x : B) => (↑e { proj := x, snd := s x }).2) b₀

Characterization of differentiable functions into a vector bundle in terms of any trivialization. Version at a point.

theorem Trivialization.mdifferentiableOn_section_iff {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {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} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] {s : (x : B) → E x} {a : Set B} (e : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] (ha : IsOpen a) (ha' : a ⊆ e.baseSet) : MDifferentiableOn IB (IB.prod (modelWithCornersSelf 𝕜 F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) a ↔ MDifferentiableOn IB (modelWithCornersSelf 𝕜 F) (fun (x : B) => (↑e { proj := x, snd := s x }).2) a

Differentiability of a section on s can be determined using any trivialisation whose baseSet contains s.

theorem Trivialization.mdifferentiableOn_section_baseSet_iff {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {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} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] {s : (x : B) → E x} (e : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] : MDifferentiableOn IB (IB.prod (modelWithCornersSelf 𝕜 F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) e.baseSet ↔ MDifferentiableOn IB (modelWithCornersSelf 𝕜 F) (fun (x : B) => (↑e { proj := x, snd := s x }).2) e.baseSet

For any trivialization e, the differentiability of a section on e.baseSet can be determined using e.

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 differentiable 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 differentiably on m, one can apply ϕ m to g m, and the resulting map is differentiable.

Note that the differentiability of ϕ cannot be always be stated as differentiability 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 differentiability 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 differentiable 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 differentiably on m, one can apply ϕ m to g m, and the resulting map is differentiable.

Note that the differentiability of ϕ cannot be always be stated as differentiability 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 differentiability 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.