The induced tree seminorm and component lattice

The induced seminorm

@[reducible, inline]

abbrev OrderClosures.TreeCoefficients (n : ℕ) : Type

W_n = c₀₀(G_n).

Equations

• OrderClosures.TreeCoefficients n = (OrderClosures.TreeNode n →₀ ℝ)

noncomputable def OrderClosures.treeBasis {n : ℕ} (t : TreeNode n) : TreeCoefficients n

The basis vector e_t.

Equations

• OrderClosures.treeBasis t = Finsupp.single t 1

noncomputable def OrderClosures.treeRho (n : ℕ) (w : TreeCoefficients n) : ℝ

The weighted ℓ¹ functional ρ_n.

Equations

• OrderClosures.treeRho n w = Finsupp.sum w fun (t : OrderClosures.TreeNode n) (a : ℝ) => 2 ^ (-↑t.level) * |a|

noncomputable def OrderClosures.treeOperator (n : ℕ) (w : TreeCoefficients n) : BoundedContinuousFunction (TreeProduct n) ℝ

The positive operator T_n.

Equations

• OrderClosures.treeOperator n w = Finsupp.sum w fun (t : OrderClosures.TreeNode n) (a : ℝ) => a • OrderClosures.treeFunction n t

noncomputable def OrderClosures.treeSeminorm (n : ℕ) (x : BoundedContinuousFunction (TreeProduct n) ℝ) : ℝ

The infimum formula defining p_n.

Equations

• OrderClosures.treeSeminorm n x = sInf {r : ℝ | ∃ (w : OrderClosures.TreeCoefficients n), 0 ≤ w ∧ |x| ≤ OrderClosures.treeOperator n w ∧ OrderClosures.treeRho n w = r}

theorem OrderClosures.treeRho_nonneg (n : ℕ) (w : TreeCoefficients n) : 0 ≤ treeRho n w

Records nonnegativity of the weighted coefficient functional; used in all seminorm and band-mass estimates.

theorem OrderClosures.treeRho_neg (n : ℕ) (w : TreeCoefficients n) : treeRho n (-w) = treeRho n w

Shows that treeRho is invariant under negation; used for symmetry of the bundled lattice seminorm.

theorem OrderClosures.treeRho_smul (n : ℕ) (a : ℝ) (w : TreeCoefficients n) : treeRho n (a • w) = |a| * treeRho n w

Computes treeRho under scalar multiplication; used for homogeneity of the tree seminorm.

theorem OrderClosures.treeRho_add_le (n : ℕ) (u v : TreeCoefficients n) : treeRho n (u + v) ≤ treeRho n u + treeRho n v

Gives the triangle inequality for treeRho; used to prove subadditivity of the induced seminorm.

theorem OrderClosures.treeRho_mono_of_nonneg (n : ℕ) {u v : TreeCoefficients n} (hu : 0 ≤ u) (huv : u ≤ v) : treeRho n u ≤ treeRho n v

Shows coefficientwise monotonicity of treeRho on the positive cone; used to compare band projections and trimmed coefficients.

theorem OrderClosures.treeOperator_zero (n : ℕ) : treeOperator n 0 = 0

Computes the tree operator at zero; used in the zero law for the induced seminorm and generated sublattice.

theorem OrderClosures.treeOperator_add (n : ℕ) (u v : TreeCoefficients n) : treeOperator n (u + v) = treeOperator n u + treeOperator n v

Records additivity of the tree operator; used in seminorm subadditivity and the moderatedness decomposition.

theorem OrderClosures.treeOperator_smul (n : ℕ) (a : ℝ) (w : TreeCoefficients n) : treeOperator n (a • w) = a • treeOperator n w

Records homogeneity of the tree operator; used to scale majorants in the seminorm and component constructions.

theorem OrderClosures.treeOperator_nonneg (n : ℕ) (w : TreeCoefficients n) (hw : 0 ≤ w) : 0 ≤ treeOperator n w

A coefficientwise positive vector has a positive tree image; used whenever an operator majorant is treated as a positive component.

theorem OrderClosures.treeOperator_single (n : ℕ) (t : TreeNode n) (a : ℝ) : treeOperator n (Finsupp.single t a) = a • treeFunction n t

Evaluates the tree operator on a single basis coefficient; used to place tree functions in the generated component.

theorem OrderClosures.treeOperator_apply (n : ℕ) (w : TreeCoefficients n) (α : TreeProduct n) : (treeOperator n w) α = Finsupp.sum w fun (t : TreeNode n) (a : ℝ) => a * (treeFunction n t) α

Expands pointwise evaluation of the tree operator as a finite sum; used in support-vanishing and root estimates.

theorem OrderClosures.treeFunction_root (n : ℕ) : treeFunction n (TreeNode.root n) = 1

Identifies the root tree function with the constant one function; used as the universal positive order majorant.

