feat: the limit of the norm of the evaluation of f at any increasing approximate unit is the norm of f

LeanOA/CStarAlgebra/Extreme.lean

@@ -126,10 +126,6 @@ lemma Unitary.coe_mem_extremePoints_closedUnitBall {A : Type*} [CStarAlgebra A]
 section nonUnital
 variable {A : Type*} [NonUnitalCStarAlgebra A]
 
--- `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric`
-alias quasispectrum.norm_le_norm_of_mem :=
-  NonUnitalIsometricContinuousFunctionalCalculus.norm_quasispectrum_le
-
 theorem star_self_conjugate_eq_self_of_mem_extremePoints_closedUnitBall {a : A}
     (ha : a ∈ extremePoints ℝ (closedBall 0 1)) : a * star a * a = a := by
   /- Suppose `a` is an extreme point of the closed unit ball. Then we want to show that

LeanOA/CStarAlgebra/PositiveLinearFunctional.lean

@@ -1,5 +1,8 @@
+import LeanOA.Mathlib.Analysis.CStarAlgebra.ApproximateUnit
+import LeanOA.Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
 import LeanOA.Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
 import LeanOA.PositiveContinuousLinearMap
+import LeanOA.Ultraweak.SeparatingDual
 import Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
 
 open scoped ComplexOrder
@@ -87,34 +90,54 @@ lemma cauchy_schwarz_mul_star (f : A →ₚ[ℂ] ℂ) (x y : A) :
   simpa using cauchy_schwarz_star_mul f (star x) (star y)
 
 end CauchySchwarz
-
 end PositiveLinearMap
 
