Documentation

LeanPool.OrderClosures.WeaklyFatou.Reductions

Weakly Fatou norms #

Formalization of the paper's construction of a weakly Fatou Banach lattice norm that is not equivalent to any lattice norm with the Fatou property.

The two reductions #

source
theorem OrderClosures.iteratedOrderAdherence_mono_and_scale {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {A B : Set X} {c : ℝ} (hc : 0 < c) :
(A ⊆ B → ∀ (m : ℕ), iteratedOrderAdherence A m ⊆ iteratedOrderAdherence B m) ∧ orderAdherence (scaleSet c A) = scaleSet c (orderAdherence A) ∧ ∀ (m : ℕ), iteratedOrderAdherence (scaleSet c A) m = scaleSet c (iteratedOrderAdherence A m)

Paper Lemma lem:order-basic.

source
theorem OrderClosures.weakFatou_iterated_unitBall {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (p : PaperLatticeNorm X) {K : ℝ} (hK : HasWeakFatouProperty p.toFun K) (m : ℕ) :
m ≥ 1 → iteratedOrderAdherence (unitBallFor p.toFun) m ⊆ scaleSet (K ^ m) (unitBallFor p.toFun)

Paper Lemma lem:fatou-order, part (a).

source
theorem OrderClosures.fatou_iterated_unitBall {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (p : PaperLatticeNorm X) (hp : HasFatouProperty p.toFun) (m : ℕ) :
m ≥ 1 → iteratedOrderAdherence (unitBallFor p.toFun) m = unitBallFor p.toFun

Paper Lemma lem:fatou-order, part (b).

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

Weak sequential Nakano constant, Definition 3(a) in the paper.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def OrderClosures.IsWeakNakanoConstant {X : Type u} [AddCommGroup X] [Lattice X] (p : X → ℝ) (K : ℝ) :
    Prop

    Weak Nakano constant, Definition 3(b) in the paper.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def OrderClosures.FremlinProperty {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] :
      Prop

      Fremlin's question, as a predicate on a vector lattice: every complete weakly Fatou lattice norm admits an equivalent Fatou lattice norm.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem OrderClosures.weakNakano_of_weakSequentialNakano_p {Y : Type u} [NormedAddCommGroup Y] [Lattice Y] [IsOrderedAddMonoid Y] [NormedVectorLattice Y] [TopologicalSpace.SeparableSpace Y] (p : PaperLatticeNorm Y) {K : ℝ} (hseq : IsWeakSequentialNakanoConstant p.toFun K) :
        IsWeakNakanoConstant p.toFun K

        Extends the separable sequential-to-directed reduction to an arbitrary PaperLatticeNorm; used to prove component_weakFatou.

        source
        theorem OrderClosures.weakFatou_of_weakNakano_p {Y : Type u} [AddCommGroup Y] [Lattice Y] [IsOrderedAddMonoid Y] [VectorLattice Y] (p : PaperLatticeNorm Y) {K : ℝ} (hNak : IsWeakNakanoConstant p.toFun K) :
        HasWeakFatouProperty p.toFun K

        Extends the weak-Nakano-to-weak-Fatou implication to a PaperLatticeNorm; used for the component norm in component_weakFatou.

        source
        theorem OrderClosures.weakNakano_of_weakSequentialNakano {Y : Type u} [NormedAddCommGroup Y] [Lattice Y] [IsOrderedAddMonoid Y] [NormedVectorLattice Y] [TopologicalSpace.SeparableSpace Y] {K : ℝ} (hseq : IsWeakSequentialNakanoConstant norm K) :
        IsWeakNakanoConstant norm K

        Promotes the sequential weak Nakano estimate to directed sets in a separable normed lattice, by specializing the paper-norm reduction.

        source
        theorem OrderClosures.weakFatou_of_weakNakano_norm {Y : Type u} [NormedAddCommGroup Y] [Lattice Y] [IsOrderedAddMonoid Y] [NormedVectorLattice Y] {K : ℝ} (hNak : IsWeakNakanoConstant norm K) :
        HasWeakFatouProperty norm K

        Converts the directed weak Nakano estimate into the weak Fatou inequality for an ambient norm, by specializing the paper-norm reduction.

        source
        theorem OrderClosures.separable_weakSequentialNakano_implies_weakNakano {Y : Type u} [NormedAddCommGroup Y] [Lattice Y] [IsOrderedAddMonoid Y] [NormedVectorLattice Y] [TopologicalSpace.SeparableSpace Y] {K : ℝ} (hseq : IsWeakSequentialNakanoConstant norm K) :
        IsWeakNakanoConstant norm K ∧ HasWeakFatouProperty norm K

        Paper Proposition prop:separable-reduction.