Positive linear maps

This file defines positive linear maps as a linear map that is also an order homomorphism.

Notes

More substantial results on positive maps such as their continuity can be found in the Analysis/CStarAlgebra folder.

structure PositiveLinearMap (R : Type u_1) (E₁ : Type u_2) (E₂ : Type u_3) [Semiring R] [OrderedAddCommMonoid E₁] [OrderedAddCommMonoid E₂] [Module R E₁] [Module R E₂] extends E₁ →ₗ[R] E₂, E₁ →o E₂ : Type (max u_2 u_3)

A positive linear map is a linear map that is also an order homomorphism.

• toFun : E₁ → E₂
• map_add' (x y : E₁) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' (m : R) (x : E₁) : self.toFun (m • x) = (RingHom.id R) m • self.toFun x
• monotone' : Monotone self.toFun

def «term_→ₚ[_]_» : Lean.TrailingParserDescr

Notation for a PositiveLinearMap.

Equations

• One or more equations did not get rendered due to their size.

class PositiveLinearMapClass (F : Type u_1) (R : outParam (Type u_2)) (E₁ : Type u_3) (E₂ : Type u_4) [Semiring R] [OrderedAddCommMonoid E₁] [OrderedAddCommMonoid E₂] [Module R E₁] [Module R E₂] [FunLike F E₁ E₂] extends SemilinearMapClass F (RingHom.id R) E₁ E₂, RelHomClass F (fun (x1 x2 : E₁) => x1 ≤ x2) fun (x1 x2 : E₂) => x1 ≤ x2 : Prop

A positive linear map is a linear map that is also an order homomorphism.

• map_add (f : F) (x y : E₁) : f (x + y) = f x + f y
• map_smulₛₗ (f : F) (c : R) (x : E₁) : f (c • x) = (RingHom.id R) c • f x
• map_rel (f : F) {a b : E₁} : a ≤ b → f a ≤ f b

def PositiveLinearMapClass.toPositiveLinearMap {F : Type u_1} {R : Type u_2} {E₁ : Type u_3} {E₂ : Type u_4} [Semiring R] [OrderedAddCommMonoid E₁] [OrderedAddCommMonoid E₂] [Module R E₁] [Module R E₂] [FunLike F E₁ E₂] [PositiveLinearMapClass F R E₁ E₂] (f : F) : E₁ →ₚ[R] E₂

Reinterpret an element of a type of positive linear maps as a positive linear map.

Equations

• PositiveLinearMapClass.toPositiveLinearMap f = { toLinearMap := ↑f, monotone' := ⋯ }

instance PositiveLinearMapClass.instCoeToLinearMap {F : Type u_1} {R : Type u_2} {E₁ : Type u_3} {E₂ : Type u_4} [Semiring R] [OrderedAddCommMonoid E₁] [OrderedAddCommMonoid E₂] [Module R E₁] [Module R E₂] [FunLike F E₁ E₂] [PositiveLinearMapClass F R E₁ E₂] : CoeHead F (E₁ →ₚ[R] E₂)

Reinterpret an element of a type of positive linear maps as a positive linear map.

Equations

• PositiveLinearMapClass.instCoeToLinearMap = { coe := fun (f : F) => PositiveLinearMapClass.toPositiveLinearMap f }

instance PositiveLinearMap.instFunLike {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [OrderedAddCommMonoid E₁] [OrderedAddCommMonoid E₂] [Module R E₁] [Module R E₂] : FunLike (E₁ →ₚ[R] E₂) E₁ E₂

Equations

• PositiveLinearMap.instFunLike = { coe := fun (f : E₁ →ₚ[R] E₂) => f.toFun, coe_injective' := ⋯ }

instance PositiveLinearMap.instPositiveLinearMapClass {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [OrderedAddCommMonoid E₁] [OrderedAddCommMonoid E₂] [Module R E₁] [Module R E₂] : PositiveLinearMapClass (E₁ →ₚ[R] E₂) R E₁ E₂

@[simp]

theorem PositiveLinearMap.map_smul_of_tower {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [OrderedAddCommMonoid E₁] [OrderedAddCommMonoid E₂] [Module R E₁] [Module R E₂] {S : Type u_4} [SMul S E₁] [SMul S E₂] [LinearMap.CompatibleSMul E₁ E₂ S R] (f : E₁ →ₚ[R] E₂) (c : S) (x : E₁) : f (c • x) = c • f x

theorem PositiveLinearMap.map_nonneg {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [OrderedAddCommMonoid E₁] [OrderedAddCommMonoid E₂] [Module R E₁] [Module R E₂] (f : E₁ →ₚ[R] E₂) {x : E₁} (hx : 0 ≤ x) : 0 ≤ f x

def PositiveLinearMap.mk₀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [OrderedAddCommGroup E₁] [OrderedAddCommGroup E₂] [Module R E₁] [Module R E₂] (f : E₁ →ₗ[R] E₂) (hf : ∀ (x : E₁), 0 ≤ x → 0 ≤ f x) : E₁ →ₚ[R] E₂

Define a positive map from a linear map that maps nonnegative elements to nonnegative elements

Equations

• PositiveLinearMap.mk₀ f hf = { toLinearMap := f, monotone' := ⋯ }