chore(Analysis/InnerProductSpace/Projection): deprecating subtypeL ∘ orthogonalProjection in favor of starProjection (#26877)

This deprecates all `U.subtypeL ∘L U.orthogonalProjection` and `(U.orthogonalProjection v : E)` in favor of `U.starProjection` and `U.starProjection v` respectively in `Analysis/InnerProductSpace/Projection` and other files.



Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>

Author: themathqueen

Mathlib/Analysis/InnerProductSpace/Adjoint.lean

@@ -295,7 +295,7 @@ theorem _root_.LinearMap.IsSymmetric.isSelfAdjoint {A : E →L[𝕜] E}
 theorem _root_.isSelfAdjoint_starProjection
     (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] :
     IsSelfAdjoint U.starProjection :=
-  U.orthogonalProjection_isSymmetric.isSelfAdjoint
+  U.starProjection_isSymmetric.isSelfAdjoint
 
 @[deprecated (since := "2025-07-05")] alias _root_.orthogonalProjection_isSelfAdjoint :=
   isSelfAdjoint_starProjection
@@ -343,7 +343,7 @@ end ContinuousLinearMap
 
 /-- `U.starProjection` is a star projection. -/
 @[simp]
-theorem isStarProjection_starProjection [CompleteSpace E] (U : Submodule 𝕜 E)
+theorem isStarProjection_starProjection [CompleteSpace E] {U : Submodule 𝕜 E}
     [U.HasOrthogonalProjection] : IsStarProjection U.starProjection :=
   ⟨U.isIdempotentElem_starProjection, isSelfAdjoint_starProjection U⟩
 
@@ -352,11 +352,11 @@ open ContinuousLinearMap in
 theorem isStarProjection_iff_eq_starProjection_range [CompleteSpace E] {p : E →L[𝕜] E} :
     IsStarProjection p ↔ ∃ (_ : (LinearMap.range p).HasOrthogonalProjection),
     p = (LinearMap.range p).starProjection := by
-  refine ⟨fun hp ↦ ?_, fun ⟨h, hp⟩ ↦ hp ▸ isStarProjection_starProjection _⟩
+  refine ⟨fun hp ↦ ?_, fun ⟨h, hp⟩ ↦ hp ▸ isStarProjection_starProjection⟩
   have := IsIdempotentElem.hasOrthogonalProjection_range hp.isIdempotentElem
   refine ⟨this, Eq.symm ?_⟩
   ext x
-  refine Submodule.eq_orthogonalProjection_of_mem_orthogonal (by simp) ?_
+  refine Submodule.eq_starProjection_of_mem_orthogonal (by simp) ?_
   simpa [p.orthogonal_range, hp.isSelfAdjoint.isSymmetric]
     using congr($(hp.isIdempotentElem.mul_one_sub_self) x)
 

Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean

@@ -59,11 +59,12 @@ theorem gramSchmidt_def' (f : ι → E) (n : ι) :
     f n = gramSchmidt 𝕜 f n + ∑ i ∈ Iio n, (𝕜 ∙ gramSchmidt 𝕜 f i).orthogonalProjection (f n) := by
   rw [gramSchmidt_def, sub_add_cancel]
 
+-- changing the definition to use `starProjection` makes the proof of this not work
 theorem gramSchmidt_def'' (f : ι → E) (n : ι) :
     f n = gramSchmidt 𝕜 f n + ∑ i ∈ Iio n,
       (⟪gramSchmidt 𝕜 f i, f n⟫ / (‖gramSchmidt 𝕜 f i‖ : 𝕜) ^ 2) • gramSchmidt 𝕜 f i := by
   convert gramSchmidt_def' 𝕜 f n
-  rw [orthogonalProjection_singleton, RCLike.ofReal_pow]
+  rw [← starProjection_apply, starProjection_singleton, RCLike.ofReal_pow]
 
 @[simp]
 theorem gramSchmidt_zero {ι : Type*} [LinearOrder ι] [LocallyFiniteOrder ι] [OrderBot ι]
@@ -84,8 +85,8 @@ theorem gramSchmidt_orthogonal (f : ι → E) {a b : ι} (h₀ : a ≠ b) :
   revert a
   apply wellFounded_lt.induction b
   intro b ih a h₀
-  simp only [gramSchmidt_def 𝕜 f b, inner_sub_right, inner_sum, orthogonalProjection_singleton,
-    inner_smul_right]
+  simp only [gramSchmidt_def 𝕜 f b, inner_sub_right, inner_sum, ← starProjection_apply,
+    starProjection_singleton, inner_smul_right]
   rw [Finset.sum_eq_single_of_mem a (Finset.mem_Iio.mpr h₀)]
   · by_cases h : gramSchmidt 𝕜 f a = 0
     · simp only [h, inner_zero_left, zero_div, zero_mul, sub_zero]
@@ -122,7 +123,7 @@ open Submodule Set Order
 theorem mem_span_gramSchmidt (f : ι → E) {i j : ι} (hij : i ≤ j) :
     f i ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j) := by
   rw [gramSchmidt_def' 𝕜 f i]
-  simp_rw [orthogonalProjection_singleton]
+  simp_rw [← starProjection_apply, starProjection_singleton]
   exact Submodule.add_mem _ (subset_span <| mem_image_of_mem _ hij)
     (Submodule.sum_mem _ fun k hk => smul_mem (span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)) _ <|
       subset_span <| mem_image_of_mem (gramSchmidt 𝕜 f) <| (Finset.mem_Iio.1 hk).le.trans hij)
@@ -131,7 +132,7 @@ theorem gramSchmidt_mem_span (f : ι → E) :
     ∀ {j i}, i ≤ j → gramSchmidt 𝕜 f i ∈ span 𝕜 (f '' Set.Iic j) := by
   intro j i hij
   rw [gramSchmidt_def 𝕜 f i]
-  simp_rw [orthogonalProjection_singleton]
+  simp_rw [← starProjection_apply, starProjection_singleton]
   refine Submodule.sub_mem _ (subset_span (mem_image_of_mem _ hij))
     (Submodule.sum_mem _ fun k hk => ?_)
   let hkj : k < j := (Finset.mem_Iio.1 hk).trans_le hij
@@ -186,7 +187,7 @@ theorem gramSchmidt_ne_zero_coe {f : ι → E} (n : ι)
     rw [← span_gramSchmidt_Iio 𝕜 f n, gramSchmidt_def' 𝕜 f, h, zero_add]
     apply Submodule.sum_mem _ _
     intro a ha
-    simp only [orthogonalProjection_singleton]
+    simp only [← starProjection_apply, starProjection_singleton]
     apply Submodule.smul_mem _ _ _
     rw [Finset.mem_Iio] at ha
     exact subset_span ⟨a, ha, by rfl⟩