Characterization of positive continuous linear functionals on C⋆-algebras

In this file we show that a continuous linear functional f on a non-unital C⋆-algebra is monotone if f tendsto ‖f‖ along any/some approximate unit. Therefore, when the algebra is unital, f is monotone if and only if ‖f‖ = f 1.

theorem PositiveContinuousLinearMap.norm_map_le_sqrt_opNorm_mul {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (f : A →P[ℂ] ℂ) (x : A) : ‖f x‖ ≤ √‖f.toContinuousLinearMap‖ * √‖f (star x * x)‖

theorem PositiveContinuousLinearMap.nnnorm_map_le_sqrt_opNNNorm_mul {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (f : A →P[ℂ] ℂ) (x : A) : ‖f x‖₊ ≤ NNReal.sqrt ‖f.toContinuousLinearMap‖₊ * NNReal.sqrt ‖f (star x * x)‖₊

theorem PositiveContinuousLinearMap.norm_map_sq_le_opNorm_mul {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (f : A →P[ℂ] ℂ) (x : A) : ‖f x‖ ^ 2 ≤ ‖f.toContinuousLinearMap‖ * ‖f (star x * x)‖

theorem PositiveContinuousLinearMap.nnnorm_map_sq_le_opNNNorm_mul {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (f : A →P[ℂ] ℂ) (x : A) : ‖f x‖₊ ^ 2 ≤ ‖f.toContinuousLinearMap‖₊ * ‖f (star x * x)‖₊

theorem PositiveContinuousLinearMap.tendsto_nhds_opNorm {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (f : A →P[ℂ] ℂ) {l : Filter A} (hl : l.IsIncreasingApproximateUnit) : Filter.Tendsto (fun (x : A) => f x) l (nhds ↑‖f.toContinuousLinearMap‖)

theorem PositiveContinuousLinearMap.ofReal_opNorm_eq_map_one {A : Type u_2} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (f : A →P[ℂ] ℂ) : ↑‖f.toContinuousLinearMap‖ = f 1

theorem ContinuousLinearMap.monotone_iff_tendsto_nhds_opNorm {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {f : A →L[ℂ] ℂ} {l : Filter A} (hl : l.IsIncreasingApproximateUnit) : Monotone ⇑f ↔ Filter.Tendsto (fun (x : A) => f x) l (nhds ↑‖f‖)

theorem ContinuousLinearMap.monotone_iff_opNorm_eq_map_one {A : Type u_2} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {f : A →L[ℂ] ℂ} : Monotone ⇑f ↔ ↑‖f‖ = f 1