feat: Gram-Schmidt orthonormalisation preserves continuity of sections

Mathlib.lean

@@ -3765,6 +3765,7 @@ import Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
 import Mathlib.Geometry.Manifold.Sheaf.Smooth
 import Mathlib.Geometry.Manifold.VectorBundle.Basic
 import Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
+import Mathlib.Geometry.Manifold.VectorBundle.GramSchmidtOrtho
 import Mathlib.Geometry.Manifold.VectorBundle.Hom
 import Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
 import Mathlib.Geometry.Manifold.VectorBundle.Pullback

Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean

@@ -31,7 +31,6 @@ and outputs a set of orthogonal vectors which have the same span.
   an indexed set of vectors of the right size
 -/
 
-
 open Finset Submodule Module
 
 variable (𝕜 : Type*) {E : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
@@ -119,7 +118,7 @@ theorem gramSchmidt_inv_triangular (v : ι → E) {i j : ι} (hij : i < j) :
   have : ⟪b j, b k⟫ = 0 := gramSchmidt_orthogonal 𝕜 v (hki.trans hij).ne'
   simp [this]
 
-open Submodule Set Order
+open Set
 
 theorem mem_span_gramSchmidt (f : ι → E) {i j : ι} (hij : i ≤ j) :
     f i ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j) := by
@@ -160,8 +159,8 @@ theorem span_gramSchmidt (f : ι → E) : span 𝕜 (range (gramSchmidt 𝕜 f))
       range_subset_iff.2 fun _ =>
         span_mono (image_subset_range _ _) <| mem_span_gramSchmidt _ _ le_rfl
 
-/-- If given an orthogonal set of vectors, `gramSchmidt` fixes its input. -/
-theorem gramSchmidt_of_orthogonal {f : ι → E} (hf : Pairwise (⟪f ·, f ·⟫ = 0)) :
+/-- The `gramSchmidt` operator acts as the identity on set of mutually orthogonal vectors. -/
+theorem gramSchmidt_of_orthogonal {f : ι → E} (hf : Pairwise fun i j => ⟪f i, f j⟫ = 0) :
     gramSchmidt 𝕜 f = f := by
   ext i
   rw [gramSchmidt_def]
@@ -235,14 +234,14 @@ variable (𝕜) in
 noncomputable def gramSchmidtNormed (f : ι → E) (n : ι) : E :=
   (‖gramSchmidt 𝕜 f n‖ : 𝕜)⁻¹ • gramSchmidt 𝕜 f n
 
-theorem gramSchmidtNormed_unit_length_coe {f : ι → E} (n : ι)
+theorem gramSchmidtNormed_unit_length_coe {f : ι → E} {n : ι}
     (h₀ : LinearIndependent 𝕜 (f ∘ ((↑) : Set.Iic n → ι))) : ‖gramSchmidtNormed 𝕜 f n‖ = 1 := by
   simp only [gramSchmidt_ne_zero_coe n h₀, gramSchmidtNormed, norm_smul_inv_norm, Ne,
     not_false_iff]
 
-theorem gramSchmidtNormed_unit_length {f : ι → E} (n : ι) (h₀ : LinearIndependent 𝕜 f) :
+theorem gramSchmidtNormed_unit_length {f : ι → E} {n : ι} (h₀ : LinearIndependent 𝕜 f) :
     ‖gramSchmidtNormed 𝕜 f n‖ = 1 :=
-  gramSchmidtNormed_unit_length_coe _ (LinearIndependent.comp h₀ _ Subtype.coe_injective)
+  gramSchmidtNormed_unit_length_coe (LinearIndependent.comp h₀ _ Subtype.coe_injective)
 
 theorem gramSchmidtNormed_unit_length' {f : ι → E} {n : ι} (hn : gramSchmidtNormed 𝕜 f n ≠ 0) :
     ‖gramSchmidtNormed 𝕜 f n‖ = 1 := by
@@ -279,8 +278,6 @@ theorem gramSchmidtNormed_orthonormal' (f : ι → E) :
 @[deprecated (since := "2025-07-10")]
 alias gramSchmidt_orthonormal' := gramSchmidtNormed_orthonormal'
 
-open Submodule Set Order
-
 theorem span_gramSchmidtNormed (f : ι → E) (s : Set ι) :
     span 𝕜 (gramSchmidtNormed 𝕜 f '' s) = span 𝕜 (gramSchmidt 𝕜 f '' s) := by
   refine span_eq_span
@@ -301,10 +298,8 @@ theorem span_gramSchmidtNormed_range (f : ι → E) :
 vectors. -/
 theorem gramSchmidtNormed_linearIndependent {f : ι → E} (h₀ : LinearIndependent 𝕜 f) :
     LinearIndependent 𝕜 (gramSchmidtNormed 𝕜 f) := by
-  unfold gramSchmidtNormed
   have (i : ι) : IsUnit (‖gramSchmidt 𝕜 f i‖⁻¹ : 𝕜) :=
     isUnit_iff_ne_zero.mpr (by simp [gramSchmidt_ne_zero i h₀])
-  let w : ι → 𝕜ˣ := fun i ↦ (this i).unit
   apply (gramSchmidt_linearIndependent h₀).units_smul (w := fun i ↦ (this i).unit)
 
 section OrthonormalBasis