theorem OrderClosures.abs_le_norm_smul_root (n : ℕ) (x : BoundedContinuousFunction (TreeProduct n) ℝ) : |x| ≤ ‖x‖ • treeFunction n (TreeNode.root n)

Dominates any continuous function by its uniform norm times the root; used to prove that the admissible-majorant set is nonempty.

theorem OrderClosures.treeAdmissible_nonempty (n : ℕ) (x : BoundedContinuousFunction (TreeProduct n) ℝ) : {r : ℝ | ∃ (w : TreeCoefficients n), 0 ≤ w ∧ |x| ≤ treeOperator n w ∧ treeRho n w = r}.Nonempty

Supplies a coefficient majorant for every function; needed to define the infimum in treeSeminorm.

theorem OrderClosures.treeAdmissible_bddBelow (n : ℕ) (x : BoundedContinuousFunction (TreeProduct n) ℝ) : BddBelow {r : ℝ | ∃ (w : TreeCoefficients n), 0 ≤ w ∧ |x| ≤ treeOperator n w ∧ treeRho n w = r}

Bounds all admissible treeRho values below by zero; used to justify order properties of the defining infimum.

theorem OrderClosures.treeSeminorm_nonneg (n : ℕ) (x : BoundedContinuousFunction (TreeProduct n) ℝ) : 0 ≤ treeSeminorm n x

Proves nonnegativity of treeSeminorm; used as a field of the bundled lattice seminorm.

theorem OrderClosures.treeSeminorm_le_of_majorant (n : ℕ) (x : BoundedContinuousFunction (TreeProduct n) ℝ) (w : TreeCoefficients n) (hw : 0 ≤ w) (hxw : |x| ≤ treeOperator n w) : treeSeminorm n x ≤ treeRho n w

Bounds the seminorm by any admissible coefficient majorant; used throughout the exact-basis and moderatedness estimates.

theorem OrderClosures.treeSeminorm_zero (n : ℕ) : treeSeminorm n 0 = 0

Evaluates the tree seminorm at zero; used for the zero field of treeLatticeSeminorm.

theorem OrderClosures.exists_treeMajorant_lt (n : ℕ) (x : BoundedContinuousFunction (TreeProduct n) ℝ) {ε : ℝ} (hε : 0 < ε) : ∃ (w : TreeCoefficients n), 0 ≤ w ∧ |x| ≤ treeOperator n w ∧ treeRho n w < treeSeminorm n x + ε

Approximates the infimum defining treeSeminorm by a strict majorant; used to prove seminorm laws and to select coefficients in component_moderated.

theorem OrderClosures.treeSeminorm_smul_le (n : ℕ) (a : ℝ) (x : BoundedContinuousFunction (TreeProduct n) ℝ) : treeSeminorm n (a • x) ≤ |a| * treeSeminorm n x

Gives the difficult direction of seminorm homogeneity; used together with rescaling to prove equality in the bundled seminorm.

theorem OrderClosures.treeFunction_norm_le_one (n : ℕ) (t : TreeNode n) : ‖treeFunction n t‖ ≤ 1

Bounds every tree function in uniform norm; used to control finite tree operators by their coefficient sums.

theorem OrderClosures.treeOperator_norm_le_sum (n : ℕ) (w : TreeCoefficients n) : ‖treeOperator n w‖ ≤ ∑ t ∈ w.support, |w t|

Bounds the uniform norm of a tree operator by the absolute coefficient sum; used in the comparison between uniform and tree norms.

theorem OrderClosures.treeRho_controls_sum (n : ℕ) (w : TreeCoefficients n) : ∑ t ∈ w.support, |w t| ≤ 2 ^ n * treeRho n w

Controls the unweighted coefficient sum by treeRho; combined with the operator estimate to obtain the norm comparison.

theorem OrderClosures.norm_le_pow_mul_treeRho (n : ℕ) (x : BoundedContinuousFunction (TreeProduct n) ℝ) (w : TreeCoefficients n) (hw : 0 ≤ w) (hxw : |x| ≤ treeOperator n w) : ‖x‖ ≤ 2 ^ n * treeRho n w

Combines the preceding estimates into the main operator norm bound; used to prove definiteness and equivalence of the component norm.

theorem OrderClosures.treeOperator_le_root_of_nonneg (n : ℕ) (w : TreeCoefficients n) (hw : 0 ≤ w) : treeOperator n w ≤ (2 ^ n * treeRho n w) • treeFunction n (TreeNode.root n)

Dominates a positive tree operator by its total coefficient mass times the root; used in the upper norm comparison.

noncomputable def OrderClosures.treeLatticeSeminorm (n : ℕ) : LatticeSeminorm (BoundedContinuousFunction (TreeProduct n) ℝ)

Paper Lemma lem:pn-seminorm, bundled using BanLat's LatticeSeminorm.

Equations

