Component adherence and the final c₀-sum

Component spaces and the final c₀-sum

def OrderClosures.terminalTreeFunctions (n : ℕ) : Set (BoundedContinuousFunction (TreeProduct n) ℝ)

Terminal tree functions L_n.

Equations

• OrderClosures.terminalTreeFunctions n = OrderClosures.treeFunction n '' {t : OrderClosures.TreeNode n | t.level = n}

theorem OrderClosures.component_large_iterated_adherence (n : ℕ) : TopologicalSpace.IsSeparable Set.univ ∧ IsCompleteFor (componentLatticeNorm n).toFun ∧ HasWeakFatouProperty (componentLatticeNorm n).toFun 2 ∧ 2 ^ n • componentRoot n ∈ iteratedOrderAdherence (unitBallFor (componentLatticeNorm n).toFun) n ∧ (componentLatticeNorm n).toFun (2 ^ n • componentRoot n) = 2 ^ n

Paper Proposition prop:component.

@[reducible, inline]

abbrev OrderClosures.ComponentProduct : Type

The ambient product of all component spaces.

Equations

• OrderClosures.ComponentProduct = ((n : ℕ) → OrderClosures.TreeComponent n)

def OrderClosures.componentVanishes (x : ComponentProduct) : Prop

The usual c₀ condition for the component norms.

Equations

• OrderClosures.componentVanishes x = Filter.Tendsto (fun (n : ℕ) => (OrderClosures.componentLatticeNorm n).toFun (x n)) Filter.atTop (nhds 0)

noncomputable def OrderClosures.componentC0Sublattice : VectorSublattice ComponentProduct

The concrete c₀-sum as a vector sublattice of the component product.

Equations

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

@[reducible, inline]

abbrev OrderClosures.FinalSpace : Type

The final space X = c₀(X_n), using the underlying submodule carrier.

Equations

• OrderClosures.FinalSpace = ↥OrderClosures.componentC0Sublattice.toSubmodule

noncomputable def OrderClosures.finalCoordinateEmbedding (n : ℕ) (z : TreeComponent n) : FinalSpace

Inclusion of one component as a coordinate band of the final c₀-sum.

Equations

• OrderClosures.finalCoordinateEmbedding n z = ⟨fun (m : ℕ) => if h : m = n then ⋯ ▸ z else 0, ⋯⟩

theorem OrderClosures.finalCoordinateEmbedding_ne (n m : ℕ) (h : m ≠ n) (z : TreeComponent n) : ↑(finalCoordinateEmbedding n z) m = 0

Evaluates a single-coordinate embedding away from its chosen coordinate; used in the final lattice and convergence calculations.

@[instance_reducible]

noncomputable instance OrderClosures.finalSpaceLattice : Lattice FinalSpace

Pointwise lattice operations on the final c₀-sum.

Equations

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

instance OrderClosures.finalSpaceIsOrderedAddMonoid : IsOrderedAddMonoid FinalSpace

Compatibility of addition and order on the final space.

@[instance_reducible]

noncomputable instance OrderClosures.finalSpaceVectorLattice : VectorLattice FinalSpace

The final c₀-sum is a real vector lattice.

Equations

• OrderClosures.finalSpaceVectorLattice = { toModule := OrderClosures.componentC0Sublattice.instVectorLatticeSubtype.toModule, toPosSMulMono := OrderClosures.finalSpaceVectorLattice._proof_5 }

noncomputable def OrderClosures.finalNormValue (x : FinalSpace) : ℝ

The supremum norm on the final c₀-sum.

Equations

• OrderClosures.finalNormValue x = sSup (Set.range fun (n : ℕ) => (OrderClosures.componentLatticeNorm n).toFun (↑x n))

theorem OrderClosures.finalNormValue_bddAbove (x : FinalSpace) : BddAbove (Set.range fun (n : ℕ) => (componentLatticeNorm n).toFun (↑x n))

Records boundedness of the component norms of a c₀ vector; needed to justify the supremum defining finalNormValue.

theorem OrderClosures.componentNorm_le_finalNormValue (x : FinalSpace) (n : ℕ) : (componentLatticeNorm n).toFun (↑x n) ≤ finalNormValue x

Bounds each component norm by the final supremum norm; used in all norm laws and coordinatewise estimates for the final space.

noncomputable def OrderClosures.finalLatticeNorm : PaperLatticeNorm FinalSpace

The final lattice norm, with all its laws exposed as proof obligations.

Equations

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

theorem OrderClosures.finalSpace_weakFatou : IsCompleteFor finalLatticeNorm.toFun ∧ HasWeakFatouProperty finalLatticeNorm.toFun 2

Paper Lemma lem:c0-weak-fatou.

theorem OrderClosures.finalLatticeNorm_coordinateEmbedding (n : ℕ) (z : TreeComponent n) : finalLatticeNorm.toFun (finalCoordinateEmbedding n z) = (componentLatticeNorm n).toFun z

Shows that single-coordinate inclusion is isometric; used to transfer the component large-vector norm to the final space.

theorem OrderClosures.finalCoordinateEmbedding_orderConverges {n : ℕ} {ι : Type} [Preorder ι] {f : ι → TreeComponent n} {z : TreeComponent n} (hf : OrderConvergesTo f z) : OrderConvergesTo (fun (i : ι) => finalCoordinateEmbedding n (f i)) (finalCoordinateEmbedding n z)

Shows that single-coordinate inclusion preserves order convergence; used to transfer iterated component adherence into the final space.

theorem OrderClosures.finalCoordinateEmbedding_iteratedOrderAdherence (n k : ℕ) {z : TreeComponent n} (hz : z ∈ iteratedOrderAdherence (unitBallFor (componentLatticeNorm n).toFun) k) : finalCoordinateEmbedding n z ∈ iteratedOrderAdherence (unitBallFor finalLatticeNorm.toFun) k

Transfers membership through every finite adherence stage along a coordinate embedding; used for finalLargeVector_properties.

noncomputable def OrderClosures.finalLargeVector (n : ℕ) : FinalSpace

The vector z_n, supported in coordinate n.

Equations

• OrderClosures.finalLargeVector n = ⟨fun (m : ℕ) => if h : m = n then ⋯ ▸ (2 ^ n • OrderClosures.componentRoot n) else 0, ⋯⟩

theorem OrderClosures.finalLargeVector_properties (n : ℕ) : finalLargeVector n ∈ iteratedOrderAdherence (unitBallFor finalLatticeNorm.toFun) n ∧ finalLatticeNorm.toFun (finalLargeVector n) = 2 ^ n

Paper Proposition prop:zn.

theorem OrderClosures.finalSpace_not_equivalent_fatou (q : PaperLatticeNorm FinalSpace) : HasFatouProperty q.toFun → ¬EquivalentNorms finalLatticeNorm.toFun q.toFun

The constructed c₀-sum admits no equivalent Fatou lattice norm.

theorem OrderClosures.exists_weaklyFatou_not_equivalent_fatou : ∃ (X : Type) (x : AddCommGroup X) (x_1 : Lattice X) (x_2 : IsOrderedAddMonoid X) (x_3 : VectorLattice X) (p : PaperLatticeNorm X), IsCompleteFor p.toFun ∧ HasWeakFatouProperty p.toFun 2 ∧ ∀ (q : PaperLatticeNorm X), HasFatouProperty q.toFun → ¬EquivalentNorms p.toFun q.toFun

Paper Theorem thm:fremlin-main.