Positive linear maps

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

Implementation notes

We do not define PositiveLinearMapClass to avoid adding a class that mixes order and algebra. One can achieve the same effect by using a combination of LinearMapClass and OrderHomClass. We nevertheless use the namespace for lemmas using that combination of typeclasses.

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] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder 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.

def PositiveLinearMapClass.toPositiveLinearMap {F : Type u_1} {R : Type u_2} {E₁ : Type u_3} {E₂ : Type u_4} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] [FunLike F E₁ E₂] [LinearMapClass F R E₁ E₂] [OrderHomClass F 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] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] [FunLike F E₁ E₂] [LinearMapClass F R E₁ E₂] [OrderHomClass F 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] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder 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.instLinearMapClass {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] : LinearMapClass (E₁ →ₚ[R] E₂) R E₁ E₂

instance PositiveLinearMap.instOrderHomClass {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] : OrderHomClass (E₁ →ₚ[R] E₂) E₁ E₂

@[simp]

theorem PositiveLinearMap.map_smul_of_tower {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder 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] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder 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] [AddCommGroup E₁] [PartialOrder E₁] [IsOrderedAddMonoid E₁] [AddCommGroup E₂] [PartialOrder E₂] [IsOrderedAddMonoid 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' := ⋯ }