Order adherence

Shared definitions and results about order convergence, unbounded-order convergence, solid hulls, and iterated order adherence used throughout the formalization.

def OrderClosures.UOConvergesTo {X : Type u} [AddCommGroup X] [Lattice X] {ι : Type v} [Preorder ι] (f : ι → X) (x : X) : Prop

Unbounded-order convergence, defined using BanLat's OrderConvergesTo.

Equations

• OrderClosures.UOConvergesTo f x = ∀ (a : X), 0 ≤ a → OrderConvergesTo (fun (i : ι) => |f i - x| ⊓ a) 0

def OrderClosures.orderAdherence {X : Type u} [AddCommGroup X] [Lattice X] (A : Set X) : Set X

The order adherence of a set: limits of order-convergent nets in the set.

Equations

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

def OrderClosures.uoAdherence {X : Type u} [AddCommGroup X] [Lattice X] (A : Set X) : Set X

The unbounded-order adherence of a set.

Equations

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

def OrderClosures.IsOrderClosed {X : Type u} [AddCommGroup X] [Lattice X] (A : Set X) : Prop

A set is order closed when it contains the order limits of all its nets.

Equations

• OrderClosures.IsOrderClosed A = (OrderClosures.orderAdherence A ⊆ A)

def OrderClosures.IsUOClosed {X : Type u} [AddCommGroup X] [Lattice X] (A : Set X) : Prop

A set is unbounded-order closed when it contains the uo-limits of all its nets.

Equations

• OrderClosures.IsUOClosed A = (OrderClosures.uoAdherence A ⊆ A)

def OrderClosures.orderClosure {X : Type u} [AddCommGroup X] [Lattice X] (A : Set X) : Set X

The least order-closed set containing A.

Equations

• OrderClosures.orderClosure A = ⋂₀ {B : Set X | A ⊆ B ∧ OrderClosures.IsOrderClosed B}

def OrderClosures.directedPositiveAdherence {X : Type u} [AddCommGroup X] [Lattice X] (A : Set X) : Set X

The paper's directed-supremum description of the positive part of order adherence.

Equations

• OrderClosures.directedPositiveAdherence A = {x : X | 0 ≤ x ∧ ∃ B ⊆ A ∩ {y : X | 0 ≤ y}, B.Nonempty ∧ DirectedOn (fun (x1 x2 : X) => x1 ≤ x2) B ∧ IsLUB B x}

def OrderClosures.solidOrderAdherence {X : Type u} [AddCommGroup X] [Lattice X] (A : Set X) : Set X

For a solid set, order adherence is the solid hull of its directed positive suprema.

Equations

• OrderClosures.solidOrderAdherence A = LatticeOrderedAddCommGroup.solidClosure (OrderClosures.directedPositiveAdherence A)

def OrderClosures.iteratedOrderAdherence {X : Type u} [AddCommGroup X] [Lattice X] (A : Set X) : ℕ → Set X

Finite iteration of order adherence.

Equations

• OrderClosures.iteratedOrderAdherence A 0 = A
• OrderClosures.iteratedOrderAdherence A n.succ = OrderClosures.orderAdherence (OrderClosures.iteratedOrderAdherence A n)

structure OrderClosures.OrderAdherenceTower {X : Type u} [AddCommGroup X] [Lattice X] (A : Set X) : Type (u + 1)

A transfinite order-adherence tower. At limit stages it is the union of earlier stages.

• stage : Ordinal.{u} → Set X

  The set reached at each ordinal stage.

• stage_zero : self.stage 0 = A
• stage_succ (ξ : Ordinal.{u}) : self.stage (Order.succ ξ) = orderAdherence (self.stage ξ)
• stage_limit (ξ : Ordinal.{u}) : Order.IsSuccLimit ξ → self.stage ξ = ⋃ (η : ↑(Set.Iio ξ)), self.stage ↑η

def OrderClosures.NeedsOrderAdherenceIterations {X : Type u} [AddCommGroup X] [Lattice X] (A : Set X) (ξ : Ordinal.{u}) : Prop

At least ξ stages are needed when every earlier adherence step is proper.

