BanLat/Operators/Regular.lean

All source files · Download exact source

SHA-256: 67f3f9dff27a45c5c3b914051a69c45b5af8c23efa1154ac33e8609af74828fb

1/-2Authors: David Muñoz-Lahoz3-/45import BanLat.Operators.OrderBounded6import BanLat.OrderComplete78/-!9# Regular operators1011An operator between vector lattices is **regular** (`IsRegularOp`) if it can12be written as the difference of two positive operators. Every regular operator13is order bounded; when the codomain is order complete, the converse holds.14-/1516variable {X Y : Type*} [AddCommGroup X] [AddCommGroup Y]17  [Lattice X] [Lattice Y] [IsOrderedAddMonoid X]18  [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y]1920/-- A linear map is **regular** if it is the difference of two positive21operators. -/22def IsRegularOp (f : X →ₗ[ℝ] Y) : Prop :=23  ∃ g h : X →ₗ[ℝ] Y, Positive g ∧ Positive h ∧ f = g - h2425namespace IsRegularOp2627/-- Every regular operator is order bounded. -/28theorem isOrderBounded {f : X →ₗ[ℝ] Y}29    (hf : IsRegularOp f) : IsOrderBounded f := by30  obtain ⟨g, h, hg, hh, rfl⟩ := hf31  exact IsOrderBounded.sub32    (Positive.isOrderBounded hg) (Positive.isOrderBounded hh)3334end IsRegularOp35