Documentation

LeanPool.OrderClosures.BanLat.Convergences.Order

Order convergence #

This file introduces order convergence of nets in a vector lattice. The definition uses a separate directed regulator net decreasing to zero, so the regulator need not have the same index set as the net being controlled.

source
def OrderConvergesTo {X : Type u} [AddCommGroup X] [Lattice X] {ι : Type v} [Preorder ι] (u : ι → X) (x : X) :
Prop

A net u order converges to x if its tails are eventually controlled by a separate decreasing regulator net with greatest lower bound zero.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem orderConvergesTo_const {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {ι : Type v} [Preorder ι] (x : X) :
    OrderConvergesTo (fun (x_1 : ι) => x) x

    A constant net order converges to its constant value.

    source
    theorem orderConvergesTo_of_monotone_isLUB {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {ι : Type v} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] {u : ι → X} {x : X} (hmono : Monotone u) (hlub : IsLUB (Set.range u) x) :
    OrderConvergesTo u x

    An increasing net order converges to its least upper bound.

    source
    theorem orderConvergesTo_of_antitone_isGLB {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {ι : Type v} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] {u : ι → X} {x : X} (hanti : Antitone u) (hglb : IsGLB (Set.range u) x) :
    OrderConvergesTo u x

    A decreasing net order converges to its greatest lower bound.

    source
    theorem OrderConvergesTo.nonneg {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {ι : Type v} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] {u : ι → X} {x : X} (hu : OrderConvergesTo u x) (hnn : ∀ (i : ι), 0 ≤ u i) :
    0 ≤ x

    The positive cone is order closed: a pointwise non-negative order-convergent net has a non-negative limit.

    source
    theorem OrderConvergesTo.add {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {ι : Type v} [Preorder ι] {u v : ι → X} {x y : X} (hu : OrderConvergesTo u x) (hv : OrderConvergesTo v y) :
    OrderConvergesTo (fun (i : ι) => u i + v i) (x + y)

    Addition is order continuous.

    source
    theorem OrderConvergesTo.neg {X : Type u} [AddCommGroup X] [Lattice X] {ι : Type v} [Preorder ι] {u : ι → X} {x : X} (hu : OrderConvergesTo u x) :
    OrderConvergesTo (fun (i : ι) => -u i) (-x)

    Negation is order continuous.

    source
    theorem OrderConvergesTo.sub {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {ι : Type v} [Preorder ι] {u v : ι → X} {x y : X} (hu : OrderConvergesTo u x) (hv : OrderConvergesTo v y) :
    OrderConvergesTo (fun (i : ι) => u i - v i) (x - y)

    Subtraction is order continuous.

    source
    theorem OrderConvergesTo.le {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {ι : Type v} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] {u v : ι → X} {x y : X} (hu : OrderConvergesTo u x) (hv : OrderConvergesTo v y) (hle : ∀ (i : ι), u i ≤ v i) :
    x ≤ y

    Order limits respect pointwise order between two nets with the same index set.

    source
    theorem OrderConvergesTo.le_of_forall_le {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {ι : Type v} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] {u : ι → X} {x b : X} (hu : OrderConvergesTo u x) (hub : ∀ (i : ι), u i ≤ b) :
    x ≤ b

    If an order-convergent net is pointwise bounded above, then its limit is bounded above by the same bound.

    source
    theorem OrderConvergesTo.forall_le {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {ι : Type v} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] {u : ι → X} {a x : X} (hu : OrderConvergesTo u x) (hau : ∀ (i : ι), a ≤ u i) :
    a ≤ x

    If an order-convergent net is pointwise bounded below, then its limit is bounded below by the same bound.

    source
    theorem OrderConvergesTo.smul {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a : ℝ) {ι : Type v} [Preorder ι] {u : ι → X} {x : X} (hu : OrderConvergesTo u x) :
    OrderConvergesTo (fun (i : ι) => a • u i) (a • x)

    Scalar multiplication is order continuous.

    source
    theorem OrderConvergesTo.sup {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {ι : Type v} [Preorder ι] {u v : ι → X} {x y : X} (hu : OrderConvergesTo u x) (hv : OrderConvergesTo v y) :
    OrderConvergesTo (fun (i : ι) => u i ⊔ v i) (x ⊔ y)

    Supremum is order continuous.

    source
    theorem OrderConvergesTo.inf {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {ι : Type v} [Preorder ι] {u v : ι → X} {x y : X} (hu : OrderConvergesTo u x) (hv : OrderConvergesTo v y) :
    OrderConvergesTo (fun (i : ι) => u i ⊓ v i) (x ⊓ y)

    Infimum is order continuous.

    source
    theorem OrderConvergesTo.abs {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {ι : Type v} [Preorder ι] {u : ι → X} {x : X} (hu : OrderConvergesTo u x) :
    OrderConvergesTo (fun (i : ι) => |u i|) |x|

    Absolute value is order continuous.

    source
    theorem le_of_orderConvergesTo_of_forall_le {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {ι : Type v} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] {u : ι → X} {x b : X} (hu : OrderConvergesTo u x) (hub : ∀ (i : ι), u i ≤ b) :
    x ≤ b

    If an order-convergent net is pointwise bounded above, then its limit is bounded above by the same bound.