Positive linear maps in C⋆-algebras

This file develops the API for positive linear maps over C⋆-algebras.

Main results

• PositiveLinearMap.exists_norm_apply_le: positive maps are bounded (and therefore continuous) on non-unital C⋆-algebras.

References

• The proof that positive maps are bounded was taken from https://math.stackexchange.com/questions/426487/why-is-every-positive-linear-map-between-c-algebras-bounded

theorem PositiveLinearMap.apply_le_of_isSelfAdjoint {B₁ : Type u_3} {B₂ : Type u_4} [CStarAlgebra B₁] [CStarAlgebra B₂] [PartialOrder B₁] [PartialOrder B₂] [StarOrderedRing B₁] (f : B₁ →ₚ[ℂ] B₂) (x : B₁) (hx : IsSelfAdjoint x) : f x ≤ f ((algebraMap ℝ B₁) ‖x‖)

theorem PositiveLinearMap.norm_apply_le_of_nonneg {B₁ : Type u_3} {B₂ : Type u_4} [CStarAlgebra B₁] [CStarAlgebra B₂] [PartialOrder B₁] [PartialOrder B₂] [StarOrderedRing B₁] [StarOrderedRing B₂] (f : B₁ →ₚ[ℂ] B₂) (x : B₁) (hx : 0 ≤ x) : ‖f x‖ ≤ ‖f 1‖ * ‖x‖

theorem PositiveLinearMap.exists_norm_apply_le {A₁ : Type u_1} {A₂ : Type u_2} [NonUnitalCStarAlgebra A₁] [NonUnitalCStarAlgebra A₂] [PartialOrder A₁] [StarOrderedRing A₁] [PartialOrder A₂] [StarOrderedRing A₂] (f : A₁ →ₚ[ℂ] A₂) : ∃ (C : NNReal), ∀ (a : A₁), ‖f a‖ ≤ ↑C * ‖a‖

If f is a positive map, then it is bounded (and therefore continuous).

instance PositiveLinearMap.instContinuousLinearMapClassComplexOfLinearMapClassOfOrderHomClass {A₁ : Type u_1} {A₂ : Type u_2} [NonUnitalCStarAlgebra A₁] [NonUnitalCStarAlgebra A₂] [PartialOrder A₁] [StarOrderedRing A₁] [PartialOrder A₂] [StarOrderedRing A₂] {F : Type u_5} [FunLike F A₁ A₂] [LinearMapClass F ℂ A₁ A₂] [OrderHomClass F A₁ A₂] : ContinuousLinearMapClass F ℂ A₁ A₂