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} : MDiffAt[s] f x₀ ↔ (MDiffAt[s] fun (x : M) => (f x).proj) x₀ ∧ (MDiffAt[s] 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 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} : MDiffAt f x₀ ↔ (MDiffAt fun (x : M) => (f x).proj) x₀ ∧ (MDiffAt 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} : MDiffAt[u] (T% s) b₀ ↔ (MDiffAt[u] fun (b : B) => (↑(trivializationAt F E b₀) ⟨b, 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 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} : MDiffAt (T% s) b₀ ↔ (MDiffAt fun (b : B) => (↑(trivializationAt F E b₀) ⟨b, 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} : MDiffAt 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} : MDiffAt[s] TotalSpace.proj 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} : MDiffAt (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} : MDiffAt[t] (zeroSection F E) 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' : Bundle.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) => ↑(Bundle.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' : Bundle.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) => ↑(Bundle.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' : Bundle.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) : (MDiffAt fun (b : B) => ↑(Bundle.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' : Bundle.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 : MDiffAt[s] f x) (he : f x ∈ e.baseSet) (he' : f x ∈ e'.baseSet) : (MDiffAt[s] fun (y : M) => ↑(Bundle.Trivialization.coordChangeL 𝕜 e e' (f y))) 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' : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] {f : M → B} {x : M} (hf : MDiffAt f x) (he : f x ∈ e.baseSet) (he' : f x ∈ e'.baseSet) : (MDiffAt fun (y : M) => ↑(Bundle.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' : Bundle.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) => ↑(Bundle.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' : Bundle.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) => ↑(Bundle.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' : Bundle.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 : MDiffAt[s] f x) (hg : MDiffAt[s] g x) (he : f x ∈ e.baseSet) (he' : f x ∈ e'.baseSet) : (MDiffAt[s] fun (y : M) => e.coordChange e' (f y) (g y)) 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' : Bundle.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 : MDiffAt f x) (hg : MDiffAt g x) (he : f x ∈ e.baseSet) (he' : f x ∈ e'.baseSet) : (MDiffAt 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' : Bundle.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' : Bundle.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 : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {e' : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e'] {f : M → Bundle.TotalSpace F E} {s : Set M} {x₀ : M} (hf : MDiffAt[s] (Bundle.TotalSpace.proj ∘ f) x₀) (he'f : (MDiffAt[s] fun (x : M) => (↑e (f x)).2) x₀) (he : f x₀ ∈ e.source) (he' : f x₀ ∈ e'.source) : (MDiffAt[s] fun (x : M) => (↑e' (f x)).2) x₀

theorem Bundle.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 (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 TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {f : M → TotalSpace F E} {s : Set M} {x₀ : M} (hex₀ : f x₀ ∈ e.source) (he'x₀ : f x₀ ∈ e'.source) (hf : MDiffAt[s] (TotalSpace.proj ∘ f) x₀) : (MDiffAt[s] fun (x : M) => (↑e (f x)).2) x₀ ↔ (MDiffAt[s] fun (x : M) => (↑e' (f x)).2) x₀

theorem Bundle.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 (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 TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {f : M → TotalSpace F E} {x₀ : M} (he : f x₀ ∈ e.source) (he' : f x₀ ∈ e'.source) (hf : (MDiffAt fun (x : M) => (f x).proj) x₀) : (MDiffAt fun (x : M) => (↑e (f x)).2) x₀ ↔ (MDiffAt fun (x : M) => (↑e' (f x)).2) x₀

theorem Bundle.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 (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 TotalSpace.proj) [MemTrivializationAtlas e] (f : M → TotalSpace F E) {s : Set M} {x₀ : M} (he : f x₀ ∈ e.source) : MDiffAt[s] f x₀ ↔ (MDiffAt[s] fun (x : M) => (f x).proj) x₀ ∧ (MDiffAt[s] 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 within a set.

theorem Bundle.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 (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 TotalSpace.proj) [MemTrivializationAtlas e] (f : M → TotalSpace F E) {x₀ : M} (he : f x₀ ∈ e.source) : MDiffAt f x₀ ↔ (MDiffAt fun (x : M) => (f x).proj) x₀ ∧ (MDiffAt 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 Bundle.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 (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 TotalSpace.proj) [MemTrivializationAtlas e] (s : (b : B) → E b) {u : Set B} {b₀ : B} (hex₀ : b₀ ∈ e.baseSet) : MDiffAt[u] (T% s) b₀ ↔ (MDiffAt[u] fun (x : B) => (↑e ⟨x, s x⟩).2) b₀

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

theorem Bundle.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 (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 TotalSpace.proj) [MemTrivializationAtlas e] (s : (b : B) → E b) {b₀ : B} (hex₀ : b₀ ∈ e.baseSet) : MDiffAt (T% s) b₀ ↔ (MDiffAt fun (x : B) => (↑e ⟨x, s x⟩).2) b₀

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

theorem Bundle.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 (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 TotalSpace.proj) [MemTrivializationAtlas e] (ha : IsOpen a) (ha' : a ⊆ e.baseSet) : MDifferentiableOn IB (IB.prod (modelWithCornersSelf 𝕜 F)) (fun (x : B) => ⟨x, s x⟩) a ↔ MDifferentiableOn IB (modelWithCornersSelf 𝕜 F) (fun (x : B) => (↑e ⟨x, s x⟩).2) a

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

theorem Bundle.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 (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 TotalSpace.proj) [MemTrivializationAtlas e] : MDifferentiableOn IB (IB.prod (modelWithCornersSelf 𝕜 F)) (fun (x : B) => ⟨x, s x⟩) e.baseSet ↔ MDifferentiableOn IB (modelWithCornersSelf 𝕜 F) (fun (x : B) => (↑e ⟨x, s x⟩).2) e.baseSet

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

theorem Bundle.Trivialization.Bundle.Trivialization.mdifferentiable {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_12} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_13} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {F : Type u_14} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {M : Type u_15} [TopologicalSpace M] [ChartedSpace H M] (Z : M → Type u_16) [TopologicalSpace (TotalSpace F Z)] [(b : M) → TopologicalSpace (Z b)] [FiberBundle F Z] [(b : M) → AddCommMonoid (Z b)] [(b : M) → Module 𝕜 (Z b)] [VectorBundle 𝕜 F Z] [ContMDiffVectorBundle 1 F Z I] (e : Trivialization F TotalSpace.proj) [MemTrivializationAtlas e] : OpenPartialHomeomorph.MDifferentiable (I.prod (modelWithCornersSelf 𝕜 F)) (I.prod (modelWithCornersSelf 𝕜 F)) e.toOpenPartialHomeomorph

theorem mdifferentiableWithinAt_add_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {s t : (x : B) → E x} {u : Set B} {x₀ : B} (hs : MDiffAt[u] (T% s) x₀) (ht : MDiffAt[u] (T% t) x₀) : (MDiffAt[u] fun (x : B) => ⟨x, (s + t) x⟩) x₀

theorem mdifferentiableAt_add_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {s t : (x : B) → E x} {x₀ : B} (hs : MDiffAt (T% s) x₀) (ht : MDiffAt (T% t) x₀) : (MDiffAt fun (x : B) => ⟨x, (s + t) x⟩) x₀

theorem mdifferentiableOn_add_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {s t : (x : B) → E x} {u : Set B} (hs : MDifferentiableOn I (I.prod (modelWithCornersSelf 𝕜 F)) (fun (x : B) => ⟨x, s x⟩) u) (ht : MDifferentiableOn I (I.prod (modelWithCornersSelf 𝕜 F)) (fun (x : B) => ⟨x, t x⟩) u) : MDifferentiableOn I (I.prod (modelWithCornersSelf 𝕜 F)) (fun (x : B) => ⟨x, (s + t) x⟩) u

theorem mdifferentiable_add_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {s t : (x : B) → E x} (hs : MDifferentiable I (I.prod (modelWithCornersSelf 𝕜 F)) fun (x : B) => ⟨x, s x⟩) (ht : MDifferentiable I (I.prod (modelWithCornersSelf 𝕜 F)) fun (x : B) => ⟨x, t x⟩) : MDifferentiable I (I.prod (modelWithCornersSelf 𝕜 F)) fun (x : B) => ⟨x, (s + t) x⟩

theorem mdifferentiableWithinAt_neg_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {s : (x : B) → E x} {u : Set B} {x₀ : B} (hs : MDiffAt[u] (T% s) x₀) : (MDiffAt[u] fun (x : B) => ⟨x, (-s) x⟩) x₀

theorem mdifferentiableAt_neg_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {s : (x : B) → E x} {x₀ : B} (hs : MDiffAt (T% s) x₀) : (MDiffAt fun (x : B) => ⟨x, (-s) x⟩) x₀

theorem mdifferentiableOn_neg_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {s : (x : B) → E x} {u : Set B} (hs : MDifferentiableOn I (I.prod (modelWithCornersSelf 𝕜 F)) (fun (x : B) => ⟨x, s x⟩) u) : MDifferentiableOn I (I.prod (modelWithCornersSelf 𝕜 F)) (fun (x : B) => ⟨x, (-s) x⟩) u

theorem mdifferentiable_neg_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {s : (x : B) → E x} (hs : MDifferentiable I (I.prod (modelWithCornersSelf 𝕜 F)) fun (x : B) => ⟨x, s x⟩) : MDifferentiable I (I.prod (modelWithCornersSelf 𝕜 F)) fun (x : B) => ⟨x, (-s) x⟩

theorem mdifferentiableWithinAt_sub_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {s t : (x : B) → E x} {u : Set B} {x₀ : B} (hs : MDiffAt[u] (T% s) x₀) (ht : MDiffAt[u] (T% t) x₀) : (MDiffAt[u] fun (x : B) => ⟨x, (s - t) x⟩) x₀

theorem mdifferentiableAt_sub_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {s t : (x : B) → E x} {x₀ : B} (hs : MDiffAt (T% s) x₀) (ht : MDiffAt (T% t) x₀) : (MDiffAt fun (x : B) => ⟨x, (s - t) x⟩) x₀

theorem mDifferentiableOn_sub_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {s t : (x : B) → E x} {u : Set B} (hs : MDifferentiableOn I (I.prod (modelWithCornersSelf 𝕜 F)) (fun (x : B) => ⟨x, s x⟩) u) (ht : MDifferentiableOn I (I.prod (modelWithCornersSelf 𝕜 F)) (fun (x : B) => ⟨x, t x⟩) u) : MDifferentiableOn I (I.prod (modelWithCornersSelf 𝕜 F)) (fun (x : B) => ⟨x, (s - t) x⟩) u

theorem mdifferentiable_sub_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {s t : (x : B) → E x} (hs : MDifferentiable I (I.prod (modelWithCornersSelf 𝕜 F)) fun (x : B) => ⟨x, s x⟩) (ht : MDifferentiable I (I.prod (modelWithCornersSelf 𝕜 F)) fun (x : B) => ⟨x, t x⟩) : MDifferentiable I (I.prod (modelWithCornersSelf 𝕜 F)) fun (x : B) => ⟨x, (s - t) x⟩

theorem MDifferentiableWithinAt.smul_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {f : B → 𝕜} {s : (x : B) → E x} {u : Set B} {x₀ : B} (hf : MDiffAt[u] f x₀) (hs : MDiffAt[u] (T% s) x₀) : (MDiffAt[u] fun (x : B) => ⟨x, (f • s) x⟩) x₀

theorem MDifferentiableAt.smul_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {f : B → 𝕜} {s : (x : B) → E x} {x₀ : B} (hf : MDiffAt f x₀) (hs : MDiffAt (T% s) x₀) : (MDiffAt fun (x : B) => ⟨x, (f • s) x⟩) x₀

theorem MDifferentiableOn.smul_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {f : B → 𝕜} {s : (x : B) → E x} {u : Set B} (hf : MDifferentiableOn I (modelWithCornersSelf 𝕜 𝕜) f u) (hs : MDifferentiableOn I (I.prod (modelWithCornersSelf 𝕜 F)) (fun (x : B) => ⟨x, s x⟩) u) : MDifferentiableOn I (I.prod (modelWithCornersSelf 𝕜 F)) (fun (x : B) => ⟨x, (f • s) x⟩) u

theorem mdifferentiable_smul_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {f : B → 𝕜} {s : (x : B) → E x} (hf : MDifferentiable I (modelWithCornersSelf 𝕜 𝕜) f) (hs : MDifferentiable I (I.prod (modelWithCornersSelf 𝕜 F)) fun (x : B) => ⟨x, s x⟩) : MDifferentiable I (I.prod (modelWithCornersSelf 𝕜 F)) fun (x : B) => ⟨x, (f • s) x⟩

theorem mdifferentiableWithinAt_smul_const_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {a : 𝕜} {s : (x : B) → E x} {u : Set B} {x₀ : B} (hs : MDiffAt[u] (T% s) x₀) : (MDiffAt[u] fun (x : B) => ⟨x, (a • s) x⟩) x₀

theorem MDifferentiableAt.smul_const_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {a : 𝕜} {s : (x : B) → E x} {x₀ : B} (hs : MDiffAt (T% s) x₀) : (MDiffAt fun (x : B) => ⟨x, (a • s) x⟩) x₀

theorem MDifferentiableOn.smul_const_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {a : 𝕜} {s : (x : B) → E x} {u : Set B} (hs : MDifferentiableOn I (I.prod (modelWithCornersSelf 𝕜 F)) (fun (x : B) => ⟨x, s x⟩) u) : MDifferentiableOn I (I.prod (modelWithCornersSelf 𝕜 F)) (fun (x : B) => ⟨x, (a • s) x⟩) u

theorem mdifferentiable_smul_const_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {a : 𝕜} {s : (x : B) → E x} (hs : MDifferentiable I (I.prod (modelWithCornersSelf 𝕜 F)) fun (x : B) => ⟨x, s x⟩) : MDifferentiable I (I.prod (modelWithCornersSelf 𝕜 F)) fun (x : B) => ⟨x, (a • s) x⟩

theorem MDifferentiableWithinAt.sum_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {u : Set B} {x₀ : B} {ι : Type u_9} {s : Finset ι} {t : ι → (x : B) → E x} (hs : ∀ (i : ι), MDiffAt[u] (T% t) x₀) : (MDiffAt[u] fun (x : B) => ⟨x, ∑ i ∈ s, t i x⟩) x₀

theorem MDifferentiableAt.sum_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {ι : Type u_9} {s : Finset ι} {t : ι → (x : B) → E x} {x₀ : B} (hs : ∀ (i : ι), MDiffAt (T% t) x₀) : (MDiffAt fun (x : B) => ⟨x, ∑ i ∈ s, t i x⟩) x₀

theorem MDifferentiableOn.sum_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {u : Set B} {ι : Type u_9} {s : Finset ι} {t : ι → (x : B) → E x} (hs : ∀ (i : ι), MDifferentiableOn I (I.prod (modelWithCornersSelf 𝕜 F)) (fun (x : B) => ⟨x, t i x⟩) u) : MDifferentiableOn I (I.prod (modelWithCornersSelf 𝕜 F)) (fun (x : B) => ⟨x, ∑ i ∈ s, t i x⟩) u

theorem MDifferentiable.sum_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {ι : Type u_9} {s : Finset ι} {t : ι → (x : B) → E x} (hs : ∀ (i : ι), MDifferentiable I (I.prod (modelWithCornersSelf 𝕜 F)) fun (x : B) => ⟨x, t i x⟩) : MDifferentiable I (I.prod (modelWithCornersSelf 𝕜 F)) fun (x : B) => ⟨x, ∑ i ∈ s, t i x⟩

theorem MDifferentiableOn.smul_section_of_tsupport {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {u : Set B} {s : (x : B) → E x} {ψ : B → 𝕜} (hψ : MDifferentiableOn I (modelWithCornersSelf 𝕜 𝕜) ψ u) (ht : IsOpen u) (ht' : tsupport ψ ⊆ u) (hs : MDifferentiableOn I (I.prod (modelWithCornersSelf 𝕜 F)) (fun (x : B) => ⟨x, s x⟩) u) : MDifferentiable I (I.prod (modelWithCornersSelf 𝕜 F)) fun (x : B) => ⟨x, (ψ • s) x⟩

The scalar product ψ • s of a differentiable function ψ : M → 𝕜 and a section s of a vector bundle V → M is differentiable once s is differentiable on an open set containing tsupport ψ.

See ContMDiffOn.smul_section_of_tsupport for the analogous result about C^n sections.

theorem MDifferentiableWithinAt.sum_section_of_locallyFinite {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {u : Set B} {x₀ : B} {ι : Type u_9} {t : ι → (x : B) → E x} (ht : LocallyFinite fun (i : ι) => {x : B | t i x ≠ 0}) (ht' : ∀ (i : ι), MDiffAt[u] (T% t) x₀) : (MDiffAt[u] fun (x : B) => ⟨x, ∑' (i : ι), t i x⟩) x₀

The sum of a locally finite collection of sections is differentiable if each section is. Version at a point within a set.

theorem MDifferentiableAt.sum_section_of_locallyFinite {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {x₀ : B} {ι : Type u_9} {t : ι → (x : B) → E x} (ht : LocallyFinite fun (i : ι) => {x : B | t i x ≠ 0}) (ht' : ∀ (i : ι), MDiffAt (T% t) x₀) : (MDiffAt fun (x : B) => ⟨x, ∑' (i : ι), t i x⟩) x₀

The sum of a locally finite collection of sections is differentiable at x if each section is.

theorem MDifferentiableOn.sum_section_of_locallyFinite {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {u : Set B} {ι : Type u_9} {t : ι → (x : B) → E x} (ht : LocallyFinite fun (i : ι) => {x : B | t i x ≠ 0}) (ht' : ∀ (i : ι), MDifferentiableOn I (I.prod (modelWithCornersSelf 𝕜 F)) (fun (x : B) => ⟨x, t i x⟩) u) : MDifferentiableOn I (I.prod (modelWithCornersSelf 𝕜 F)) (fun (x : B) => ⟨x, ∑' (i : ι), t i x⟩) u

The sum of a locally finite collection of sections is differentiable on a set u if each section is.

theorem MDifferentiable.sum_section_of_locallyFinite {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {ι : Type u_9} {t : ι → (x : B) → E x} (ht : LocallyFinite fun (i : ι) => {x : B | t i x ≠ 0}) (ht' : ∀ (i : ι), MDifferentiable I (I.prod (modelWithCornersSelf 𝕜 F)) fun (x : B) => ⟨x, t i x⟩) : MDifferentiable I (I.prod (modelWithCornersSelf 𝕜 F)) fun (x : B) => ⟨x, ∑' (i : ι), t i x⟩

The sum of a locally finite collection of sections is differentiable if each section is.

theorem MDifferentiableWithinAt.finsum_section_of_locallyFinite {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {u : Set B} {x₀ : B} {ι : Type u_9} {t : ι → (x : B) → E x} (ht : LocallyFinite fun (i : ι) => {x : B | t i x ≠ 0}) (ht' : ∀ (i : ι), MDiffAt[u] (T% t) x₀) : (MDiffAt[u] fun (x : B) => ⟨x, ∑ᶠ (i : ι), t i x⟩) x₀

theorem MDifferentiableAt.finsum_section_of_locallyFinite {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {x₀ : B} {ι : Type u_9} {t : ι → (x : B) → E x} (ht : LocallyFinite fun (i : ι) => {x : B | t i x ≠ 0}) (ht' : ∀ (i : ι), MDiffAt (T% t) x₀) : (MDiffAt fun (x : B) => ⟨x, ∑ᶠ (i : ι), t i x⟩) x₀

theorem MDifferentiableOn.finsum_section_of_locallyFinite {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {u : Set B} {ι : Type u_9} {t : ι → (x : B) → E x} (ht : LocallyFinite fun (i : ι) => {x : B | t i x ≠ 0}) (ht' : ∀ (i : ι), MDifferentiableOn I (I.prod (modelWithCornersSelf 𝕜 F)) (fun (x : B) => ⟨x, t i x⟩) u) : MDifferentiableOn I (I.prod (modelWithCornersSelf 𝕜 F)) (fun (x : B) => ⟨x, ∑ᶠ (i : ι), t i x⟩) u

theorem MDifferentiable.finsum_section_of_locallyFinite {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [FiberBundle F E] [(x : B) → AddCommGroup (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {ι : Type u_9} {t : ι → (x : B) → E x} (ht : LocallyFinite fun (i : ι) => {x : B | t i x ≠ 0}) (ht' : ∀ (i : ι), MDifferentiable I (I.prod (modelWithCornersSelf 𝕜 F)) fun (x : B) => ⟨x, t i x⟩) : MDifferentiable I (I.prod (modelWithCornersSelf 𝕜 F)) fun (x : B) => ⟨x, ∑ᶠ (i : ι), t i x⟩

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ϕ : (MDiffAt[s] fun (m : M) => ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀) (hv : (MDiffAt[s] fun (m : M) => ⟨b₁ m, v m⟩) m₀) (hb₂ : MDiffAt[s] b₂ m₀) : (MDiffAt[s] fun (m : M) => ⟨b₂ m, (ϕ 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 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ϕ : (MDiffAt fun (m : M) => ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀) (hv : (MDiffAt fun (m : M) => ⟨b₁ m, v m⟩) m₀) (hb₂ : MDiffAt b₂ m₀) : (MDiffAt fun (m : M) => ⟨b₂ m, (ϕ 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.

theorem FiberBundle.exists_contMDiffOn_extend {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (F : Type u_5) [NormedAddCommGroup F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [NormedSpace 𝕜 F] {k : WithTop ℕ∞} [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] [ContMDiffVectorBundle k F V I] {x₀ : M} (σ₀ : V x₀) : ∃ s ∈ nhds x₀, ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) k (fun (x' : M) => ⟨x', extend F σ₀ x'⟩) s

theorem FiberBundle.contMDiffAt_extend' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (F : Type u_5) [NormedAddCommGroup F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [NormedSpace 𝕜 F] {k : WithTop ℕ∞} {x : M} (σ₀ : V x) : ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) k (fun (x' : M) => ⟨x', extend F σ₀ x'⟩) x

theorem FiberBundle.exists_mdifferentiableOn_extend {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (F : Type u_5) [NormedAddCommGroup F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [NormedSpace 𝕜 F] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] [ContMDiffVectorBundle 1 F V I] {x₀ : M} (σ₀ : V x₀) : ∃ s ∈ nhds x₀, MDifferentiableOn I (I.prod (modelWithCornersSelf 𝕜 F)) (fun (x' : M) => ⟨x', extend F σ₀ x'⟩) s

theorem FiberBundle.mdifferentiableAt_extend {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (F : Type u_5) [NormedAddCommGroup F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [NormedSpace 𝕜 F] {x : M} (σ₀ : V x) : (MDiffAt fun (x' : M) => ⟨x', extend F σ₀ x'⟩) x