feat(CstarRing): weaken the definition of CstarRing from an equality to an inequality (#14737)

This PR weakens the definition of `CstarRing` from `‖x⋆ * x‖ = ‖x‖ * ‖x‖` to `‖x‖ * ‖x‖ ≤ ‖x⋆ * x‖`. The "weaker" condition is then shown to be equivalent to the original one.

Author: dupuisf

Mathlib/Analysis/InnerProductSpace/Adjoint.lean

@@ -240,7 +240,7 @@ theorem norm_adjoint_comp_self (A : E →L[𝕜] F) :
           Real.sqrt_mul_self (norm_nonneg x)]
 
 instance : CstarRing (E →L[𝕜] E) where
-  norm_star_mul_self := norm_adjoint_comp_self _
+  norm_mul_self_le x := le_of_eq <| Eq.symm <| norm_adjoint_comp_self x
 
 theorem isAdjointPair_inner (A : E →L[𝕜] F) :
     LinearMap.IsAdjointPair (sesqFormOfInner : E →ₗ[𝕜] E →ₗ⋆[𝕜] 𝕜)

Mathlib/Analysis/NormedSpace/Star/Basic.lean

@@ -19,8 +19,8 @@ import Mathlib.Topology.Algebra.Module.Star
 A normed star group is a normed group with a compatible `star` which is isometric.
 
 A C⋆-ring is a normed star group that is also a ring and that verifies the stronger