-variable {A : Type*} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
-
-set_option backward.isDefEq.respectTransparency false in
-lemma PositiveLinearMap.norm_apply_le (f : A →ₚ[ℂ] ℂ) (x : A) : ‖f x‖ ≤ (f 1).re * ‖x‖ := by
-  have := by simpa [f.preGNS_norm_def, f.preGNS_inner_def] using
-    norm_inner_le_norm (𝕜 := ℂ) (f.toPreGNS 1) (f.toPreGNS x)
-  have hf := Complex.nonneg_iff.mp (f.map_nonneg zero_le_one) |>.1
-  grw [this, ← sq_le_sq₀ (by positivity) (mul_nonneg hf (by positivity))]
-  simp_rw [mul_pow, Real.sq_sqrt hf, sq, mul_assoc, ← sq, Real.sq_sqrt
-    (Complex.nonneg_iff.mp (f.map_nonneg (star_mul_self_nonneg _))).1]
-  refine mul_le_mul_of_nonneg_left ?_ hf
-  have := by simpa [CStarRing.norm_star_mul_self, Algebra.algebraMap_eq_smul_one, ← sq] using
-    f.apply_le_of_isSelfAdjoint _ (.star_mul_self x)
-  convert Complex.le_def.mp this |>.1
-  rw [← Complex.ofReal_pow, Complex.re_ofReal_mul, mul_comm]
-
-theorem PositiveLinearMap.norm_map_one (f : A →ₚ[ℂ] ℂ) : ‖f 1‖ = (f 1).re := by
-  by_cases! Subsingleton A
-  · simp [Subsingleton.eq_zero (1 : A)]
-  exact le_antisymm (by simpa using f.norm_apply_le 1) (Complex.re_le_norm _)
-
-theorem PositiveLinearMap.opNorm_eq_re_map_one (f : A →ₚ[ℂ] ℂ) :
-    ‖f.toContinuousLinearMap‖ = (f 1).re := by
-  refine le_antisymm (f.toContinuousLinearMap.opNorm_le_bound
-    (by simp [← norm_map_one]) f.norm_apply_le) ?_
-  by_cases! Subsingleton A
-  · simp [Subsingleton.eq_zero (1 : A)]
-  simpa [norm_map_one] using f.toContinuousLinearMap.le_opNorm 1
+namespace PositiveContinuousLinearMap
+variable {A : Type*} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
+
+theorem norm_apply_le_sqrt_opNorm_mul (f : A →P[ℂ] ℂ) (x : A) :
+    ‖f x‖ ≤ √‖(f : A →L[ℂ] ℂ)‖ * √‖f (star x * x)‖ := by
+  have hl := CStarAlgebra.increasingApproximateUnit A
+  refine le_of_tendsto ((ContinuousAt.tendsto (by fun_prop)).comp (hl.tendsto_mul_right _)).norm ?_
+  filter_upwards [hl.eventually_nonneg, hl.eventually_norm] with e he1 he2
+  grw [← he1.star_eq, Function.comp_apply, ← f.coe_toPositiveLinearMap,
+    f.toPositiveLinearMap.cauchy_schwarz_star_mul, f.coe_toPositiveLinearMap,
+    ← f.coe_toContinuousLinearMap, f.toContinuousLinearMap.le_opNorm (star e * e),
+    CStarRing.norm_star_mul_self, 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
+  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
+    grw [← f.coe_toContinuousLinearMap, ContinuousLinearMap.le_opNorm, hx, mul_one]
+    grind
+  have h2 : ∀ᶠ x in l, ‖(f : A →L[ℂ] ℂ)‖ - ε / 2 < ‖f x‖ := by
+    obtain ⟨_, ⟨a, ha1, rfl⟩, ha2⟩ := exists_lt_of_lt_csSup (b := ‖(f : A →L[ℂ] ℂ)‖ - ε / 4)
+      ((Metric.nonempty_closedBall (x := 0).mpr zero_le_one).image (‖f ·‖))
+      (by grind [f.toContinuousLinearMap.sSup_unitClosedBall_eq_norm])
+    have h3 : ∀ᶠ x in l, ‖f (x * a)‖ ^ 2 ≤ ‖f x‖ * ‖(f : A →L[ℂ] ℂ)‖ := by
+      filter_upwards [hl.eventually_nonneg, hl.eventually_norm] with x hx1 hx2
+      have : ‖f (star x * x)‖ ≤ ‖f x‖ := by
+        refine CStarAlgebra.norm_le_norm_of_nonneg_of_le (f.map_nonneg (star_mul_self_nonneg _)) ?_
+        exact f.mono <| hx1.star_eq.symm ▸ CStarAlgebra.mul_self_le_of_nonneg_of_norm_le_one hx1 hx2
+      conv_lhs => rw [← hx1.star_eq, ← f.coe_toPositiveLinearMap]
+      grw [f.cauchy_schwarz_star_mul x a, mul_pow, Real.sq_sqrt (norm_nonneg _),
+        Real.sq_sqrt (norm_nonneg _), f.coe_toPositiveLinearMap, this,
+        ← f.coe_toContinuousLinearMap, f.toContinuousLinearMap.le_opNorm (star a * a),
+        CStarRing.norm_star_mul_self, ← mul_assoc]
+      refine mul_le_of_le_one_right (by positivity) ?_
+      grw [mem_closedBall_zero_iff.mp ha1, one_mul]
+    have h4 : ∀ᶠ x in l, ‖(f : A →L[ℂ] ℂ)‖ - ε / 4 < ‖f (x * a)‖ := by
+      refine (Filter.Tendsto.norm ?_).eventually (lt_mem_nhds ha2)
+      exact (ContinuousAt.tendsto (by fun_prop)).comp (hl.tendsto_mul_right a)
+    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 _ _)
+
+end PositiveContinuousLinearMap

LeanOA/Mathlib/Algebra/Order/Module/PositiveLinearMap.lean

@@ -43,6 +43,15 @@ protected def unop : Eᵐᵒᵖ →ₚ[R] E where
 @[simp]
 lemma unop_apply (x : Eᵐᵒᵖ) : PositiveLinearMap.unop (R := R) x = unop x := rfl
 
+variable (R E) in
+/-- The identity as a positive linear map. -/
+@[simps!] protected def id : E →ₚ[R] E where
+  __ := LinearMap.id
+  __ := OrderHom.id
+
+@[simp] lemma toLinearMap_id : (PositiveLinearMap.id R E).toLinearMap = .id := rfl
+@[simp] lemma toOrderHom_id : (PositiveLinearMap.id R E).toOrderHom = .id := rfl
+
 end MulOpposite
 
 section Comp

LeanOA/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean

