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.

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.

@[implicit_reducible]

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.

theorem OrderHomClass.of_addMonoidHom {F' : Type u_5} {E₁' : Type u_6} {E₂' : Type u_7} [FunLike F' E₁' E₂'] [AddGroup E₁'] [LE E₁'] [AddRightMono E₁'] [AddGroup E₂'] [LE E₂'] [AddRightMono E₂'] [AddMonoidHomClass F' E₁' E₂'] (h : ∀ (f : F') (x : E₁'), 0 ≤ x → 0 ≤ f x) : OrderHomClass F' E₁' E₂'

An additive group homomorphism that maps nonnegative elements to nonnegative elements is an order homomorphism.

@[implicit_reducible]

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₂

theorem PositiveLinearMap.ext {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 g : E₁ →ₚ[R] E₂} (h : ∀ (x : E₁), f x = g x) : f = g

theorem PositiveLinearMap.ext_iff {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 g : E₁ →ₚ[R] E₂} : f = g ↔ ∀ (x : E₁), f x = g x

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

@[simp]

theorem PositiveLinearMap.coe_toLinearMap {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₂) : ⇑f.toLinearMap = ⇑f

theorem PositiveLinearMap.toLinearMap_injective {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₂] : Function.Injective toLinearMap

@[simp]

theorem PositiveLinearMap.toLinearMap_inj {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 g : E₁ →ₚ[R] E₂} : f.toLinearMap = g.toLinearMap ↔ f = g

@[implicit_reducible]

instance PositiveLinearMap.instZero {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₂] : Zero (E₁ →ₚ[R] E₂)

@[simp]

theorem PositiveLinearMap.toLinearMap_zero {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₂] : toLinearMap 0 = 0

@[simp]

theorem PositiveLinearMap.zero_apply {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₂] (x : E₁) : 0 x = 0

@[implicit_reducible]

instance PositiveLinearMap.instAdd {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₂] [IsOrderedAddMonoid E₂] : Add (E₁ →ₚ[R] E₂)

@[simp]

theorem PositiveLinearMap.toLinearMap_add {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₂] [IsOrderedAddMonoid E₂] (f g : E₁ →ₚ[R] E₂) : (f + g).toLinearMap = f.toLinearMap + g.toLinearMap

@[simp]

theorem PositiveLinearMap.add_apply {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₂] [IsOrderedAddMonoid E₂] (f g : E₁ →ₚ[R] E₂) (x : E₁) : (f + g) x = f x + g x

@[implicit_reducible]

instance PositiveLinearMap.instSMulNat {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₂] [IsOrderedAddMonoid E₂] : SMul ℕ (E₁ →ₚ[R] E₂)

@[simp]

theorem PositiveLinearMap.toLinearMap_nsmul {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₂] [IsOrderedAddMonoid E₂] (f : E₁ →ₚ[R] E₂) (n : ℕ) : (n • f).toLinearMap = n • f.toLinearMap

@[simp]

theorem PositiveLinearMap.nsmul_apply {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₂] [IsOrderedAddMonoid E₂] (f : E₁ →ₚ[R] E₂) (n : ℕ) (x : E₁) : (n • f) x = n • f x

@[implicit_reducible]

instance PositiveLinearMap.instAddCommMonoid {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₂] [IsOrderedAddMonoid E₂] : AddCommMonoid (E₁ →ₚ[R] E₂)

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