-condition `‖x⋆ * x‖ = ‖x‖^2` for all `x`.  If a C⋆-ring is also a star algebra, then it is a
-C⋆-algebra.
+condition `‖x‖^2 ≤ ‖x⋆ * x‖` for all `x` (which actually implies equality). If a C⋆-ring is also
+a star algebra, then it is a C⋆-algebra.
 
 To get a C⋆-algebra `E` over field `𝕜`, use
 `[NormedField 𝕜] [StarRing 𝕜] [NormedRing E] [StarRing E] [CstarRing E]
@@ -79,13 +79,16 @@ instance RingHomIsometric.starRingEnd [NormedCommRing E] [StarRing E] [NormedSta
   ⟨@norm_star _ _ _ _⟩
 #align ring_hom_isometric.star_ring_end RingHomIsometric.starRingEnd
 
-/-- A C*-ring is a normed star ring that satisfies the stronger condition `‖x⋆ * x‖ = ‖x‖^2`
-for every `x`. -/
+/-- A C*-ring is a normed star ring that satisfies the stronger condition `‖x‖ ^ 2 ≤ ‖x⋆ * x‖`
+for every `x`. Note that this condition actually implies equality, as is shown in
+`norm_star_mul_self` below. -/
 class CstarRing (E : Type*) [NonUnitalNormedRing E] [StarRing E] : Prop where
-  norm_star_mul_self : ∀ {x : E}, ‖x⋆ * x‖ = ‖x‖ * ‖x‖
+  norm_mul_self_le : ∀ x : E, ‖x‖ * ‖x‖ ≤ ‖x⋆ * x‖
 #align cstar_ring CstarRing
 
-instance : CstarRing ℝ where norm_star_mul_self {x} := by simp only [star, id, norm_mul]
+instance : CstarRing ℝ where
+  norm_mul_self_le x := by
+    simp only [Real.norm_eq_abs, abs_mul_abs_self, star, id, norm_mul, le_refl]
 
 namespace CstarRing
 
@@ -101,19 +104,19 @@ instance (priority := 100) to_normedStarGroup : NormedStarGroup E :=
     by_cases htriv : x = 0
     · simp only [htriv, star_zero]
     · have hnt : 0 < ‖x‖ := norm_pos_iff.mpr htriv
-      have hnt_star : 0 < ‖x⋆‖ :=
-        norm_pos_iff.mpr ((AddEquiv.map_ne_zero_iff starAddEquiv (M := E)).mpr htriv)
-      have h₁ :=
-        calc
-          ‖x‖ * ‖x‖ = ‖x⋆ * x‖ := norm_star_mul_self.symm
-          _ ≤ ‖x⋆‖ * ‖x‖ := norm_mul_le _ _
-      have h₂ :=
-        calc
-          ‖x⋆‖ * ‖x⋆‖ = ‖x * x⋆‖ := by rw [← norm_star_mul_self, star_star]
-          _ ≤ ‖x‖ * ‖x⋆‖ := norm_mul_le _ _
-      exact le_antisymm (le_of_mul_le_mul_right h₂ hnt_star) (le_of_mul_le_mul_right h₁ hnt)⟩
+      have h₁ : ∀ z : E, ‖z⋆ * z‖ ≤ ‖z⋆‖ * ‖z‖ := fun z => norm_mul_le z⋆ z
+      have h₂ : ∀ z : E, 0 < ‖z‖ → ‖z‖ ≤ ‖z⋆‖ := fun z hz => by
+        rw [← mul_le_mul_right hz]; exact (CstarRing.norm_mul_self_le z).trans (h₁ z)
+      have h₃ : ‖x⋆‖ ≤ ‖x‖ := by
+        conv_rhs => rw [← star_star x]
+        exact h₂ x⋆ (gt_of_ge_of_gt (h₂ x hnt) hnt)
+      exact le_antisymm h₃ (h₂ x hnt)⟩
 #align cstar_ring.to_normed_star_group CstarRing.to_normedStarGroup
 
+theorem norm_star_mul_self {x : E} : ‖x⋆ * x‖ = ‖x‖ * ‖x‖ :=
+  le_antisymm ((norm_mul_le _ _).trans (by rw [norm_star])) (CstarRing.norm_mul_self_le x)
+#align cstar_ring.norm_star_mul_self CstarRing.norm_star_mul_self
+
 theorem norm_self_mul_star {x : E} : ‖x * x⋆‖ = ‖x‖ * ‖x‖ := by
   nth_rw 1 [← star_star x]
   simp only [norm_star_mul_self, norm_star]
@@ -167,19 +170,16 @@ instance _root_.Pi.starRing' : StarRing (∀ i, R i) :=
 variable [Fintype ι] [∀ i, CstarRing (R i)]
 
 instance _root_.Prod.cstarRing : CstarRing (R₁ × R₂) where
-  norm_star_mul_self {x} := by
+  norm_mul_self_le x := by
     dsimp only [norm]
     simp only [Prod.fst_mul, Prod.fst_star, Prod.snd_mul, Prod.snd_star, norm_star_mul_self, ← sq]
-    refine le_antisymm ?_ ?_
-    · refine max_le ?_ ?_ <;> rw [sq_le_sq, abs_of_nonneg (norm_nonneg _)]
-      · exact (le_max_left _ _).trans (le_abs_self _)
-      · exact (le_max_right _ _).trans (le_abs_self _)
-    · rw [le_sup_iff]
-      rcases le_total ‖x.fst‖ ‖x.snd‖ with (h | h) <;> simp [h]
+    rw [le_sup_iff]
+    rcases le_total ‖x.fst‖ ‖x.snd‖ with (h | h) <;> simp [h]
 #align prod.cstar_ring Prod.cstarRing
 
 instance _root_.Pi.cstarRing : CstarRing (∀ i, R i) where
-  norm_star_mul_self {x} := by
+  norm_mul_self_le x := by
+    refine le_of_eq (Eq.symm ?_)
     simp only [norm, Pi.mul_apply, Pi.star_apply, nnnorm_star_mul_self, ← sq]
     norm_cast
     exact
@@ -315,7 +315,7 @@ instance toNormedAlgebra {𝕜 A : Type*} [NormedField 𝕜] [StarRing 𝕜] [Se
 
 instance to_cstarRing {R A} [CommRing R] [StarRing R] [NormedRing A] [StarRing A] [CstarRing A]
     [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) : CstarRing S where
-  norm_star_mul_self {x} := @CstarRing.norm_star_mul_self A _ _ _ x
+  norm_mul_self_le x := @CstarRing.norm_mul_self_le A _ _ _ x
 #align star_subalgebra.to_cstar_ring StarSubalgebra.to_cstarRing
 
 end StarSubalgebra

Mathlib/Analysis/NormedSpace/Star/Matrix.lean

@@ -272,7 +272,7 @@ scoped[Matrix.L2OpNorm] attribute [instance] Matrix.instL2OpNormedAlgebra
 /-- The operator norm on `Matrix n n 𝕜` given by the identification with (continuous) linear
 endmorphisms of `EuclideanSpace 𝕜 n` makes it into a `L2OpRing`. -/
 lemma instCstarRing : CstarRing (Matrix n n 𝕜) where
-  norm_star_mul_self := l2_opNorm_conjTranspose_mul_self _
+  norm_mul_self_le M := le_of_eq <| Eq.symm <| l2_opNorm_conjTranspose_mul_self M
 
 scoped[Matrix.L2OpNorm] attribute [instance] Matrix.instCstarRing
 

Mathlib/Analysis/NormedSpace/Star/Multiplier.lean

@@ -673,7 +673,7 @@ variable [NonUnitalNormedRing A] [StarRing A] [CstarRing A]
 variable [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [StarModule 𝕜 A]
 
 instance instCstarRing : CstarRing 𝓜(𝕜, A) where
-  norm_star_mul_self := @fun (a : 𝓜(𝕜, A)) => congr_arg ((↑) : ℝ≥0 → ℝ) <|
+  norm_mul_self_le := fun (a : 𝓜(𝕜, A)) => le_of_eq <| Eq.symm <| congr_arg ((↑) : ℝ≥0 → ℝ) <|
     show ‖star a * a‖₊ = ‖a‖₊ * ‖a‖₊ by
     /- The essence of the argument is this: let `a = (L,R)` and recall `‖a‖ = ‖L‖`.
     `star a = (star ∘ R ∘ star, star ∘ L ∘ star)`. Then for any `x y : A`, we have

Mathlib/Analysis/NormedSpace/Star/Unitization.lean

@@ -127,7 +127,7 @@ variable {𝕜}
 
 /-- The norm on `Unitization 𝕜 E` satisfies the C⋆-property -/
 instance Unitization.instCstarRing : CstarRing (Unitization 𝕜 E) where
-  norm_star_mul_self {x} := by
+  norm_mul_self_le x := by
     -- rewrite both sides as a `⊔`
     simp only [Unitization.norm_def, Prod.norm_def, ← sup_eq_max]
     -- Show that `(Unitization.splitMul 𝕜 E x).snd` satisifes the C⋆-property, in two stages:

Mathlib/Analysis/NormedSpace/lpSpace.lean

@@ -829,18 +829,11 @@ instance inftyStarRing : StarRing (lp B ∞) :=
 #align lp.infty_star_ring lp.inftyStarRing
 
 instance inftyCstarRing [∀ i, CstarRing (B i)] : CstarRing (lp B ∞) where
-  norm_star_mul_self := by
-    intro f
-    apply le_antisymm
-    · rw [← sq]
-      refine lp.norm_le_of_forall_le (sq_nonneg ‖f‖) fun i => ?_
-      simp only [lp.star_apply, CstarRing.norm_star_mul_self, ← sq, infty_coeFn_mul, Pi.mul_apply]
-      refine sq_le_sq' ?_ (lp.norm_apply_le_norm ENNReal.top_ne_zero _ _)
-      linarith [norm_nonneg (f i), norm_nonneg f]
-    · rw [← sq, ← Real.le_sqrt (norm_nonneg _) (norm_nonneg _)]
-      refine lp.norm_le_of_forall_le ‖star f * f‖.sqrt_nonneg fun i => ?_
-      rw [Real.le_sqrt (norm_nonneg _) (norm_nonneg _), sq, ← CstarRing.norm_star_mul_self]
-      exact lp.norm_apply_le_norm ENNReal.top_ne_zero (star f * f) i
+  norm_mul_self_le f := by
+    rw [← sq, ← Real.le_sqrt (norm_nonneg _) (norm_nonneg _)]
+    refine lp.norm_le_of_forall_le ‖star f * f‖.sqrt_nonneg fun i => ?_
+    rw [Real.le_sqrt (norm_nonneg _) (norm_nonneg _), sq, ← CstarRing.norm_star_mul_self]
+    exact lp.norm_apply_le_norm ENNReal.top_ne_zero (star f * f) i
 #align lp.infty_cstar_ring lp.inftyCstarRing
 
 end StarRing

Mathlib/Analysis/Quaternion.lean

@@ -101,7 +101,8 @@ noncomputable instance : NormedAlgebra ℝ ℍ where
   toAlgebra := Quaternion.algebra
 
 instance : CstarRing ℍ where
-  norm_star_mul_self {x} := (norm_mul _ _).trans <| congr_arg (· * ‖x‖) (norm_star x)
+  norm_mul_self_le x :=
+    le_of_eq <| Eq.symm <| (norm_mul _ _).trans <| congr_arg (· * ‖x‖) (norm_star x)
 
 /-- Coercion from `ℂ` to `ℍ`. -/
 @[coe] def coeComplex (z : ℂ) : ℍ := ⟨z.re, z.im, 0, 0⟩

Mathlib/Analysis/RCLike/Basic.lean

@@ -624,7 +624,7 @@ theorem norm_conj {z : K} : ‖conj z‖ = ‖z‖ := by simp only [← sqrt_nor
 #align is_R_or_C.norm_conj RCLike.norm_conj
 
 instance (priority := 100) : CstarRing K where
-  norm_star_mul_self {x} := (norm_mul _ _).trans <| congr_arg (· * ‖x‖) norm_conj
+  norm_mul_self_le x := le_of_eq <| ((norm_mul _ _).trans <| congr_arg (· * ‖x‖) norm_conj).symm
 
 /-! ### Cast lemmas -/
 

Mathlib/Topology/ContinuousFunction/Bounded.lean

@@ -1531,19 +1531,11 @@ instance instStarRing [NormedStarGroup β] : StarRing (α →ᵇ β) where
 variable [CstarRing β]
 
 instance instCstarRing : CstarRing (α →ᵇ β) where
-  norm_star_mul_self {f} := by
-    refine le_antisymm ?_ ?_
-    · rw [← sq, norm_le (sq_nonneg _)]
-      dsimp [star_apply]
-      intro x
-      rw [CstarRing.norm_star_mul_self, ← sq]
-      refine sq_le_sq' ?_ ?_
-      · linarith [norm_nonneg (f x), norm_nonneg f]
-      · exact norm_coe_le_norm f x
-    · rw [← sq, ← Real.le_sqrt (norm_nonneg _) (norm_nonneg _), norm_le (Real.sqrt_nonneg _)]
-      intro x
-      rw [Real.le_sqrt (norm_nonneg _) (norm_nonneg _), sq, ← CstarRing.norm_star_mul_self]
-      exact norm_coe_le_norm (star f * f) x
+  norm_mul_self_le f := by
+    rw [← sq, ← Real.le_sqrt (norm_nonneg _) (norm_nonneg _), norm_le (Real.sqrt_nonneg _)]
+    intro x
+    rw [Real.le_sqrt (norm_nonneg _) (norm_nonneg _), sq, ← CstarRing.norm_star_mul_self]
+    exact norm_coe_le_norm (star f * f) x
 
 end CstarRing
 

Mathlib/Topology/ContinuousFunction/Compact.lean

@@ -530,20 +530,12 @@ variable {α : Type*} {β : Type*}
 variable [TopologicalSpace α] [NormedRing β] [StarRing β]
 
 instance [CompactSpace α] [CstarRing β] : CstarRing C(α, β) where
-  norm_star_mul_self {f} := by
-    refine le_antisymm ?_ ?_
-    · rw [← sq, ContinuousMap.norm_le _ (sq_nonneg _)]
-      intro x
-      simp only [ContinuousMap.coe_mul, coe_star, Pi.mul_apply, Pi.star_apply,
-        CstarRing.norm_star_mul_self, ← sq]
-      refine sq_le_sq' ?_ ?_
-      · linarith [norm_nonneg (f x), norm_nonneg f]
-      · exact ContinuousMap.norm_coe_le_norm f x
-    · rw [← sq, ← Real.le_sqrt (norm_nonneg _) (norm_nonneg _),
-        ContinuousMap.norm_le _ (Real.sqrt_nonneg _)]
-      intro x
-      rw [Real.le_sqrt (norm_nonneg _) (norm_nonneg _), sq, ← CstarRing.norm_star_mul_self]
-      exact ContinuousMap.norm_coe_le_norm (star f * f) x
+  norm_mul_self_le f := by
+    rw [← sq, ← Real.le_sqrt (norm_nonneg _) (norm_nonneg _),
+      ContinuousMap.norm_le _ (Real.sqrt_nonneg _)]
+    intro x
+    rw [Real.le_sqrt (norm_nonneg _) (norm_nonneg _), sq, ← CstarRing.norm_star_mul_self]
+    exact ContinuousMap.norm_coe_le_norm (star f * f) x
 
 end CstarRing
 

Mathlib/Topology/ContinuousFunction/ZeroAtInfty.lean

@@ -597,7 +597,7 @@ end StarRing
 section CstarRing
 
 instance instCstarRing [NonUnitalNormedRing β] [StarRing β] [CstarRing β] : CstarRing C₀(α, β) where
-  norm_star_mul_self {f} := CstarRing.norm_star_mul_self (x := f.toBCF)
+  norm_mul_self_le f := CstarRing.norm_mul_self_le (x := f.toBCF)
 
 end CstarRing