feat: bounded linear functional is monotone iff ‖f‖ = f 1

LeanOA/CFC.lean

@@ -95,6 +95,16 @@ theorem IsSelfAdjoint.norm_le_max_of_le_of_le {A : Type*} [NonUnitalCStarAlgebra
       (CStarAlgebra.norm_posPart_mono hbc hb)
     _ ≤ max ‖a‖ ‖c‖ := max_le_max (by simp) (by simp)
 
+open CStarAlgebra Unitization in
+lemma CStarAlgebra.norm_sub_le_one_of_nonneg_of_norm_le_one {A : Type*} [NonUnitalCStarAlgebra A]
+    [PartialOrder A] [StarOrderedRing A] {x y : A} (hx : 0 ≤ x) (hx0 : ‖x‖ ≤ 1) (hy : 0 ≤ y)
+    (hy0 : ‖y‖ ≤ 1) : ‖x - y‖ ≤ 1 := by
+  rw [← norm_inr (𝕜 := ℂ), norm_le_one_iff_of_nonneg _] at hx0 hy0
+  rw [← norm_inr (𝕜 := ℂ), inr_sub]
+  simpa [sub_eq_add_neg] using (IsSelfAdjoint.one _).neg.norm_le_max_of_le_of_le
+    (by simpa using add_le_add hx.inr (neg_le_neg_iff.mpr hy0))
+    (add_le_add hx0 (by simpa using neg_le_neg hy.inr : -(y : A⁺¹) ≤ 0))
+
 open scoped ComplexStarModule in
 /-- A set in a non-unital C⋆-algebra which is bounded above and below is
 bounded in norm. -/

LeanOA/CStarAlgebra/Extreme.lean

@@ -257,15 +257,6 @@ theorem CStarAlgebra.isUnital_iff :
   refine ⟨fun h ↦ ⟨1, one_mem_extremePoints_unitClosedBall⟩, fun ⟨x, hx⟩ ↦ ?_⟩
   exact ⟨_, fun y ↦ ⟨ofExtremePtOne_mul hx y, mul_ofExtremePtOne hx y⟩⟩
 
-private lemma CStarAlgebra.norm_sub_le_one_of_nonneg_of_norm_le_one [PartialOrder A]
-    [StarOrderedRing A] {x y : A} (hx : 0 ≤ x) (hx0 : ‖x‖ ≤ 1) (hy : 0 ≤ y) (hy0 : ‖y‖ ≤ 1) :
-    ‖x - y‖ ≤ 1 := by
-  rw [← norm_inr (𝕜 := ℂ), norm_le_one_iff_of_nonneg _] at hx0 hy0
-  rw [← norm_inr (𝕜 := ℂ), inr_sub]
-  simpa [sub_eq_add_neg] using (IsSelfAdjoint.one _).neg.norm_le_max_of_le_of_le
-    (by simpa using add_le_add hx.inr (neg_le_neg_iff.mpr hy0))
-    (add_le_add hx0 (by simpa using neg_le_neg hy.inr : -(y : A⁺¹) ≤ 0))
-
 theorem isStarProjection_posPart_of_mem_extremePoints_isSelfAdjoint_and_mem_unitClosedBall
     {e : A} (he : e ∈ extremePoints ℝ {x | IsSelfAdjoint x ∧ x ∈ closedBall 0 1}) :
     IsStarProjection (e⁺ : A) := by

LeanOA/CStarAlgebra/PositiveLinearFunctional.lean

@@ -7,6 +7,8 @@ public import LeanOA.PositiveContinuousLinearMap
 public import LeanOA.Ultraweak.SeparatingDual
 public import Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
 
+import LeanOA.CFC
+
 @[expose] public section
 
 open scoped ComplexOrder
@@ -109,9 +111,11 @@ theorem norm_apply_le_sqrt_opNorm_mul (f : A →P[ℂ] ℂ) (x : A) :
     ← f.coe_toContinuousLinearMap, f.toContinuousLinearMap.le_opNorm (star e * e),
     CStarRing.norm_star_mul_self, he2, he2, one_mul, mul_one]
 
