Add some helpers in Hom.lean, address TODOs in GramSchmidtOrtho.lean

Mathlib/Geometry/Manifold/VectorBundle/GramSchmidtOrtho.lean

@@ -271,14 +271,11 @@ end VectorBundle
 /-! The Gram-Schmidt process preserves continuity of sections -/
 section continuity
 
--- TODO: need continuity analogues of ContMDiff.{smul_section,sub_section}
-
 section helper
 
 variable {s t : (x : B) → E x} {u : Set B} {x : B}
 
--- TODO: give a much better name!
-lemma continuousWithinAt_aux
+lemma continuousWithinAt_inner_div_norm_sq
     (hs : ContinuousWithinAt (T% s) u x) (ht : ContinuousWithinAt (T% t) u x) (hs' : s x ≠ 0) :
     ContinuousWithinAt (fun x ↦ ⟪s x, t x⟫ / (‖s x‖ ^ 2)) u x := by
   have := (hs.inner_bundle ht).smul ((hs.inner_bundle hs).inv₀ (inner_self_ne_zero.mpr hs'))
@@ -289,22 +286,21 @@ lemma continuousWithinAt_aux
   · congr
     rw [← real_inner_self_eq_norm_sq]
 
-lemma continuousAt_aux (hs : ContinuousAt (T% s) x) (ht : ContinuousAt (T% t) x) (hs' : s x ≠ 0) :
+lemma continuousAt_inner_div_norm_sq
+    (hs : ContinuousAt (T% s) x) (ht : ContinuousAt (T% t) x) (hs' : s x ≠ 0) :
     ContinuousAt (fun x ↦ ⟪s x, t x⟫ / (‖s x‖ ^ 2)) x := by
   rw [← continuousWithinAt_univ] at hs ht ⊢
-  exact continuousWithinAt_aux hs ht hs'
+  exact continuousWithinAt_inner_div_norm_sq hs ht hs'
 
 def ContinuousWithinAt.starProjection
     (hs : ContinuousWithinAt (T% s) u x) (ht : ContinuousWithinAt (T% t) u x) (hs' : s x ≠ 0) :
-    -- TODO: leaving out the type ascription yields a horrible error message, add test and fix!
-    letI S : (x : B) → E x := fun x ↦ (Submodule.span ℝ {s x}).orthogonalProjection (t x);
-    ContinuousWithinAt (T% S) u x := by
+    ContinuousWithinAt (T% fun x ↦ (Submodule.span ℝ {s x}).starProjection (t x)) u x := by
   simp [Submodule.starProjection_singleton]
-  sorry -- missing API! exact (continuousWithinAt_aux hs ht hs').smul_section hs
+  exact (continuousWithinAt_inner_div_norm_sq hs ht hs').smul_section hs
 
 lemma continuousWithinAt_inner (hs : ContinuousWithinAt (T% s) u x) :
     ContinuousWithinAt (‖s ·‖) u x := by
-  convert (Real.continuous_sqrt.continuousWithinAt).comp (hs.inner_bundle hs) (Set.mapsTo_image _ u)
+  convert (Real.continuous_sqrt.continuousWithinAt).comp (hs.inner_bundle hs) (u.mapsTo_image _)
   simp [← norm_eq_sqrt_real_inner]
 
 end helper
@@ -316,20 +312,24 @@ attribute [local instance] IsWellOrder.toHasWellFounded
 lemma gramSchmidt_continuousWithinAt (hs : ∀ i, ContinuousWithinAt (T% (s i)) u x)
     {i : ι} (hs' : LinearIndependent ℝ ((s · x) ∘ ((↑) : Set.Iic i → ι))) :
     ContinuousWithinAt (T% (VectorBundle.gramSchmidt s i)) u x := by
-  sorry /- simp_rw [VectorBundle.gramSchmidt_def]
-  apply (hs i).sub_section
-  apply ContMDiffWithinAt.sum_section
+  suffices ContinuousWithinAt (T% (fun x ↦ (s i x -
+      ∑ i_1 ∈ Iio i, (span ℝ {VectorBundle.gramSchmidt s i_1 x}).starProjection (s i x)))) u x by
+    apply ContinuousWithinAt.congr this
+    · simp_rw [VectorBundle.gramSchmidt_def s i]; intros; trivial
+    · rw [VectorBundle.gramSchmidt_def s i]
+  refine ContinuousWithinAt.sub_section (𝕜 := ℝ) (hs i) ?_
+  refine ContinuousWithinAt.sum_section (𝕜 := ℝ) ?_
   intro i' hi'
   let aux : { x // x ∈ Set.Iic i' } → { x // x ∈ Set.Iic i } :=
     fun ⟨x, hx⟩ ↦ ⟨x, hx.trans (Finset.mem_Iio.mp hi').le⟩
   have : LinearIndependent ℝ ((fun x_1 ↦ s x_1 x) ∘ @Subtype.val ι fun x ↦ x ∈ Set.Iic i') := by
     apply hs'.comp aux
     intro ⟨x, hx⟩ ⟨x', hx'⟩ h
     simp_all only [Subtype.mk.injEq, aux]
-  apply ContMDiffWithinAt.orthogonalProjection (gramSchmidt_contMDiffWithinAt hs this) (hs i)
-  apply VectorBundle.gramSchmidt_ne_zero_coe _ this -/
--- termination_by i
--- decreasing_by exact (LocallyFiniteOrderBot.finset_mem_Iio i i').mp hi'
+  exact ContinuousWithinAt.starProjection (gramSchmidt_continuousWithinAt hs this) (hs i)
+    (VectorBundle.gramSchmidt_ne_zero_coe _ this)
+  termination_by i
+  decreasing_by exact (LocallyFiniteOrderBot.finset_mem_Iio i i').mp hi'
 
 lemma gramSchmidt_continuousAt (hs : ∀ i, ContinuousAt (T% (s i)) x)
     (hs' : LinearIndependent ℝ ((s · x) ∘ ((↑) : Set.Iic i → ι))) :
@@ -353,12 +353,10 @@ lemma gramSchmidtNormed_continuousWithinAt (hs : ∀ i, ContinuousWithinAt (T% (
     ContinuousWithinAt (T% (VectorBundle.gramSchmidtNormed s i)) u x := by
   have : ContinuousWithinAt (T%
       (fun x ↦ ‖VectorBundle.gramSchmidt s i x‖⁻¹ • VectorBundle.gramSchmidt s i x)) u x := by
-    sorry
-  --   refine ContMDiffWithinAt.smul_section ?_ (gramSchmidt_contMDiffWithinAt hs hs')
-  --   refine ContMDiffWithinAt.inv₀ ?_ ?_
-  --   · refine contMDiffWithinAt_inner (gramSchmidt_contMDiffWithinAt hs hs') ?_
-  --     simpa using InnerProductSpace.gramSchmidt_ne_zero_coe i hs'
-  --   · simpa using InnerProductSpace.gramSchmidt_ne_zero_coe i hs'
+    refine ContinuousWithinAt.smul_section (𝕜 := ℝ) ?_
+      (gramSchmidt_continuousWithinAt hs hs')
+    refine (continuousWithinAt_inner (gramSchmidt_continuousWithinAt hs hs')).inv₀ ?_
+    simpa using InnerProductSpace.gramSchmidt_ne_zero_coe i hs'
   exact this.congr (fun y hy ↦ by congr) (by congr)
 
 lemma gramSchmidtNormed_continuousAt (hs : ∀ i, ContinuousAt (T% (s i)) x)
@@ -401,8 +399,7 @@ section helper
 
 variable {s t : (x : B) → E x} {u : Set B} {x : B}
 
--- TODO: give a much better name!
-lemma contMDiffWithinAt_aux
+lemma contMDiffWithinAt_inner_div_norm_sq
     (hs : CMDiffAt[u] n (T% s) x) (ht : CMDiffAt[u] n (T% t) x) (hs' : s x ≠ 0) :
     CMDiffAt[u] n (fun x ↦ ⟪s x, t x⟫ / (‖s x‖ ^ 2)) x := by
   have := (hs.inner_bundle ht).smul ((hs.inner_bundle hs).inv₀ (inner_self_ne_zero.mpr hs'))
@@ -413,18 +410,17 @@ lemma contMDiffWithinAt_aux
   · congr
     rw [← real_inner_self_eq_norm_sq]
 
-lemma contMDiffAt_aux (hs : CMDiffAt n (T% s) x) (ht : CMDiffAt n (T% t) x) (hs' : s x ≠ 0) :
+lemma contMDiffAt_inner_div_norm_sq
+    (hs : CMDiffAt n (T% s) x) (ht : CMDiffAt n (T% t) x) (hs' : s x ≠ 0) :
     CMDiffAt n (fun x ↦ ⟪s x, t x⟫ / (‖s x‖ ^ 2)) x := by
   rw [← contMDiffWithinAt_univ] at hs ht ⊢
-  exact contMDiffWithinAt_aux hs ht hs'
+  exact contMDiffWithinAt_inner_div_norm_sq hs ht hs'
 
 def ContMDiffWithinAt.starProjection
     (hs : CMDiffAt[u] n (T% s) x) (ht : CMDiffAt[u] n (T% t) x) (hs' : s x ≠ 0) :
-    -- TODO: leaving out the type ascription yields a horrible error message, add test and fix!
-    letI S : (x : B) → E x := fun x ↦ (Submodule.span ℝ {s x}).starProjection (t x);
-    CMDiffAt[u] n (T% S) x := by
+    CMDiffAt[u] n (T% fun x ↦ (Submodule.span ℝ {s x}).starProjection (t x)) x := by
   simp_rw [Submodule.starProjection_singleton]
-  exact (contMDiffWithinAt_aux hs ht hs').smul_section hs
+  exact (contMDiffWithinAt_inner_div_norm_sq hs ht hs').smul_section hs
 
 lemma contMDiffWithinAt_inner (hs : CMDiffAt[u] n (T% s) x) (hs' : s x ≠ 0) :
     CMDiffAt[u] n (‖s ·‖) x := by

Mathlib/Geometry/Manifold/VectorBundle/Riemannian.lean

@@ -70,6 +70,12 @@ lemma IsContMDiffRiemannianBundle.of_le [h : IsContMDiffRiemannianBundle IB n F
   rcases h.exists_contMDiff with ⟨g, g_smooth, hg⟩
   exact ⟨g, g_smooth.of_le h', hg⟩
 
+/-- A smooth Riemannian bundle is in particular a continuous Riemannian bundle. -/
+lemma IsContMDiffRiemannianBundle.toIsContinuousRiemannianBundle
+    [h : IsContMDiffRiemannianBundle IB n F E] : IsContinuousRiemannianBundle F E := by
+  rcases h.exists_contMDiff with ⟨g, hg, hinner⟩
+  exact ⟨⟨g, hg.continuous, hinner⟩⟩
+
 instance {a : WithTop ℕ∞} [IsContMDiffRiemannianBundle IB ∞ F E] [h : LEInfty a] :
     IsContMDiffRiemannianBundle IB a F E :=
   IsContMDiffRiemannianBundle.of_le h.out

Mathlib/Topology/VectorBundle/Hom.lean

@@ -533,3 +533,170 @@ theorem inCoordinates_apply_eq₂
 end TwoVariables
 
 end
+
+section Operations
+
+variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
+  {M : Type*} [TopologicalSpace M]
+  {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+  {V : M → Type*} [TopologicalSpace (TotalSpace F V)]
+  [∀ x, TopologicalSpace (V x)] [FiberBundle F V]
+
+variable {f : M → 𝕜} {a : 𝕜} {s t : Π x : M, V x} {u : Set M} {x₀ : M}
+
+local notation "T% " s => (fun x ↦ TotalSpace.mk' F x (s x))
+
+lemma continuousWithinAt_section : ContinuousWithinAt (T% s) u x₀ ↔
+    ContinuousWithinAt (fun x ↦ (trivializationAt F V x₀ ⟨x, s x⟩).2) u x₀ := by
+  rw [FiberBundle.continuousWithinAt_totalSpace]
+  simpa using (and_iff_right continuousWithinAt_id)
+
+variable [∀ x, AddCommGroup (V x)] [∀ x, Module 𝕜 (V x)] [VectorBundle 𝕜 F V]
+
+include 𝕜
+
+lemma ContinuousWithinAt.add_section (hs : ContinuousWithinAt (T% s) u x₀)
+    (ht : ContinuousWithinAt (T% t) u x₀) : ContinuousWithinAt (T% (s + t)) u x₀ := by
+  rw [continuousWithinAt_section] at hs ht ⊢
+  set e := trivializationAt F V x₀
+  refine (hs.add ht).congr_of_eventuallyEq ?_ ?_
+  · filter_upwards [mem_nhdsWithin_of_mem_nhds
+      (e.open_baseSet.mem_nhds (mem_baseSet_trivializationAt F V x₀))] with x hx
+    apply (e.linear 𝕜 hx).1
+  · apply (e.linear 𝕜 (FiberBundle.mem_baseSet_trivializationAt' x₀)).1
+
+lemma ContinuousAt.add_section (hs : ContinuousAt (T% s) x₀) (ht : ContinuousAt (T% t) x₀) :
+    ContinuousAt (T% (s + t)) x₀ := by
+  rw [← continuousWithinAt_univ] at hs ht ⊢
+  exact hs.add_section (𝕜 := 𝕜) ht
+
+lemma ContinuousOn.add_section (hs : ContinuousOn (T% s) u) (ht : ContinuousOn (T% t) u) :
+    ContinuousOn (T% (s + t)) u :=
+  fun x₀ hx₀ ↦ (hs x₀ hx₀).add_section (𝕜 := 𝕜) (ht x₀ hx₀)
+
+lemma Continuous.add_section (hs : Continuous (T% s)) (ht : Continuous (T% t)) :
+    Continuous (T% (s + t)) := by
+  simp_rw [continuous_iff_continuousAt] at hs ht ⊢
+  exact fun x₀ ↦ (hs x₀).add_section (𝕜 := 𝕜) (ht x₀)
+
+lemma ContinuousWithinAt.neg_section (hs : ContinuousWithinAt (T% s) u x₀) :
+    ContinuousWithinAt (T% (-s)) u x₀ := by
+  rw [continuousWithinAt_section] at hs ⊢
+  set e := trivializationAt F V x₀
+  refine hs.neg.congr_of_eventuallyEq ?_ ?_
+  · filter_upwards [mem_nhdsWithin_of_mem_nhds
+      (e.open_baseSet.mem_nhds (mem_baseSet_trivializationAt F V x₀))] with x hx
+    apply (e.linear 𝕜 hx).map_neg
+  · apply (e.linear 𝕜 (FiberBundle.mem_baseSet_trivializationAt' x₀)).map_neg
+
+lemma ContinuousAt.neg_section (hs : ContinuousAt (T% s) x₀) : ContinuousAt (T% (-s)) x₀ := by
+  rw [← continuousWithinAt_univ] at hs ⊢
+  exact ContinuousWithinAt.neg_section (𝕜 := 𝕜) hs
+
+lemma ContinuousOn.neg_section (hs : ContinuousOn (T% s) u) : ContinuousOn (T% (-s)) u :=
+  fun x₀ hx₀ ↦ (hs x₀ hx₀).neg_section (𝕜 := 𝕜)
+
+lemma Continuous.neg_section (hs : Continuous (T% s)) : Continuous (T% (-s)) := by
+  simp_rw [continuous_iff_continuousAt] at hs ⊢
+  exact fun x₀ ↦ (hs x₀).neg_section (𝕜 := 𝕜)
+
+lemma ContinuousWithinAt.sub_section (hs : ContinuousWithinAt (T% s) u x₀)
+    (ht : ContinuousWithinAt (T% t) u x₀) : ContinuousWithinAt (T% (s - t)) u x₀ := by
+  rw [sub_eq_add_neg]
+  exact hs.add_section (𝕜 := 𝕜) (ht.neg_section (𝕜 := 𝕜))
+
+lemma ContinuousAt.sub_section (hs : ContinuousAt (T% s) x₀) (ht : ContinuousAt (T% t) x₀) :
+    ContinuousAt (T% (s - t)) x₀ := by
+  rw [sub_eq_add_neg]
+  exact hs.add_section (𝕜 := 𝕜) (ht.neg_section (𝕜 := 𝕜))
+
+lemma ContinuousOn.sub_section (hs : ContinuousOn (T% s) u) (ht : ContinuousOn (T% t) u) :
+    ContinuousOn (T% (s - t)) u :=
+  fun x₀ hx₀ ↦ (hs x₀ hx₀).sub_section (𝕜 := 𝕜) (ht x₀ hx₀)
+
+lemma Continuous.sub_section (hs : Continuous (T% s)) (ht : Continuous (T% t)) :
+    Continuous (T% (s - t)) := by
+  simp_rw [continuous_iff_continuousAt] at hs ht ⊢
+  exact fun x₀ ↦ (hs x₀).sub_section (𝕜 := 𝕜) (ht x₀)
+
+lemma ContinuousWithinAt.smul_section (hf : ContinuousWithinAt f u x₀)
+    (hs : ContinuousWithinAt (T% s) u x₀) : ContinuousWithinAt (T% (fun x ↦ f x • s x)) u x₀ := by
+  rw [continuousWithinAt_section] at hs ⊢
+  set e := trivializationAt F V x₀
+  refine (hf.smul hs).congr_of_eventuallyEq ?_ ?_
+  · filter_upwards [mem_nhdsWithin_of_mem_nhds
+      (e.open_baseSet.mem_nhds (mem_baseSet_trivializationAt F V x₀))] with x hx
+    apply (e.linear 𝕜 hx).2
+  · apply (e.linear 𝕜 (FiberBundle.mem_baseSet_trivializationAt' x₀)).2
+
+lemma ContinuousAt.smul_section (hf : ContinuousAt f x₀) (hs : ContinuousAt (T% s) x₀) :
+    ContinuousAt (T% (fun x ↦ f x • s x)) x₀ := by
+  rw [← continuousWithinAt_univ] at hf hs ⊢
+  exact hf.smul_section hs
+
+lemma ContinuousOn.smul_section (hf : ContinuousOn f u) (hs : ContinuousOn (T% s) u) :
+    ContinuousOn (T% (fun x ↦ f x • s x)) u :=
+  fun x₀ hx₀ ↦ (hf x₀ hx₀).smul_section (hs x₀ hx₀)
+
+lemma Continuous.smul_section (hf : Continuous f) (hs : Continuous (T% s)) :
+    Continuous (T% (fun x ↦ f x • s x)) := by
+  simp_rw [continuous_iff_continuousAt] at hf hs ⊢
+  exact fun x₀ ↦ (hf x₀).smul_section (hs x₀)
+
+lemma ContinuousWithinAt.const_smul_section (hs : ContinuousWithinAt (T% s) u x₀) :
+    ContinuousWithinAt (T% (a • s)) u x₀ :=
+  continuousWithinAt_const.smul_section hs
+
+lemma ContinuousAt.const_smul_section (hs : ContinuousAt (T% s) x₀) :
+    ContinuousAt (T% (a • s)) x₀ :=
+  continuousAt_const.smul_section hs
+
+lemma ContinuousOn.const_smul_section (hs : ContinuousOn (T% s) u) : ContinuousOn (T% (a • s)) u :=
+  continuousOn_const.smul_section hs
+
+lemma Continuous.const_smul_section (hs : Continuous (T% s)) : Continuous (T% (a • s)) := by
+  simp_rw [continuous_iff_continuousAt] at hs ⊢
+  exact fun x₀ ↦ (hs x₀).const_smul_section
+
+variable {ι : Type*} {t' : ι → (x : M) → V x}
+
+lemma continuousWithinAt_zero_section : ContinuousWithinAt (T% (0 : Π x, V x)) u x₀ := by
+  rw [continuousWithinAt_section]
+  have hconst : ContinuousWithinAt (fun _ : M ↦ (0 : F)) u x₀ := continuousWithinAt_const
+  refine hconst.congr_of_eventuallyEq ?_ ?_
+  · filter_upwards [mem_nhdsWithin_of_mem_nhds ((trivializationAt F V x₀).open_baseSet.mem_nhds
+      (mem_baseSet_trivializationAt F V x₀))] with x hx
+    exact congrArg Prod.snd <| (trivializationAt F V x₀).zeroSection 𝕜 hx
+  · exact congrArg Prod.snd <|
+      (trivializationAt F V x₀).zeroSection 𝕜 (mem_baseSet_trivializationAt F V x₀)
+
+lemma ContinuousWithinAt.sum_section {s : Finset ι}
+    (hs : ∀ i ∈ s, ContinuousWithinAt (T% (t' i)) u x₀) :
+    ContinuousWithinAt (T% (fun x ↦ ∑ i ∈ s, (t' i x))) u x₀ := by
+  classical
+  induction s using Finset.induction_on with
+  | empty =>
+    simpa only [Finset.sum_empty] using continuousWithinAt_zero_section (𝕜 := 𝕜)
+  | insert i s hi h =>
+    simp only [Finset.sum_insert hi]
+    exact (hs i (s.mem_insert_self i)).add_section (𝕜 := 𝕜)
+      (h (fun i hi ↦ hs i (s.mem_insert_of_mem hi)))
+
+lemma ContinuousAt.sum_section {s : Finset ι} (hs : ∀ i ∈ s, ContinuousAt (T% (t' i)) x₀) :
+    ContinuousAt (T% (fun x ↦ ∑ i ∈ s, (t' i x))) x₀ := by
+  have hs' : ∀ i ∈ s, ContinuousWithinAt (T% (t' i)) univ x₀ := by
+    intro i hi
+    simpa [← continuousWithinAt_univ] using hs i hi
+  simpa [← continuousWithinAt_univ] using (ContinuousWithinAt.sum_section (𝕜 := 𝕜) hs')
+
+lemma ContinuousOn.sum_section {s : Finset ι} (hs : ∀ i ∈ s, ContinuousOn (T% (t' i)) u) :
+    ContinuousOn (T% (fun x ↦ ∑ i ∈ s, (t' i x))) u :=
+  fun x₀ hx₀ ↦ ContinuousWithinAt.sum_section (𝕜 := 𝕜) (fun i hi ↦ hs i hi x₀ hx₀)
+
+lemma Continuous.sum_section {s : Finset ι} (hs : ∀ i ∈ s, Continuous (T% (t' i))) :
+    Continuous (T% (fun x ↦ ∑ i ∈ s, (t' i x))) := by
+  simp_rw [continuous_iff_continuousAt] at hs ⊢
+  intro x₀
+  exact ContinuousAt.sum_section (𝕜 := 𝕜) (fun i hi ↦ hs i hi x₀)
+
+end Operations