@@ -18,6 +18,12 @@ lemma nonneg_mem {l : Filter A} (hl : l.IsIncreasingApproximateUnit) :
     {x | 0 ≤ x} ∈ l := by
   simpa using hl.eventually_nonneg
 
+theorem pure_one (A : Type*) [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] :
+    (pure 1 : Filter A).IsIncreasingApproximateUnit where
+  toIsApproximateUnit := .pure_one A
+  eventually_nonneg := by simp
+  eventually_norm := by nontriviality A; simp
+
 end Filter.IsIncreasingApproximateUnit
 
 end ApproximateUnit

LeanOA/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

@@ -17,3 +17,38 @@ lemma CStarAlgebra.dominated_convergence {x y : ι → A} (hx : Summable x)
   refine CStarAlgebra.norm_le_norm_of_nonneg_of_le (t.sum_nonneg fun i _ ↦ (hy_nonneg i)) ?_
   gcongr
   exact h_le _
+
+-- `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric`
+alias quasispectrum.norm_le_norm_of_mem :=
+  NonUnitalIsometricContinuousFunctionalCalculus.norm_quasispectrum_le
+
+open Unitization NNReal CStarAlgebra in
+lemma CStarAlgebra.nnrpow_le_self_of_nonneg_of_norm_le_one {e : A} (he0 : 0 ≤ e) (he1 : ‖e‖ ≤ 1)
+    {n : ℝ≥0} (hn : 1 ≤ n) : e ^ n ≤ e := by
+  have : n ≠ 0 := by aesop
+  conv_rhs => rw [← cfcₙ_id' ℝ e]
+  rw [CFC.nnrpow_eq_cfcₙ_real e, ← sub_nonneg, ← cfcₙ_sub ..]
+  refine cfcₙ_nonneg fun x hx ↦ sub_nonneg.mpr ?_
+  have := quasispectrum.norm_le_norm_of_mem _ hx
+  grw [he1, Real.norm_eq_abs] at this
+  exact Real.rpow_le_self_of_le_one (quasispectrum_nonneg_of_nonneg _ he0 _ hx) (by grind) hn
+
+/-- If `e` is an element of the nonnegative closed unit ball, then `e * e ≤ e`, with equality
+if `e` is an extreme point
+(see `isStarProjection_iff_mem_extremePoints_nonneg_and_mem_closedUnitBall`). -/
+lemma CStarAlgebra.mul_self_le_of_nonneg_of_norm_le_one {e : A} (he0 : 0 ≤ e) (he1 : ‖e‖ ≤ 1) :
+    e * e ≤ e := CFC.nnrpow_two e ▸ nnrpow_le_self_of_nonneg_of_norm_le_one he0 he1 one_le_two
+
+open Unitization NNReal CStarAlgebra in
+lemma CStarAlgebra.self_le_nnrpow_of_nonneg_of_norm_le_one {e : A} (he0 : 0 ≤ e) (he1 : ‖e‖ ≤ 1)
+    {n : ℝ≥0} (hn0 : n ≠ 0) (hn : n ≤ 1) : e ≤ e ^ n := by
+  conv_lhs => rw [← cfcₙ_id' ℝ e]
+  rw [CFC.nnrpow_eq_cfcₙ_real e, ← sub_nonneg, ← cfcₙ_sub ..]
+  refine cfcₙ_nonneg fun x hx ↦ sub_nonneg.mpr ?_
+  have := quasispectrum.norm_le_norm_of_mem _ hx
+  grw [he1, Real.norm_eq_abs] at this
+  exact Real.self_le_rpow_of_le_one (quasispectrum_nonneg_of_nonneg _ he0 _ hx) (by grind) hn
+
+lemma CStarAlgebra.self_le_sqrt_of_nonneg_of_norm_le_one {e : A} (he0 : 0 ≤ e) (he1 : ‖e‖ ≤ 1) :
+    e ≤ CFC.sqrt e :=
+  CFC.sqrt_eq_nnrpow e ▸ self_le_nnrpow_of_nonneg_of_norm_le_one he0 he1 (by simp) (by simp)

LeanOA/Mathlib/Analysis/CStarAlgebra/PositiveLinearMap.lean

@@ -1,15 +1,29 @@
+import LeanOA.PositiveContinuousLinearMap
 import Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
 
 namespace PositiveLinearMap
 variable {A₁ A₂ : Type*} [NonUnitalCStarAlgebra A₁] [NonUnitalCStarAlgebra A₂] [PartialOrder A₁]
   [StarOrderedRing A₁] [PartialOrder A₂] [StarOrderedRing A₂] (f : A₁ →ₚ[ℂ] A₂)
 
-/-- Lift a positive linear map between C⋆-algebras to a continuous linear map. -/
-def toContinuousLinearMap : A₁ →L[ℂ] A₂ := { f with cont := map_continuous f }
+/-- Lift a positive linear map between C⋆-algebras to a positive continuous linear map. -/
+def toPositiveContinuousLinearMap : A₁ →P[ℂ] A₂ where __ := f
+
+@[simp] theorem toPositiveContinuousLinearMap_apply (x : A₁) :
+    f.toPositiveContinuousLinearMap x = f x := rfl
+@[simp] theorem toPositiveContinuousLinearMap_zero :
+    (0 : A₁ →ₚ[ℂ] A₂).toPositiveContinuousLinearMap = 0 := rfl
+@[simp] lemma toPositiveContinuousLinearMap_id :
+    (PositiveLinearMap.id ℂ A₁).toPositiveContinuousLinearMap = .id ℂ A₁ := rfl
 
-@[simp] theorem toContinuousLinearMap_apply (x : A₁) : f.toContinuousLinearMap x = f x := rfl
+-- maybe remove the following?
+/-- Lift a positive linear map between C⋆-algebras to a continuous linear map. -/
+abbrev toContinuousLinearMap : A₁ →L[ℂ] A₂ := f.toPositiveContinuousLinearMap.toContinuousLinearMap
 
+theorem toContinuousLinearMap_apply (x : A₁) : f.toContinuousLinearMap x = f x := rfl
+@[simp] theorem toContinuousLinearMap_zero : (0 : A₁ →ₚ[ℂ] A₂).toContinuousLinearMap = 0 := rfl
 @[simp] theorem toLinearMap_toContinuousLinearMap :
     f.toContinuousLinearMap.toLinearMap = f.toLinearMap := rfl
+@[simp] lemma toContinuousLinearMap_id :
+    (PositiveLinearMap.id ℂ A₁).toContinuousLinearMap = .id ℂ A₁ := rfl
 
 end PositiveLinearMap

LeanOA/PositiveContinuousLinearMap.lean

@@ -61,6 +61,7 @@ notation:25 E " →P[" R:25 "] " F:0 => PositiveContinuousLinearMap R E F
 add_decl_doc PositiveContinuousLinearMap.toContinuousLinearMap
 /-- The `PositiveLinearMap` underlying a `PositiveContinuousLinearMap`. -/
 add_decl_doc PositiveContinuousLinearMap.toPositiveLinearMap
+
 namespace PositiveContinuousLinearMap
 
 section General
@@ -128,6 +129,7 @@ lemma coe_ofClass (f : F) : ⇑(ofClass f) = f := rfl
 
 end ofClass
 
+instance : Coe (E₁ →P[R] E₂) (E₁ →L[R] E₂) := ⟨toContinuousLinearMap⟩
 
 @[simp]
 lemma coe_toPositiveLinearMap (f : E₁ →P[R] E₂) :
@@ -162,6 +164,15 @@ lemma toContinuousLinearMap_zero : (0 : E₁ →P[R] E₂).toContinuousLinearMap
 lemma zero_apply (x : E₁) : (0 : E₁ →P[R] E₂) x = 0 :=
   rfl
 
+variable (R E₁) in
+/-- The identity as a positive continuous linear map. -/
+@[simps!] protected def id : E₁ →P[R] E₁ where __ := PositiveLinearMap.id R E₁
+
+@[simp] lemma toContinuousLinearMap_id :
+    (PositiveContinuousLinearMap.id R E₁).toContinuousLinearMap = .id R E₁ := rfl
+@[simp] lemma toPositiveLinearMap_id :
+    (PositiveContinuousLinearMap.id R E₁).toPositiveLinearMap = .id R E₁ := rfl
+
 variable [IsOrderedAddMonoid E₂] [ContinuousAdd E₂]
 
 instance : Add (E₁ →P[R] E₂) where