• OrderClosures.treeLatticeSeminorm n = { toFun := OrderClosures.treeSeminorm n, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, smul' := ⋯, monotone_abs' := ⋯ }

theorem OrderClosures.treeSeminorm_norm_comparison (n : ℕ) (x : BoundedContinuousFunction (TreeProduct n) ℝ) : treeSeminorm n x ≤ ‖x‖ ∧ ‖x‖ ≤ 2 ^ n * treeSeminorm n x

Paper Lemma lem:norm-comparison.

theorem OrderClosures.level_strictPrefix {n : ℕ} (t : TreeNode n) (j : Fin t.level) : (↑(strictPrefix t j)).level = ↑j

Computes the level of a strict prefix; used to compare nodes from nested tree cylinders in the exact-basis proof.

theorem OrderClosures.level_le_of_treeCylinder_subset {n : ℕ} {t u : TreeNode n} (hsub : treeCylinder n t ⊆ treeCylinder n u) : u.level ≤ t.level

Shows that inclusion of nonempty tree cylinders forces the corresponding level inequality; used to isolate the maximal-weight basis term.

theorem OrderClosures.treeFunction_nonneg (n : ℕ) (t : TreeNode n) : 0 ≤ treeFunction n t

Records positivity of every tree function; used for lattice estimates and for the positive terminal family in the component construction.

theorem OrderClosures.treeSeminorm_exact_basis (n : ℕ) (t : TreeNode n) : (∀ (w : TreeCoefficients n), 0 ≤ w → treeFunction n t ≤ treeOperator n w → 2 ^ (-↑t.level) ≤ treeRho n w) ∧ treeSeminorm n (treeFunction n t) = 2 ^ (-↑t.level)

Paper Lemma lem:exact-basis.

noncomputable def OrderClosures.treeSublattice (n : ℕ) : VectorSublattice (BoundedContinuousFunction (TreeProduct n) ℝ)

The closed vector sublattice generated by the tree functions.

Equations

• OrderClosures.treeSublattice n = (VectorSublattice.generated (Set.range (OrderClosures.treeFunction n))).topologicalClosure

theorem OrderClosures.treeOperator_mem_treeSublattice (n : ℕ) (w : TreeCoefficients n) : treeOperator n w ∈ treeSublattice n

Places every finitely supported tree operator in the generated closed sublattice; used to turn coefficient majorants into component elements.

@[reducible, inline]

abbrev OrderClosures.TreeComponent (n : ℕ) : Type

The component space X_n, using the underlying submodule carrier.

Equations

• OrderClosures.TreeComponent n = ↥(OrderClosures.treeSublattice n).toSubmodule

@[instance_reducible]

noncomputable instance OrderClosures.treeComponentLattice (n : ℕ) : Lattice (TreeComponent n)

Pointwise lattice operations on the component subspace.

Equations

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

instance OrderClosures.treeComponentIsOrderedAddMonoid (n : ℕ) : IsOrderedAddMonoid (TreeComponent n)

Compatibility of the inherited addition with the pointwise order.

@[instance_reducible]

noncomputable instance OrderClosures.treeComponentVectorLattice (n : ℕ) : VectorLattice (TreeComponent n)

The component subspace is a real vector lattice.

Equations

• OrderClosures.treeComponentVectorLattice n = { toModule := (OrderClosures.treeSublattice n).instVectorLatticeSubtype.toModule, toPosSMulMono := ⋯ }

noncomputable def OrderClosures.componentLatticeNorm (n : ℕ) : PaperLatticeNorm (TreeComponent n)

The norm p_n restricted to X_n.

Equations

• OrderClosures.componentLatticeNorm n = { toFun := fun (x : OrderClosures.TreeComponent n) => OrderClosures.treeSeminorm n ↑x, nonneg := ⋯, eq_zero_iff := ⋯, add_le := ⋯, smul := ⋯, solid := ⋯ }

noncomputable def OrderClosures.componentRoot (n : ℕ) : TreeComponent n

The constant function 1, as an element of X_n.

Equations

• OrderClosures.componentRoot n = ⟨OrderClosures.treeFunction n (OrderClosures.TreeNode.root n), ⋯⟩

noncomputable def OrderClosures.componentTreeFunction (n : ℕ) (t : TreeNode n) : TreeComponent n

Any tree function, viewed in the generated component.

Equations

• OrderClosures.componentTreeFunction n t = ⟨OrderClosures.treeFunction n t, ⋯⟩

theorem OrderClosures.component_basic (n : ℕ) : TopologicalSpace.IsSeparable Set.univ ∧ IsCompleteFor (componentLatticeNorm n).toFun ∧ (componentLatticeNorm n).toFun (componentRoot n) = 1 ∧ ∀ (t : TreeNode n), t.level = n → (componentLatticeNorm n).toFun (componentTreeFunction n t) = 2 ^ (-↑n)

Paper Corollary cor:Yn-basic.