Positive operators

A linear map between vector lattices is positive if it sends non-negative elements to non-negative elements. For linear maps, positivity is equivalent to monotonicity, and a positive operator satisfies |f x| ≤ f |x|.

The extension lemma shows that an additive map on the positive cone extends uniquely to a positive linear operator when the codomain is Archimedean. Finally, every positive operator from a Banach lattice to a normed vector lattice is automatically continuous.

Definition and basic properties

def Positive {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] (f : X →ₗ[ℝ] Y) : Prop

A linear map is positive if it sends non-negative elements to non-negative elements.

Equations

• Positive f = ∀ (x : X), 0 ≤ x → 0 ≤ f x

theorem Positive.monotone_iff {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] {f : X →ₗ[ℝ] Y} : Monotone ⇑f ↔ Positive f

For a linear map between vector lattices, monotonicity and positivity are equivalent.

theorem Positive.abs_le_map_abs {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] {f : X →ₗ[ℝ] Y} (hf : Positive f) (x : X) : |f x| ≤ f |x|

A positive operator satisfies |f x| ≤ f |x|.

Order on linear operators

The space X →ₗ[ℝ] Y of linear operators between vector lattices is partially ordered by T ≤ S ↔ Positive (S - T), equivalently T x ≤ S x for every 0 ≤ x. Under this order, 0 ≤ T is the same as Positive T.

@[instance_reducible]

instance Positive.instLELinearMapRealId {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] : LE (X →ₗ[ℝ] Y)

Equations

• Positive.instLELinearMapRealId = { le := fun (T S : X →ₗ[ℝ] Y) => Positive (S - T) }

theorem Positive.le_def {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] {T S : X →ₗ[ℝ] Y} : T ≤ S ↔ Positive (S - T)

theorem Positive.le_iff {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] {T S : X →ₗ[ℝ] Y} : T ≤ S ↔ ∀ (x : X), 0 ≤ x → T x ≤ S x

@[simp]

theorem Positive.zero_le_iff {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] {T : X →ₗ[ℝ] Y} : 0 ≤ T ↔ Positive T

@[instance_reducible]

instance Positive.instPartialOrderLinearMapRealId {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] : PartialOrder (X →ₗ[ℝ] Y)

Equations

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

Extension from the positive cone

theorem Positive.extFun_add {X : Type u_3} {Y : Type u_4} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [IsOrderedAddMonoid X] {τ : X → Y} (hτ_add : ∀ (x y : X), 0 ≤ x → 0 ≤ y → τ (x + y) = τ x + τ y) (x y : X) : τ (x + y)⁺ - τ (x + y)⁻ = τ x⁺ - τ x⁻ + (τ y⁺ - τ y⁻)

noncomputable def Positive.extension {X : Type u_3} {Y : Type u_4} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] [IsVLArchimedean Y] {τ : X → Y} (hτ_nn : ∀ (x : X), 0 ≤ x → 0 ≤ τ x) (hτ_add : ∀ (x y : X), 0 ≤ x → 0 ≤ y → τ (x + y) = τ x + τ y) : X →ₗ[ℝ] Y

Extension Lemma: an additive map on the positive cone of a vector lattice extends to a unique positive linear operator when the codomain is Archimedean. The extension satisfies T x = τ x⁺ − τ x⁻.

Equations

• Positive.extension hτ_nn hτ_add = { toFun := fun (x : X) => τ x⁺ - τ x⁻, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Positive.extension_apply {X : Type u_3} {Y : Type u_4} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] [IsVLArchimedean Y] {τ : X → Y} (hτ_nn : ∀ (x : X), 0 ≤ x → 0 ≤ τ x) (hτ_add : ∀ (x y : X), 0 ≤ x → 0 ≤ y → τ (x + y) = τ x + τ y) (x : X) : (extension hτ_nn hτ_add) x = τ x⁺ - τ x⁻

theorem Positive.extension_nonneg {X : Type u_3} {Y : Type u_4} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] [IsVLArchimedean Y] {τ : X → Y} (hτ_nn : ∀ (x : X), 0 ≤ x → 0 ≤ τ x) (hτ_add : ∀ (x y : X), 0 ≤ x → 0 ≤ y → τ (x + y) = τ x + τ y) {x : X} (hx : 0 ≤ x) : (extension hτ_nn hτ_add) x = τ x

theorem Positive.extension_positive {X : Type u_3} {Y : Type u_4} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] [IsVLArchimedean Y] {τ : X → Y} (hτ_nn : ∀ (x : X), 0 ≤ x → 0 ≤ τ x) (hτ_add : ∀ (x y : X), 0 ≤ x → 0 ≤ y → τ (x + y) = τ x + τ y) : Positive (extension hτ_nn hτ_add)

theorem Positive.extension_unique {X : Type u_3} {Y : Type u_4} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y] [IsVLArchimedean Y] {τ : X → Y} (hτ_nn : ∀ (x : X), 0 ≤ x → 0 ≤ τ x) (hτ_add : ∀ (x y : X), 0 ≤ x → 0 ≤ y → τ (x + y) = τ x + τ y) {f : X →ₗ[ℝ] Y} (hext : ∀ (x : X), 0 ≤ x → f x = τ x) : f = extension hτ_nn hτ_add

The extension is the unique linear operator extending τ on nonnegative elements.

Automatic continuity on Banach lattices

theorem Positive.continuous {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup X] [NormedAddCommGroup Y] [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [BanachLattice X] [NormedVectorLattice Y] {f : X →ₗ[ℝ] Y} (hf : Positive f) : Continuous ⇑f

Every positive linear operator from a Banach lattice to a normed vector lattice is continuous.