chore(Analysis/CStarAlgebra/CFC/Order): relate section to strict positivity (#30694)

Author: themathqueen

Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean

@@ -61,8 +61,7 @@ lemma CFC.monotoneOn_one_sub_one_add_inv :
   rw [h_cfc_one_sub (a : A⁺¹), h_cfc_one_sub (b : A⁺¹)]
   gcongr
   rw [← CFC.rpow_neg_one_eq_cfc_inv, ← CFC.rpow_neg_one_eq_cfc_inv]
-  exact rpow_neg_one_le_rpow_neg_one (add_nonneg zero_le_one ha) (by gcongr) <|
-    isUnit_of_le isUnit_one zero_le_one <| le_add_of_nonneg_right ha
+  exact rpow_neg_one_le_rpow_neg_one (by gcongr)
 
 lemma CFC.monotoneOn_one_sub_one_add_inv_real :
     MonotoneOn (cfcₙ (fun x : ℝ => 1 - (1 + x)⁻¹)) (Set.Ici (0 : A)) := by

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

@@ -262,20 +262,20 @@ open CFC
 
 variable [PartialOrder A] [StarOrderedRing A]
 
--- TODO : relate everything in this section to strict positivity
-
-lemma CFC.conjugate_rpow_neg_one_half {a : A} (h₀ : IsUnit a) (ha : 0 ≤ a := by cfc_tac) :
+lemma CFC.conjugate_rpow_neg_one_half (a : A) (ha : IsStrictlyPositive a := by cfc_tac) :
     a ^ (-(1 / 2) : ℝ) * a * a ^ (-(1 / 2) : ℝ) = 1 := by
-  lift a to Aˣ using h₀
+  lift a to Aˣ using ha.isUnit
   nth_rw 2 [← rpow_one (a : A)]
   simp only [← rpow_add a.isUnit]
   norm_num
   exact rpow_zero _
 
-/-- In a unital C⋆-algebra, if `a` is nonnegative and invertible, and `a ≤ b`, then `b` is
+/-- In a unital C⋆-algebra, if `a` is strictly positive, and `a ≤ b`, then `b` is
 invertible. -/
-lemma CStarAlgebra.isUnit_of_le {a b : A} (h₀ : IsUnit a) (ha : 0 ≤ a := by cfc_tac)
-    (hab : a ≤ b) : IsUnit b := by
+lemma CStarAlgebra.isUnit_of_le (a : A) {b : A} (hab : a ≤ b)
+    (h : IsStrictlyPositive a := by cfc_tac) : IsUnit b := by
+  have h₀ := h.isUnit
+  have ha := h.nonneg
   rw [← spectrum.zero_notMem_iff ℝ≥0] at h₀ ⊢
   nontriviality A
   have hb := (show 0 ≤ a from ha).trans hab
@@ -284,9 +284,10 @@ lemma CStarAlgebra.isUnit_of_le {a b : A} (h₀ : IsUnit a) (ha : 0 ≤ a := by
   peel h₀ with r hr _
   exact this.trans hab
 
-lemma le_iff_norm_sqrt_mul_rpow {a b : A} (hbu : IsUnit b) (ha : 0 ≤ a) (hb : 0 ≤ (b : A)) :
+lemma le_iff_norm_sqrt_mul_rpow (a b : A) (ha : 0 ≤ a := by cfc_tac)
+    (hb : IsStrictlyPositive b := by cfc_tac) :
     a ≤ b ↔ ‖sqrt a * (b : A) ^ (-(1 / 2) : ℝ)‖ ≤ 1 := by
-  lift b to Aˣ using hbu
+  lift b to Aˣ using hb.isUnit
   have hbab : 0 ≤ (b : A) ^ (-(1 / 2) : ℝ) * a * (b : A) ^ (-(1 / 2) : ℝ) :=
     conjugate_nonneg_of_nonneg ha rpow_nonneg
   conv_rhs =>
@@ -298,7 +299,7 @@ lemma le_iff_norm_sqrt_mul_rpow {a b : A} (hbu : IsUnit b) (ha : 0 ≤ a) (hb :
   · calc
       _ ≤ ↑b ^ (-(1 / 2) : ℝ) * (b : A) * ↑b ^ (-(1 / 2) : ℝ) :=
         IsSelfAdjoint.of_nonneg rpow_nonneg |>.conjugate_le_conjugate h
-      _ = 1 := conjugate_rpow_neg_one_half b.isUnit
+      _ = 1 := conjugate_rpow_neg_one_half (b : A)
   · calc
       a = (sqrt ↑b * ↑b ^ (-(1 / 2) : ℝ)) * a * (↑b ^ (-(1 / 2) : ℝ) * sqrt ↑b) := by
         simp only [CFC.sqrt_eq_rpow .., ← CFC.rpow_add b.isUnit]
@@ -312,7 +313,8 @@ lemma le_iff_norm_sqrt_mul_rpow {a b : A} (hbu : IsUnit b) (ha : 0 ≤ a) (hb :
 lemma le_iff_norm_sqrt_mul_sqrt_inv {a : A} {b : Aˣ} (ha : 0 ≤ a) (hb : 0 ≤ (b : A)) :
     a ≤ b ↔ ‖sqrt a * sqrt (↑b⁻¹ : A)‖ ≤ 1 := by
   rw [CFC.sqrt_eq_rpow (a := (↑b⁻¹ : A)), ← CFC.rpow_neg_one_eq_inv b,
-    CFC.rpow_rpow (b : A) _ _ (by simp) (by simp), le_iff_norm_sqrt_mul_rpow b.isUnit ha hb]
+    CFC.rpow_rpow (b : A) _ _ (by simp) (by simp),
+    le_iff_norm_sqrt_mul_rpow a (hb := b.isUnit.isStrictlyPositive hb)]
   simp
 
 namespace CStarAlgebra
@@ -358,21 +360,22 @@ lemma inv_le_one {a : Aˣ} (ha : 1 ≤ a) : (↑a⁻¹ : A) ≤ 1 :=
 lemma le_one_of_one_le_inv {a : Aˣ} (ha : 1 ≤ (↑a⁻¹ : A)) : (a : A) ≤ 1 := by
   simpa using CStarAlgebra.inv_le_one ha
 
-lemma rpow_neg_one_le_rpow_neg_one {a b : A} (ha : 0 ≤ a) (hab : a ≤ b) (hau : IsUnit a) :
+lemma rpow_neg_one_le_rpow_neg_one {a b : A} (hab : a ≤ b)
+    (ha : IsStrictlyPositive a := by cfc_tac) :
     b ^ (-1 : ℝ) ≤ a ^ (-1 : ℝ) := by
-  lift b to Aˣ using isUnit_of_le hau ha hab
-  lift a to Aˣ using hau
-  rw [rpow_neg_one_eq_inv a ha, rpow_neg_one_eq_inv b (ha.trans hab)]
-  exact CStarAlgebra.inv_le_inv ha hab
+  lift b to Aˣ using isUnit_of_le a hab
+  lift a to Aˣ using ha.isUnit
+  rw [rpow_neg_one_eq_inv a, rpow_neg_one_eq_inv b (ha.nonneg.trans hab)]
+  exact CStarAlgebra.inv_le_inv ha.nonneg hab
 
 lemma rpow_neg_one_le_one {a : A} (ha : 1 ≤ a) : a ^ (-1 : ℝ) ≤ 1 := by
-  lift a to Aˣ using isUnit_of_le isUnit_one zero_le_one ha
+  lift a to Aˣ using isUnit_of_le 1 ha
   rw [rpow_neg_one_eq_inv a (zero_le_one.trans ha)]
   exact inv_le_one ha
 
 protected lemma _root_.IsStrictlyPositive.of_le {a b : A} (ha : IsStrictlyPositive a)
     (hab : a ≤ b) : IsStrictlyPositive b :=
-  ⟨ha.nonneg.trans hab, CStarAlgebra.isUnit_of_le ha.isUnit ha.nonneg hab⟩
+  ⟨ha.nonneg.trans hab, CStarAlgebra.isUnit_of_le a hab⟩
 
 theorem _root_.IsStrictlyPositive.add_nonneg {a b : A}
     (ha : IsStrictlyPositive a) (hb : 0 ≤ b) : IsStrictlyPositive (a + b) :=