chore(Analysis/InnerProductAlgebra/Projection): adding norm and other results for Submodule.starProjection (#27317)

Analogue results for `Submodule.starProjection`.

Author: themathqueen

Mathlib/Analysis/InnerProductSpace/Projection.lean

@@ -588,6 +588,10 @@ theorem orthogonalProjection_mem_subspace_eq_self (v : K) : K.orthogonalProjecti
   ext
   apply eq_starProjection_of_mem_of_inner_eq_zero <;> simp
 
+@[simp]
+theorem starProjection_mem_subspace_eq_self (v : K) :
+    K.starProjection v = v := by simp [starProjection_apply]
+
 /-- A point equals its orthogonal projection if and only if it lies in the subspace. -/
 theorem starProjection_eq_self_iff {v : E} : K.starProjection v = v ↔ v ∈ K := by
   refine ⟨fun h => ?_, fun h => eq_starProjection_of_mem_of_inner_eq_zero h ?_⟩
@@ -684,22 +688,36 @@ variable (K)
 theorem orthogonalProjection_norm_le : ‖K.orthogonalProjection‖ ≤ 1 :=
   LinearMap.mkContinuous_norm_le _ (by norm_num) _
 
+theorem starProjection_norm_le : ‖K.starProjection‖ ≤ 1 :=
+  K.orthogonalProjection_norm_le
+
 theorem norm_orthogonalProjection_apply {v : E} (hv : v ∈ K) :
     ‖orthogonalProjection K v‖ = ‖v‖ :=
   congr(‖$(K.starProjection_eq_self_iff.mpr hv)‖)
 
+theorem norm_starProjection_apply {v : E} (hv : v ∈ K) :
+    ‖K.starProjection v‖ = ‖v‖ :=
+  norm_orthogonalProjection_apply _ hv
+
 /-- The orthogonal projection onto a closed subspace is norm non-increasing. -/
 theorem norm_orthogonalProjection_apply_le (v : E) :
     ‖orthogonalProjection K v‖ ≤ ‖v‖ := by calc
   ‖orthogonalProjection K v‖ ≤ ‖orthogonalProjection K‖ * ‖v‖ := K.orthogonalProjection.le_opNorm _
   _ ≤ 1 * ‖v‖ := by gcongr; exact orthogonalProjection_norm_le K
   _ = _ := by simp
 
+theorem norm_starProjection_apply_le (v : E) :
+    ‖K.starProjection v‖ ≤ ‖v‖ := K.norm_orthogonalProjection_apply_le v
+
 /-- The orthogonal projection onto a closed subspace is a `1`-Lipschitz map. -/
 theorem lipschitzWith_orthogonalProjection :
     LipschitzWith 1 (orthogonalProjection K) :=
   ContinuousLinearMap.lipschitzWith_of_opNorm_le (orthogonalProjection_norm_le K)
 
+theorem lipschitzWith_starProjection :
+    LipschitzWith 1 K.starProjection :=
+  ContinuousLinearMap.lipschitzWith_of_opNorm_le (starProjection_norm_le K)
+
 /-- The operator norm of the orthogonal projection onto a nontrivial subspace is `1`. -/
 theorem norm_orthogonalProjection (hK : K ≠ ⊥) :
     ‖K.orthogonalProjection‖ = 1 := by
@@ -708,6 +726,10 @@ theorem norm_orthogonalProjection (hK : K ≠ ⊥) :
   simpa [K.norm_orthogonalProjection_apply hxK, norm_eq_zero, hx_ne_zero]
     using K.orthogonalProjection.ratio_le_opNorm x
 
+theorem norm_starProjection (hK : K ≠ ⊥) :
+    ‖K.starProjection‖ = 1 :=
+  K.norm_orthogonalProjection hK
+
 variable (𝕜)
 
 theorem smul_starProjection_singleton {v : E} (w : E) :
@@ -959,6 +981,13 @@ theorem IsOrtho.orthogonalProjection_comp_subtypeL {U V : Submodule 𝕜 E}
   ContinuousLinearMap.ext fun v =>
     orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero <| h.symm v.prop
 
+theorem IsOrtho.starProjection_comp_starProjection {U V : Submodule 𝕜 E}
+    [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] (h : U ⟂ V) :
+    U.starProjection ∘L V.starProjection = 0 :=
+  calc _ = U.subtypeL ∘L (U.orthogonalProjection ∘L V.subtypeL) ∘L V.orthogonalProjection := by
+        simp only [starProjection, ContinuousLinearMap.comp_assoc]
+    _ = 0 := by simp [h.orthogonalProjection_comp_subtypeL]
+
 /-- The projection into `U` from `V` is the zero map if and only if `U` and `V` are orthogonal. -/
 theorem orthogonalProjection_comp_subtypeL_eq_zero_iff {U V : Submodule 𝕜 E}
     [U.HasOrthogonalProjection] : U.orthogonalProjection ∘L V.subtypeL = 0 ↔ U ⟂ V :=
@@ -968,6 +997,17 @@ theorem orthogonalProjection_comp_subtypeL_eq_zero_iff {U V : Submodule 𝕜 E}
     rw [starProjection_apply, this, Submodule.coe_zero, sub_zero],
     Submodule.IsOrtho.orthogonalProjection_comp_subtypeL⟩
 
+/-- `U.starProjection ∘ V.starProjection = 0` iff `U` and `V` are pairwise orthogonal. -/
+theorem starProjection_comp_starProjection_eq_zero_iff {U V : Submodule 𝕜 E}
+    [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] :
+    U.starProjection ∘L V.starProjection = 0 ↔ U ⟂ V := by
+  refine ⟨fun h => ?_, fun h => h.starProjection_comp_starProjection⟩
+  rw [← orthogonalProjection_comp_subtypeL_eq_zero_iff]
+  simp only [ContinuousLinearMap.ext_iff, ContinuousLinearMap.comp_apply, subtypeL_apply,
+    starProjection_apply, ContinuousLinearMap.zero_apply, coe_eq_zero] at h ⊢
+  intro x
+  simpa using h (x : E)
+
 theorem orthogonalProjection_eq_linear_proj [K.HasOrthogonalProjection] (x : E) :
     K.orthogonalProjection x =
       K.linearProjOfIsCompl _ Submodule.isCompl_orthogonal_of_completeSpace x := by
@@ -988,10 +1028,20 @@ theorem reflection_mem_subspace_orthogonalComplement_eq_neg [K.HasOrthogonalProj
     orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero hv]
 
 /-- The orthogonal projection onto `Kᗮ` of an element of `K` is zero. -/
-theorem orthogonalProjection_mem_subspace_orthogonal_precomplement_eq_zero
+theorem orthogonalProjection_orthogonal_apply_eq_zero
     [Kᗮ.HasOrthogonalProjection] {v : E} (hv : v ∈ K) : Kᗮ.orthogonalProjection v = 0 :=
   orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero (K.le_orthogonal_orthogonal hv)
 
+@[deprecated (since := "22-07-2025")] alias
+  orthogonalProjection_mem_subspace_orthogonal_precomplement_eq_zero :=
+  orthogonalProjection_orthogonal_apply_eq_zero
+
+theorem starProjection_orthogonal_apply_eq_zero
+    [Kᗮ.HasOrthogonalProjection] {v : E} (hv : v ∈ K) :
+    Kᗮ.starProjection v = 0 := by
+  rw [starProjection_apply, coe_eq_zero]
+  exact orthogonalProjection_orthogonal_apply_eq_zero hv
+
 /-- If `U ≤ V`, then projecting on `V` and then on `U` is the same as projecting on `U`. -/
 theorem orthogonalProjection_starProjection_of_le {U V : Submodule 𝕜 E}
     [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] (h : U ≤ V) (x : E) :
@@ -1004,6 +1054,12 @@ theorem orthogonalProjection_starProjection_of_le {U V : Submodule 𝕜 E}
 @[deprecated (since := "2025-07-07")] alias orthogonalProjection_orthogonalProjection_of_le :=
   orthogonalProjection_starProjection_of_le
 
+theorem starProjection_comp_starProjection_of_le {U V : Submodule 𝕜 E}
+    [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] (h : U ≤ V) :
+    U.starProjection ∘L V.starProjection = U.starProjection := ContinuousLinearMap.ext fun _ => by
+  nth_rw 1 [starProjection]
+  simp [orthogonalProjection_starProjection_of_le h]
+
 /-- Given a monotone family `U` of complete submodules of `E` and a fixed `x : E`,
 the orthogonal projection of `x` on `U i` tends to the orthogonal projection of `x` on
 `(⨆ i, U i).topologicalClosure` along `atTop`. -/
@@ -1116,9 +1172,14 @@ theorem reflection_mem_subspace_orthogonal_precomplement_eq_neg [K.HasOrthogonal
 /-- The orthogonal projection onto `(𝕜 ∙ v)ᗮ` of `v` is zero. -/
 theorem orthogonalProjection_orthogonalComplement_singleton_eq_zero (v : E) :
     (𝕜 ∙ v)ᗮ.orthogonalProjection v = 0 :=
-  orthogonalProjection_mem_subspace_orthogonal_precomplement_eq_zero
+  orthogonalProjection_orthogonal_apply_eq_zero
     (Submodule.mem_span_singleton_self v)
 
+theorem starProjection_orthogonalComplement_singleton_eq_zero (v : E) :
+    (𝕜 ∙ v)ᗮ.starProjection v = 0 := by
+  rw [starProjection_apply, coe_eq_zero]
+  exact orthogonalProjection_orthogonalComplement_singleton_eq_zero v
+
 /-- The reflection in `(𝕜 ∙ v)ᗮ` of `v` is `-v`. -/
 theorem reflection_orthogonalComplement_singleton_eq_neg (v : E) : reflection (𝕜 ∙ v)ᗮ v = -v :=
   reflection_mem_subspace_orthogonal_precomplement_eq_neg (Submodule.mem_span_singleton_self v)
@@ -1195,6 +1256,11 @@ theorem norm_sq_eq_add_norm_sq_projection (x : E) (S : Submodule 𝕜 E) [S.HasO
       exact norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero _ _ <|
         (S.mem_orthogonal _).1 (Sᗮ.orthogonalProjection x).2 _ (S.orthogonalProjection x).2
 
+theorem norm_sq_eq_add_norm_sq_starProjection (x : E) (S : Submodule 𝕜 E)
+    [S.HasOrthogonalProjection] :
+    ‖x‖ ^ 2 = ‖S.starProjection x‖ ^ 2 + ‖Sᗮ.starProjection x‖ ^ 2 :=
+  norm_sq_eq_add_norm_sq_projection x S
+
 /-- In a complete space `E`, the projection maps onto a complete subspace `K` and its orthogonal
 complement sum to the identity. -/
 theorem id_eq_sum_starProjection_self_orthogonalComplement [K.HasOrthogonalProjection] :
@@ -1240,6 +1306,13 @@ theorem starProjection_isSymmetric [K.HasOrthogonalProjection] :
 @[deprecated (since := "2025-07-07")] alias
   orthogonalProjection_isSymmetric := starProjection_isSymmetric
 
+theorem starProjection_apply_eq_zero_iff [K.HasOrthogonalProjection] {v : E} :
+    K.starProjection v = 0 ↔ v ∈ Kᗮ := by
+  refine ⟨fun h w hw => ?_, fun hv => ?_⟩
+  · rw [← starProjection_eq_self_iff.mpr hw, inner_starProjection_left_eq_right, h,
+      inner_zero_right]
+  · simp [starProjection_apply, orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero hv]
+
 lemma re_inner_starProjection_eq_normSq [K.HasOrthogonalProjection] (v : E) :
     re ⟪K.starProjection v, v⟫ = ‖K.orthogonalProjection v‖^2 := by
   rw [starProjection_apply,