-open Topology in
-theorem tendsto_isIncreasingApproximateUnit_nhds_opNorm (f : A →P[ℂ] ℂ) {l : Filter A}
-    (hl : l.IsIncreasingApproximateUnit) : l.Tendsto (‖f ·‖) (𝓝 ‖(f : A →L[ℂ] ℂ)‖) := by
+open Topology Complex in
+theorem tendsto_nhds_opNorm (f : A →P[ℂ] ℂ) {l : Filter A} (hl : l.IsIncreasingApproximateUnit) :
+    l.Tendsto (f ·) (𝓝 ‖(f : A →L[ℂ] ℂ)‖) := by
+  suffices l.Tendsto (‖f ·‖) (𝓝 ‖(f : A →L[ℂ] ℂ)‖) from this.ofReal.congr' <| by
+    filter_upwards [hl.eventually_nonneg] using by simp_all [norm_of_nonneg' (f.map_nonneg _)]
   refine Metric.tendsto_nhds.mpr fun ε hε ↦ ?_
   have h : ∀ᶠ x in l, ‖f x‖ ≤ ‖(f : A →L[ℂ] ℂ)‖ + ε / 2 := by
     filter_upwards [hl.eventually_norm] with x hx
@@ -139,9 +143,63 @@ theorem tendsto_isIncreasingApproximateUnit_nhds_opNorm (f : A →P[ℂ] ℂ) {l
     filter_upwards [h3, h4] with x _ _ using by nlinarith [norm_nonneg (f x)]
   filter_upwards [h, h2] using by grind [Real.dist_eq]
 
-theorem opNorm_eq_norm_map_one {A : Type*} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
-    (f : A →P[ℂ] ℂ) : ‖(f : A →L[ℂ] ℂ)‖ = ‖f 1‖ :=
-  tendsto_nhds_unique (f.tendsto_isIncreasingApproximateUnit_nhds_opNorm (.pure_one A))
-    (tendsto_pure_nhds _ _)
+theorem ofReal_opNorm_eq_map_one {A : Type*} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
+    (f : A →P[ℂ] ℂ) : ‖(f : A →L[ℂ] ℂ)‖ = f 1 :=
+  tendsto_nhds_unique (f.tendsto_nhds_opNorm (.pure_one A)) (tendsto_pure_nhds _ _)
 
 end PositiveContinuousLinearMap
+
+namespace ContinuousLinearMap
+variable {A} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {f : A →L[ℂ] ℂ}
+
+open Topology Filter Complex CStarRing
+
+private lemma im_apply_eq_zero_of_tendsto_nhds_opNorm {l : Filter A}
+    (hl : l.IsIncreasingApproximateUnit) (hf : l.Tendsto (f ·) (𝓝 ‖f‖)) {a : A}
+    (ha : IsSelfAdjoint a) : (f a).im = 0 := by
+  by_cases ‖f‖ = 0
+  · simp_all
+  suffices ∀ (t : ℝ), ‖f a + I * t * ‖f‖‖ ^ 2 ≤ ‖f‖ ^ 2 * (‖a‖ ^ 2 + t ^ 2) by
+    contrapose! this
+    refine ⟨(‖f‖ ^ 2 * ‖a‖ ^ 2 - ‖f a‖ ^ 2 + 1) / (2 * (f a).im * ‖f‖), ?_⟩
+    simp [normSq, ← normSq_eq_norm_sq, -ofReal_div]; field_simp; grind
+  intro t
+  suffices (fun x ↦ ‖f (a + (I * t) • x)‖ ^ 2) ≤ᶠ[l]
+        (fun x ↦ ‖f‖ ^ 2 * (‖a‖ ^ 2 + t ^ 2 + |t| * ‖a * x - x * a‖)) by
+    refine le_of_tendsto_of_tendsto (hb := hl.neBot) ?_ ?_ this
+    · simp_rw [map_add, map_smul, smul_eq_mul]
+      apply_rules [Tendsto.pow, Tendsto.norm, Tendsto.const_add, Tendsto.const_mul]
+    · simpa using (hl.tendsto_mul_left a).sub (hl.tendsto_mul_right a)
+        |>.norm |>.const_mul _ |>.const_add _ |>.const_mul _
+  filter_upwards [hl.eventually_isSelfAdjoint, hl.eventually_norm] with x hx hx2
+  grw [f.le_opNorm, mul_pow, mul_le_mul_iff_of_pos_left (by simp_all), sq, ← norm_star_mul_self]
+  calc
+    _ = ‖a * a + (t ^ 2 : ℂ) • (x * x) + (I * t) • (a * x + -(x * a))‖ := by
+      simp [add_mul, mul_add, smul_mul_assoc, mul_smul_comm, smul_smul, mul_mul_mul_comm]
+      grind [sq]
+  _ ≤ ‖a‖ ^ 2 + t ^ 2 + |t| * ‖a * x - x * a‖ := by
+      grw [add_assoc, sq, norm_add_le, norm_add_le, ← sub_eq_add_neg, sq, ← norm_star_mul_self,
+        add_assoc, ha.star_eq, add_le_add_iff_left, norm_smul, norm_mul_le x, hx2, hx2]
+      simp [norm_smul, sq]
+
+theorem monotone_iff_tendsto_nhds_opNorm {l : Filter A} (hl : l.IsIncreasingApproximateUnit) :
+    Monotone f ↔ l.Tendsto (f ·) (𝓝 ‖f‖) := by
+  refine ⟨fun hf ↦ ?_, fun hf ↦ monotone_iff_map_nonneg _ |>.mpr fun a ha ↦ ?_⟩
+  · exact ({ __ := f, monotone' := hf } : _ →P[ℂ] _).tendsto_nhds_opNorm hl
+  by_cases ha0 : a = 0
+  · simp [ha0]
+  suffices 0 ≤ (f (‖a‖⁻¹ • a)).re by simpa [Complex.le_def, ha0,
+    im_apply_eq_zero_of_tendsto_nhds_opNorm hl hf ha.isSelfAdjoint] using this
+  suffices ‖‖f‖ - f (‖a‖⁻¹ • a)‖ ≤ ‖f‖ by grw [← re_le_norm] at this; simpa
+  refine le_of_tendsto (hx := hl.neBot) (hf.sub_const (f _) |>.norm) ?_
+  filter_upwards [hl.eventually_nonneg, hl.eventually_norm] with y hy hy2
+  grw [← map_sub, f.le_opNorm, CStarAlgebra.norm_sub_le_one_of_nonneg_of_norm_le_one hy hy2
+    (by simp [smul_nonneg, ha]) (by simp [norm_smul, ha0]), mul_one]
+
+theorem monotone_iff_opNorm_eq_map_one {A : Type*} [CStarAlgebra A] [PartialOrder A]
+    [StarOrderedRing A] {f : A →L[ℂ] ℂ} : Monotone f ↔ ‖f‖ = f 1 := by
+  rw [f.monotone_iff_tendsto_nhds_opNorm (.pure_one A)]
+  have := tendsto_pure_nhds f 1
+  exact ⟨fun h ↦ tendsto_nhds_unique h this, fun h ↦ by simpa [h]⟩
+
+end ContinuousLinearMap