Positive continuous linear maps

This file contains the continuous version of PositiveLinearMap. While positive linear maps between C⋆-algebras are automatically continuous (see PositiveLinearMap.exists_norm_apply_le which leads to an instance of ContinuousLinearMapClass) there are other situations (e.g., in the theory of W⋆-algebras) in which this does not hold and yet we wish to restrict to consider only continuous positive linear maps.

Implementation notes

We do not define PositiveContinuousLinearMapClass to avoid adding a class that mixes order and algebra. One can achieve the same effect by using a combination of ContinuousLinearMapClass and OrderHomClass.

structure PositiveContinuousLinearMap (R : Type u_1) (E₁ : Type u_2) (E₂ : Type u_3) [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [TopologicalSpace E₁] [AddCommMonoid E₂] [PartialOrder E₂] [TopologicalSpace E₂] [Module R E₁] [Module R E₂] extends E₁ →ₚ[R] E₂, E₁ →L[R] E₂ : Type (max u_2 u_3)

A PositiveContinuousLinearMap is a linear map which is both an order homomorphism and continuous. This comes equipped with the notation E₁ →P[R] E₂.

• 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
• cont : Continuous self.toFun

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

Notation for a PositiveContinuousLinearMap.

Equations

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

@[instance_reducible]

instance PositiveContinuousLinearMap.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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] : FunLike (E₁ →P[R] E₂) E₁ E₂

Equations

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

instance PositiveContinuousLinearMap.instContinuousLinearMapClass {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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] : ContinuousLinearMapClass (E₁ →P[R] E₂) R E₁ E₂

instance PositiveContinuousLinearMap.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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] : OrderHomClass (E₁ →P[R] E₂) E₁ E₂

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

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

@[simp]

theorem PositiveContinuousLinearMap.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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] {S : Type u_6} [SMul S E₁] [SMul S E₂] [LinearMap.CompatibleSMul E₁ E₂ S R] (f : E₁ →P[R] E₂) (c : S) (x : E₁) : f (c • x) = c • f x

theorem PositiveContinuousLinearMap.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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] (f : E₁ →P[R] E₂) {x : E₁} (hx : 0 ≤ x) : 0 ≤ f x

def PositiveContinuousLinearMap.ofClass {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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] {F : Type u_6} [FunLike F E₁ E₂] [ContinuousLinearMapClass F R E₁ E₂] [OrderHomClass F E₁ E₂] (f : F) : E₁ →P[R] E₂

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

Equations

• PositiveContinuousLinearMap.ofClass f = { toPositiveLinearMap := PositiveLinearMap.ofClass f, cont := ⋯ }

@[simp]

theorem PositiveContinuousLinearMap.coe_ofClass {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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] {F : Type u_6} [FunLike F E₁ E₂] [ContinuousLinearMapClass F R E₁ E₂] [OrderHomClass F E₁ E₂] (f : F) : ⇑(ofClass f) = ⇑f

@[instance_reducible]

instance PositiveContinuousLinearMap.instCoeContinuousLinearMapId {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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] : Coe (E₁ →P[R] E₂) (E₁ →L[R] E₂)

Equations

• PositiveContinuousLinearMap.instCoeContinuousLinearMapId = { coe := PositiveContinuousLinearMap.toContinuousLinearMap }

@[instance_reducible]

instance PositiveContinuousLinearMap.instCoePositiveLinearMap {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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] : Coe (E₁ →P[R] E₂) (E₁ →ₚ[R] E₂)

Equations

• PositiveContinuousLinearMap.instCoePositiveLinearMap = { coe := PositiveContinuousLinearMap.toPositiveLinearMap }

@[simp]

theorem PositiveContinuousLinearMap.coe_toPositiveLinearMap {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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] (f : E₁ →P[R] E₂) : ⇑f.toPositiveLinearMap = ⇑f

@[simp]

theorem PositiveContinuousLinearMap.coe_toContinuousLinearMap {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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] (f : E₁ →P[R] E₂) : ⇑f.toContinuousLinearMap = ⇑f

theorem PositiveContinuousLinearMap.toPositiveLinearMap_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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] : Function.Injective toPositiveLinearMap

@[simp]

theorem PositiveContinuousLinearMap.toPositiveLinearMap_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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] (f g : E₁ →P[R] E₂) : f.toPositiveLinearMap = g.toPositiveLinearMap ↔ f = g

theorem PositiveContinuousLinearMap.toContinuousLinearMap_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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] : Function.Injective toContinuousLinearMap

theorem PositiveContinuousLinearMap.toContinuousLinearMap_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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] (f g : E₁ →P[R] E₂) : f.toContinuousLinearMap = g.toContinuousLinearMap ↔ f = g

@[instance_reducible]

instance PositiveContinuousLinearMap.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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] : Zero (E₁ →P[R] E₂)

Equations

• PositiveContinuousLinearMap.instZero = { zero := { toPositiveLinearMap := 0, cont := ⋯ } }

@[simp]

theorem PositiveContinuousLinearMap.toPositiveLinearMap_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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] : toPositiveLinearMap 0 = 0

@[simp]

