Documentation

LeanPool.OrderClosures.BanLat.OrderContinuous.Basic

Order continuous norms — basic theory #

A normed vector lattice has an order continuous norm when every decreasing net of non-negative elements with infimum zero converges to zero in norm. The sequential version is σ-order continuity; equivalently, every increasing positive sequence whose supremum exists converges in norm to that supremum.

This file introduces the σ- and full classes IsSigmaOrderContinuousNorm and IsOrderContinuousNorm, records that the latter is stronger, proves the equivalent sequential characterisations of σ-order continuity, and shows that an order continuous Banach lattice is order complete.

Definitions #

source
class IsSigmaOrderContinuousNorm (X : Type u_2) [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] :
Prop

A normed vector lattice has a σ-order continuous norm if every antitone sequence of non-negative elements with greatest lower bound zero converges to zero in norm.

Instances
    source
    class IsOrderContinuousNorm (X : Type u) [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] :
    Prop

    A normed vector lattice has an order continuous norm if every antitone net of non-negative elements (over a non-empty directed index set) with greatest lower bound zero converges to zero in norm.

    The index set ι is constrained to live in the same universe as X; in applications (e.g. indexing by a subset of X) this is the case.

    Instances
      source
      theorem tendsto_of_orderConvergesTo_of_isOrderContinuousNorm {X : Type u} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] [IsOrderContinuousNorm X] {ι : Type u} [Preorder ι] {x : ι → X} {a : X} (hx : OrderConvergesTo x a) :
      Filter.Tendsto x Filter.atTop (nhds a)

      In a normed vector lattice with order-continuous norm, order convergence of a net implies norm convergence.

      source
      @[instance 100]
      instance IsOrderContinuousNorm.toIsSigmaOrderContinuousNorm {X : Type u} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] [h : IsOrderContinuousNorm X] :
      IsSigmaOrderContinuousNorm X

      An order continuous norm is in particular σ-order continuous.

      Equivalent sequential characterisations #

      source
      theorem IsSigmaOrderContinuousNorm.tendsto_of_monotone_isLUB {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] [IsSigmaOrderContinuousNorm X] {u : ℕ → X} {x : X} (hmono : Monotone u) (hlub : IsLUB (Set.range u) x) :
      Filter.Tendsto u Filter.atTop (nhds x)

      An increasing sequence with a least upper bound converges in norm to that bound.

      source
      theorem IsSigmaOrderContinuousNorm.tendsto_of_antitone_isGLB {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] [IsSigmaOrderContinuousNorm X] {u : ℕ → X} {x : X} (hanti : Antitone u) (hglb : IsGLB (Set.range u) x) :
      Filter.Tendsto u Filter.atTop (nhds x)

      An antitone sequence with a greatest lower bound converges in norm to that bound.

      source
      theorem IsSigmaOrderContinuousNorm.tendsto_of_abs_sub_le_antitone {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] [IsSigmaOrderContinuousNorm X] {u v : ℕ → X} {x : X} (hv_anti : Antitone v) (hv_nn : ∀ (n : ℕ), 0 ≤ v n) (hv_glb : IsGLB (Set.range v) 0) (hle : ∀ (n : ℕ), |u n - x| ≤ v n) :
      Filter.Tendsto u Filter.atTop (nhds x)

      The norm is σ-order continuous: if |u n - x| ≤ v n for an antitone sequence v with inf v = 0, then u n → x in norm.

      source
      theorem IsSigmaOrderContinuousNorm.tendsto_norm_of_monotone_isLUB {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] [IsSigmaOrderContinuousNorm X] {u : ℕ → X} {x : X} (hmono : Monotone u) (hlub : IsLUB (Set.range u) x) :
      Filter.Tendsto (fun (n : ℕ) => ‖u n‖) Filter.atTop (nhds ‖x‖)

      The norm itself is an order continuous function on positive elements: if u n converges in order to x, then ‖u n‖ → ‖x‖.

      Order continuity implies order completeness #

      source
      theorem BanachLattice.le_zero_of_lb_upperBounds_sub {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [IsVLArchimedean X] {A : Set X} (hne : A.Nonempty) (hbd : BddAbove A) {ε : X} (hε : ∀ w ∈ upperBounds A, ∀ a ∈ A, ε ≤ w - a) :
      ε ≤ 0

      Archimedean "gap" lemma. In an Archimedean vector lattice, any common lower bound of all differences w - a with w an upper bound of a nonempty bounded-above set A and a ∈ A must be ≤ 0.

      source
      @[reducible]
      noncomputable def BanachLattice.conditionallyCompleteLatticeOfIsOrderContinuousNorm {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [BanachLattice X] [IsOrderContinuousNorm X] :
      ConditionallyCompleteLattice X

      An order continuous Banach lattice is order complete.

      Equations
      Instances For