WIP: do the same for continuous bundles --- need more API for operations on continuous sections first

Author: grunweg

Mathlib/Geometry/Manifold/VectorBundle/GramSchmidtOrtho.lean

@@ -267,6 +267,140 @@ theorem gramSchmidtOrthonormalBasis_apply_of_orthonormal [Fintype ι]
 
 end VectorBundle
 
+/-! The Gram-Schmidt process preserves continuity of sections -/
+section continuity
+
+-- -- Let `V` be a smooth vector bundle with a `C^n` Riemannian structure over a `C^k` manifold `B`.
+-- variable
+--   {EB : Type*} [NormedAddCommGroup EB] [NormedSpace ℝ EB]
+--   {HB : Type*} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞}
+--   {B : Type*} [TopologicalSpace B] [ChartedSpace HB B]
+--   {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
+--   {E : B → Type*} [TopologicalSpace (TotalSpace F E)] [∀ x, NormedAddCommGroup (E x)]
+--   [∀ x, InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E]
+--   [IsManifold IB n B] [ContMDiffVectorBundle n F E IB]
+--   [IsContMDiffRiemannianBundle IB n F E]
+
+--variable [IsContMDiffRiemannianBundle IB n F E]
+
+-- section helper
+
+-- variable {s t : (x : B) → E x} {u : Set B} {x : B}
+
+-- -- TODO: give a much better name!
+-- lemma contMDiffWithinAt_aux
+--     (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'))
+--   apply this.congr
+--   · intro y hy
+--     congr
+--     simp [inner_self_eq_norm_sq_to_K]
+--   · 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) :
+--     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'
+
+-- def ContMDiffWithinAt.orthogonalProjection
+--     (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}).orthogonalProjection (t x);
+--     CMDiffAt[u] n (T% S) x := by
+--   simp_rw [Submodule.orthogonalProjection_singleton]
+--   exact (contMDiffWithinAt_aux 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
+--   let F (x) := ⟪s x, s x⟫
+--   have aux : CMDiffAt[u] n (Real.sqrt ∘ F) x := by
+--     have h1 : CMDiffAt[(F '' u)] n (Real.sqrt) (F x) := by
+--       apply ContMDiffAt.contMDiffWithinAt
+--       rw [contMDiffAt_iff_contDiffAt]
+--       exact Real.contDiffAt_sqrt (by simp [F, hs'])
+--     exact h1.comp x (hs.inner_bundle hs) (Set.mapsTo_image _ u)
+--   convert aux
+--   simp [F, ← norm_eq_sqrt_real_inner]
+
+-- end helper
+
+variable {s : ι → (x : B) → E x} {u : Set B} {x : B} {i : ι}
+
+attribute [local instance] IsWellOrder.toHasWellFounded
+
+-- TODO: need continuity analogues of ContMDiff.sub_section
+
+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
+  simp_rw [VectorBundle.gramSchmidt_def]
+  sorry /-apply (hs i).sub_section
+  apply ContMDiffWithinAt.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'
+
+lemma gramSchmidt_continuousAt (hs : ∀ i, ContinuousAt (T% (s i)) x)
+    (hs' : LinearIndependent ℝ ((s · x) ∘ ((↑) : Set.Iic i → ι))) :
+    ContinuousAt (T% (VectorBundle.gramSchmidt s i)) x := by
+  simp_rw [← continuousWithinAt_univ] at hs ⊢
+  exact gramSchmidt_continuousWithinAt (fun i ↦ hs i) hs'
+
+lemma gramSchmidt_contMDiffOn (hs : ∀ i, ContinuousOn (T% (s i)) u)
+    (hs' : ∀ x ∈ u, LinearIndependent ℝ ((s · x) ∘ ((↑) : Set.Iic i → ι))) :
+    ContinuousOn (T% (VectorBundle.gramSchmidt s i)) u :=
+  fun x hx ↦ gramSchmidt_continuousWithinAt (fun i ↦ hs i x hx) (hs' _ hx)
+
+lemma gramSchmidt_continuous (hs : ∀ i, Continuous (T% (s i)))
+    (hs' : ∀ x, LinearIndependent ℝ ((s · x) ∘ ((↑) : Set.Iic i → ι))) :
+    Continuous (T% (VectorBundle.gramSchmidt s i)) := by
+  simp_rw [continuous_iff_continuousAt] at hs ⊢
+  exact fun x ↦ gramSchmidt_continuousAt (fun i ↦ hs i x) (hs' x)
+
+lemma gramSchmidtNormed_continuousWithinAt (hs : ∀ i, ContinuousWithinAt (T% (s i)) u x)
+    (hs' : LinearIndependent ℝ ((s · x) ∘ ((↑) : Set.Iic i → ι))) :
+    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'
+  exact this.congr (fun y hy ↦ by congr) (by congr)
+
+lemma gramSchmidtNormed_continuousAt (hs : ∀ i, ContinuousAt (T% (s i)) x)
+    (hs' : LinearIndependent ℝ ((s · x) ∘ ((↑) : Set.Iic i → ι))) :
+    ContinuousAt (T% (VectorBundle.gramSchmidtNormed s i)) x := by
+  simp_rw [← continuousWithinAt_univ] at hs ⊢
+  exact gramSchmidtNormed_continuousWithinAt (fun i ↦ hs i) hs'
+
+lemma gramSchmidtNormed_continuousOn (hs : ∀ i, ContinuousOn (T% (s i)) u)
+    (hs' : ∀ x ∈ u, LinearIndependent ℝ ((s · x) ∘ ((↑) : Set.Iic i → ι))) :
+    ContinuousOn (T% (VectorBundle.gramSchmidtNormed s i)) u :=
+  fun x hx ↦ gramSchmidtNormed_continuousWithinAt (fun i ↦ hs i x hx) (hs' _ hx)
+
+lemma gramSchmidtNormed_continuous (hs : ∀ i, Continuous (T% (s i)))
+    (hs' : ∀ x, LinearIndependent ℝ ((s · x) ∘ ((↑) : Set.Iic i → ι))) :
+    Continuous (T% (VectorBundle.gramSchmidtNormed s i)) := by
+  simp_rw [continuous_iff_continuousAt] at hs ⊢
+  exact fun x ↦ gramSchmidtNormed_continuousAt (fun i ↦ hs i x) (hs' x)
+
+end continuity
+
+#exit
+
 /-! The Gram-Schmidt process preserves smoothness of sections -/
 section smoothness