theorem PositiveContinuousLinearMap.toContinuousLinearMap_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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] : toContinuousLinearMap 0 = 0

instance PositiveContinuousLinearMap.instIsZeroApply {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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] : IsZeroApply (E₁ →P[R] E₂) E₁ E₂

def PositiveContinuousLinearMap.id (R : Type u_1) (E₁ : Type u_2) [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [Module R E₁] [TopologicalSpace E₁] : E₁ →P[R] E₁

The identity as a positive continuous linear map.

Equations

• PositiveContinuousLinearMap.id R E₁ = { toPositiveLinearMap := PositiveLinearMap.id R E₁, cont := ⋯ }

@[simp]

theorem PositiveContinuousLinearMap.id_apply (R : Type u_1) (E₁ : Type u_2) [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [Module R E₁] [TopologicalSpace E₁] (x : E₁) : (PositiveContinuousLinearMap.id R E₁) x = x

@[simp]

theorem PositiveContinuousLinearMap.toPositiveLinearMap_id (R : Type u_1) (E₁ : Type u_2) [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [Module R E₁] [TopologicalSpace E₁] : (PositiveContinuousLinearMap.id R E₁).toPositiveLinearMap = PositiveLinearMap.id R E₁

@[simp]

theorem PositiveContinuousLinearMap.toContinuousLinearMap_id {R : Type u_1} {E₁ : Type u_2} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [Module R E₁] [TopologicalSpace E₁] : (PositiveContinuousLinearMap.id R E₁).toContinuousLinearMap = ContinuousLinearMap.id R E₁

def PositiveContinuousLinearMap.comp {R : Type u_1} {E₁ : 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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] [AddCommMonoid E₃] [PartialOrder E₃] [Module R E₃] [TopologicalSpace E₃] (g : E₂ →P[R] E₃) (f : E₁ →P[R] E₂) : E₁ →P[R] E₃

Composition of positive continuous linear maps.

Equations

• g.comp f = { toPositiveLinearMap := g.comp f.toPositiveLinearMap, cont := ⋯ }

@[simp]

theorem PositiveContinuousLinearMap.toPositiveLinearMap_comp {R : Type u_1} {E₁ : 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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] [AddCommMonoid E₃] [PartialOrder E₃] [Module R E₃] [TopologicalSpace E₃] (g : E₂ →P[R] E₃) (f : E₁ →P[R] E₂) : (g.comp f).toPositiveLinearMap = g.comp f.toPositiveLinearMap

@[simp]

theorem PositiveContinuousLinearMap.comp_apply {R : Type u_1} {E₁ : 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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] [AddCommMonoid E₃] [PartialOrder E₃] [Module R E₃] [TopologicalSpace E₃] (g : E₂ →P[R] E₃) (f : E₁ →P[R] E₂) (x : E₁) : (g.comp f) x = g (f x)

@[simp]

theorem PositiveContinuousLinearMap.toContinuousLinearMap_comp {R : Type u_1} {E₁ : 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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] [AddCommMonoid E₃] [PartialOrder E₃] [Module R E₃] [TopologicalSpace E₃] (g : E₂ →P[R] E₃) (f : E₁ →P[R] E₂) : (g.comp f).toContinuousLinearMap = g.toContinuousLinearMap ∘SL f.toContinuousLinearMap

theorem PositiveContinuousLinearMap.comp_assoc {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {E₃ : Type u_4} {E₄ : Type u_5} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] [TopologicalSpace E₁] [TopologicalSpace E₂] [AddCommMonoid E₃] [PartialOrder E₃] [Module R E₃] [TopologicalSpace E₃] [AddCommMonoid E₄] [PartialOrder E₄] [Module R E₄] [TopologicalSpace E₄] (h : E₃ →P[R] E₄) (g : E₂ →P[R] E₃) (f : E₁ →P[R] E₂) : h.comp (g.comp f) = (h.comp g).comp f

@[simp]

theorem PositiveContinuousLinearMap.comp_id {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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] (f : E₁ →P[R] E₂) : f.comp (PositiveContinuousLinearMap.id R E₁) = f

@[simp]

theorem PositiveContinuousLinearMap.id_comp {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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] (f : E₁ →P[R] E₂) : (PositiveContinuousLinearMap.id R E₂).comp f = f

@[simp]

theorem PositiveContinuousLinearMap.zero_comp {R : Type u_1} {E₁ : 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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] [AddCommMonoid E₃] [PartialOrder E₃] [Module R E₃] [TopologicalSpace E₃] (f : E₁ →P[R] E₂) : comp 0 f = 0

@[simp]

theorem PositiveContinuousLinearMap.comp_zero {R : Type u_1} {E₁ : 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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] [AddCommMonoid E₃] [PartialOrder E₃] [Module R E₃] [TopologicalSpace E₃] (f : E₂ →P[R] E₃) : f.comp 0 = 0

@[instance_reducible]

instance PositiveContinuousLinearMap.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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] [IsOrderedAddMonoid E₂] [ContinuousAdd E₂] : Add (E₁ →P[R] E₂)

Equations

• PositiveContinuousLinearMap.instAdd = { add := fun (f g : E₁ →P[R] E₂) => { toPositiveLinearMap := f.toPositiveLinearMap + g.toPositiveLinearMap, cont := ⋯ } }

@[simp]

theorem PositiveContinuousLinearMap.toPositiveLinearMap_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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] [IsOrderedAddMonoid E₂] [ContinuousAdd E₂] (f g : E₁ →P[R] E₂) : (f + g).toPositiveLinearMap = f.toPositiveLinearMap + g.toPositiveLinearMap

@[simp]

theorem PositiveContinuousLinearMap.toContinuousLinearMap_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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] [IsOrderedAddMonoid E₂] [ContinuousAdd E₂] (f g : E₁ →P[R] E₂) : (f + g).toContinuousLinearMap = f.toContinuousLinearMap + g.toContinuousLinearMap