Equations

• OrderClosures.NeedsOrderAdherenceIterations A ξ = ∃ (T : OrderClosures.OrderAdherenceTower A), ∀ η < ξ, T.stage η ⊂ T.stage (Order.succ η)

theorem OrderClosures.orderAdherence_eq_solidOrderAdherence {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {A : Set X} (hA : LatticeOrderedAddCommGroup.IsSolid A) : orderAdherence A = solidOrderAdherence A

The generic net definition and the directed-positive definition agree for solid sets.

theorem OrderClosures.subset_orderAdherence {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (A : Set X) : A ⊆ orderAdherence A

Order adherence is extensive.

theorem OrderClosures.orderAdherence_mono {X : Type u} [AddCommGroup X] [Lattice X] : Monotone orderAdherence

Order adherence is monotone.

theorem OrderClosures.subset_uoAdherence {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (A : Set X) : A ⊆ uoAdherence A

Uo-adherence is extensive.

theorem OrderClosures.OrderConvergesTo.uoConvergesTo {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {ι : Type v} [Preorder ι] {f : ι → X} {x : X} (h : OrderConvergesTo f x) : UOConvergesTo f x

Order convergence implies unbounded-order convergence.

theorem OrderClosures.orderAdherence_subset_uoAdherence_subset {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {Y : VectorSublattice X} : orderAdherence ↑Y ⊆ uoAdherence ↑Y ∧ uoAdherence ↑Y ⊆ orderAdherence (orderAdherence ↑Y)

Gao--Leung, Lemma 2.1: the two adherences lie within two order-adherence steps.

theorem OrderClosures.uoAdherence_eq_orderClosure_of_isOrderClosed {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {Y : VectorSublattice X} (hY : IsOrderClosed (uoAdherence ↑Y)) : uoAdherence ↑Y = orderClosure ↑Y

If the uo-adherence is order closed, it is the order closure.

theorem OrderClosures.uoAdherence_eq_double_orderAdherence_and_stabilizes {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {Y : VectorSublattice X} (hY : IsOrderClosed (uoAdherence ↑Y)) : uoAdherence ↑Y = orderAdherence (orderAdherence ↑Y) ∧ orderAdherence (orderAdherence (orderAdherence ↑Y)) = orderAdherence (orderAdherence ↑Y)

The remaining equalities and stabilization stated after Gao--Leung Lemma 2.1.

theorem OrderClosures.isSolid_orderAdherence {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {A : Set X} (hA : LatticeOrderedAddCommGroup.IsSolid A) : LatticeOrderedAddCommGroup.IsSolid (orderAdherence A)

The order adherence of a solid set is solid.

@[reducible, inline]

abbrev OrderClosures.solidHull {X : Type u} [AddCommGroup X] [Lattice X] (A : Set X) : Set X

The least solid set containing A, using Mathlib's solid closure.

Equations

• OrderClosures.solidHull A = LatticeOrderedAddCommGroup.solidClosure A

theorem OrderClosures.solidHull_eq_iUnion_Icc {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (A : Set X) : solidHull A = ⋃ a ∈ A, Set.Icc (-|a|) |a|

The interval-union description of the solid hull used in the paper.

noncomputable def OrderClosures.solidGeneratorNumber {X : Type u} [AddCommGroup X] [Lattice X] (S : Set X) : Cardinal.{u}

The least cardinality of a set whose solid hull is S.

Equations

• OrderClosures.solidGeneratorNumber S = sInf {κ : Cardinal.{?u.1} | ∃ (A : Set X), Cardinal.mk ↑A = κ ∧ OrderClosures.solidHull A = S}

def OrderClosures.scaleSet {X : Type u} (a : ℝ) (A : Set X) [SMul ℝ X] : Set X

Scalar dilation of a set.

Equations

• OrderClosures.scaleSet a A = (fun (x : X) => a • x) '' A

def OrderClosures.unitBallFor {X : Type u} (p : X → ℝ) : Set X

A set-theoretic unit ball for a specified real-valued norm.

Equations

• OrderClosures.unitBallFor p = {x : X | p x ≤ 1}

def OrderClosures.IsOrderComplete (X : Type u) [Preorder X] : Prop

Order completeness, stated without installing a second lattice instance.

Equations

• OrderClosures.IsOrderComplete X = ∀ (A : Set X), A.Nonempty → BddAbove A → ∃ (x : X), IsLUB A x

@[reducible]

noncomputable def OrderClosures.conditionallyCompleteLatticeOfIsOrderComplete (X : Type u) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (hX : IsOrderComplete X) : ConditionallyCompleteLattice X

Install BanLat's order-complete lattice structure locally from the paper's set-theoretic order-completeness predicate.

Equations

• OrderClosures.conditionallyCompleteLatticeOfIsOrderComplete X hX = conditionallyCompleteLatticeOfPosSet X ⋯

noncomputable def OrderClosures.densityCharacter (X : Type u) [TopologicalSpace X] : Cardinal.{u}

Density character: the least cardinality of a dense subset.

Equations

• OrderClosures.densityCharacter X = sInf {κ : Cardinal.{?u.1} | ∃ (D : Set X), Dense D ∧ Cardinal.mk ↑D = κ}

structure OrderClosures.PaperLatticeNorm (X : Type u) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [Module ℝ X] : Type u

A real lattice norm recorded independently of the ambient typeclass norm.

• toFun : X → ℝ

  The real-valued lattice norm.

• nonneg (x : X) : 0 ≤ self.toFun x
• eq_zero_iff (x : X) : self.toFun x = 0 ↔ x = 0
• add_le (x y : X) : self.toFun (x + y) ≤ self.toFun x + self.toFun y
• smul (a : ℝ) (x : X) : self.toFun (a • x) = |a| * self.toFun x
• solid {x y : X} : |x| ≤ |y| → self.toFun x ≤ self.toFun y

@[instance_reducible]

instance OrderClosures.instCoeFunPaperLatticeNormForallReal {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [Module ℝ X] : CoeFun (PaperLatticeNorm X) fun (x : PaperLatticeNorm X) => X → ℝ

Allows a bundled paper lattice norm to be applied as a function; used by all subsequent Fatou and norm-comparison statements.

Equations

• OrderClosures.instCoeFunPaperLatticeNormForallReal = { coe := OrderClosures.PaperLatticeNorm.toFun }

def OrderClosures.IsCompleteFor {X : Type u} [AddCommGroup X] (p : X → ℝ) : Prop

Sequential completeness for the metric induced by p.

Equations

• OrderClosures.IsCompleteFor p = ∀ (f : ℕ → X), (∀ ε > 0, ∃ (N : ℕ), ∀ m ≥ N, ∀ n ≥ N, p (f m - f n) < ε) → ∃ (x : X), ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, p (f n - x) < ε

def OrderClosures.HasFatouProperty {X : Type u} [AddCommGroup X] [Lattice X] (p : X → ℝ) : Prop

Fatou's property for a specified lattice norm.

Equations

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

def OrderClosures.HasWeakFatouProperty {X : Type u} [AddCommGroup X] [Lattice X] (p : X → ℝ) (K : ℝ) : Prop

Weak Fatou property with constant K for a specified lattice norm.

Equations

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

def OrderClosures.EquivalentNorms {X : Type u} (p q : X → ℝ) : Prop

Equivalence of two norms through two positive comparison constants.

Equations

• OrderClosures.EquivalentNorms p q = ∃ (c : ℝ) (C : ℝ), 0 < c ∧ 0 < C ∧ ∀ (x : X), c * p x ≤ q x ∧ q x ≤ C * p x

noncomputable def OrderClosures.ambientLatticeNorm {Y : Type u} [NormedAddCommGroup Y] [Lattice Y] [IsOrderedAddMonoid Y] [NormedVectorLattice Y] : PaperLatticeNorm Y

The ambient norm as a paper lattice norm.

Equations

• OrderClosures.ambientLatticeNorm = { toFun := norm, nonneg := ⋯, eq_zero_iff := ⋯, add_le := ⋯, smul := ⋯, solid := ⋯ }