instance PositiveContinuousLinearMap.instIsAddApply {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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] [IsOrderedAddMonoid E₂] [ContinuousAdd E₂] : IsAddApply (E₁ →P[R] E₂) E₁ E₂

@[instance_reducible]

instance PositiveContinuousLinearMap.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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] [IsOrderedAddMonoid E₂] [ContinuousAdd E₂] : SMul ℕ (E₁ →P[R] E₂)

Equations

• PositiveContinuousLinearMap.instSMulNat = { smul := fun (n : ℕ) (f : E₁ →P[R] E₂) => { toPositiveLinearMap := n • f.toPositiveLinearMap, cont := ⋯ } }

@[simp]

theorem PositiveContinuousLinearMap.toPositiveLinearMap_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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] [IsOrderedAddMonoid E₂] [ContinuousAdd E₂] (f : E₁ →P[R] E₂) (n : ℕ) : (n • f).toPositiveLinearMap = n • f.toPositiveLinearMap

@[simp]

theorem PositiveContinuousLinearMap.toContinuousLinearMap_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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] [IsOrderedAddMonoid E₂] [ContinuousAdd E₂] (f : E₁ →P[R] E₂) (n : ℕ) : (n • f).toContinuousLinearMap = n • f.toContinuousLinearMap

instance PositiveContinuousLinearMap.instIsSMulApplyNat {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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] [IsOrderedAddMonoid E₂] [ContinuousAdd E₂] : IsSMulApply ℕ (E₁ →P[R] E₂) E₁ E₂

@[instance_reducible]

instance PositiveContinuousLinearMap.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₂] [TopologicalSpace E₁] [TopologicalSpace E₂] [IsOrderedAddMonoid E₂] [ContinuousAdd E₂] : AddCommMonoid (E₁ →P[R] E₂)

Equations

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

def PositiveContinuousLinearMap.mk₀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommGroup E₁] [PartialOrder E₁] [IsOrderedAddMonoid E₁] [TopologicalSpace E₁] [AddCommGroup E₂] [PartialOrder E₂] [IsOrderedAddMonoid E₂] [TopologicalSpace E₂] [Module R E₁] [Module R E₂] (f : E₁ →L[R] E₂) (hf : ∀ (x : E₁), 0 ≤ x → 0 ≤ f x) : E₁ →P[R] E₂

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

Equations

• PositiveContinuousLinearMap.mk₀ f hf = { toPositiveLinearMap := PositiveLinearMap.mk₀ (↑f) hf, cont := ⋯ }

@[simp]

theorem PositiveContinuousLinearMap.toPositiveLinearMap_mk₀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommGroup E₁] [PartialOrder E₁] [IsOrderedAddMonoid E₁] [TopologicalSpace E₁] [AddCommGroup E₂] [PartialOrder E₂] [IsOrderedAddMonoid E₂] [TopologicalSpace E₂] [Module R E₁] [Module R E₂] (f : E₁ →L[R] E₂) (hf : ∀ (x : E₁), 0 ≤ x → 0 ≤ f x) : (mk₀ f hf).toPositiveLinearMap = PositiveLinearMap.mk₀ (↑f) hf

@[simp]

theorem PositiveContinuousLinearMap.mk₀_apply {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommGroup E₁] [PartialOrder E₁] [IsOrderedAddMonoid E₁] [TopologicalSpace E₁] [AddCommGroup E₂] [PartialOrder E₂] [IsOrderedAddMonoid E₂] [TopologicalSpace E₂] [Module R E₁] [Module R E₂] (f : E₁ →L[R] E₂) (hf : ∀ (x : E₁), 0 ≤ x → 0 ≤ f x) (x : E₁) : (mk₀ f hf) x = f x

@[simp]

theorem PositiveContinuousLinearMap.toContinuousLinearMap_mk₀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommGroup E₁] [PartialOrder E₁] [IsOrderedAddMonoid E₁] [TopologicalSpace E₁] [AddCommGroup E₂] [PartialOrder E₂] [IsOrderedAddMonoid E₂] [TopologicalSpace E₂] [Module R E₁] [Module R E₂] (f : E₁ →L[R] E₂) (hf : ∀ (x : E₁), 0 ≤ x → 0 ≤ f x) : (mk₀ f hf).toContinuousLinearMap = f