Bands, upshift, trimming, and the weak Fatou estimate

Bands, upshift, and the weak Fatou estimate

@[reducible, inline]

abbrev OrderClosures.TreeBandIndex (n : ℕ) : Type

Indexing the root band and the sibling bands.

Equations

• OrderClosures.TreeBandIndex n = Option (OrderClosures.TreeNonterminal n)

def OrderClosures.treeBandSupport (n : ℕ) : TreeBandIndex n → Set (TreeNode n)

Support of a sibling band, with none denoting the root band.

Equations

• OrderClosures.treeBandSupport n none = {OrderClosures.TreeNode.root n}
• OrderClosures.treeBandSupport n (some u) = {t : OrderClosures.TreeNode n | t.parent = ↑u ∧ t ≠ OrderClosures.TreeNode.root n}

noncomputable def OrderClosures.treeBandProjection (n : ℕ) (B : TreeBandIndex n) (w : TreeCoefficients n) : TreeCoefficients n

Coordinate projection onto a sibling band.

Equations

• OrderClosures.treeBandProjection n B w = Finsupp.filter (fun (t : OrderClosures.TreeNode n) => t ∈ OrderClosures.treeBandSupport n B) w

noncomputable def OrderClosures.finiteBandProjection (n : ℕ) (Λ : Finset (TreeBandIndex n)) (w : TreeCoefficients n) : TreeCoefficients n

Projection onto a finite family of sibling bands.

Equations

• OrderClosures.finiteBandProjection n Λ w = Finsupp.filter (fun (t : OrderClosures.TreeNode n) => ∃ B ∈ Λ, t ∈ OrderClosures.treeBandSupport n B) w

noncomputable def OrderClosures.treeBandOfNode (n : ℕ) (t : TreeNode n) : TreeBandIndex n

Assigns a node to the root band or the sibling band indexed by its parent; used to define the finite band partition pointwise.

Equations

• OrderClosures.treeBandOfNode n t = if h : t = OrderClosures.TreeNode.root n then none else some ⟨t.parent, ⋯⟩

theorem OrderClosures.node_mem_its_treeBand (n : ℕ) (t : TreeNode n) : t ∈ treeBandSupport n (treeBandOfNode n t)

Assigns every node to its canonical root or sibling band; used to partition coefficient supports.

theorem OrderClosures.treeBandOfNode_eq_of_mem (n : ℕ) (t : TreeNode n) (B : TreeBandIndex n) (ht : t ∈ treeBandSupport n B) : treeBandOfNode n t = B

Recovers the canonical band from membership in a band support; used to prove uniqueness in the band partition.

theorem OrderClosures.treeBandProjection_support_nonempty_iff (n : ℕ) (B : TreeBandIndex n) (w : TreeCoefficients n) : (treeBandProjection n B w).support.Nonempty ↔ ∃ t ∈ w.support, treeBandOfNode n t = B

Characterizes when a band projection has nonempty support; used to define and track recurrent bands.

noncomputable def OrderClosures.bandsAt (n : ℕ) (w : TreeCoefficients n) : Finset (TreeBandIndex n)

The finite set of canonical bands meeting the support of w; used by the subsequence recursion in tree_thinning.

Equations

• OrderClosures.bandsAt n w = Finset.image (OrderClosures.treeBandOfNode n) w.support

theorem OrderClosures.mem_bandsAt_iff (n : ℕ) (w : TreeCoefficients n) (B : TreeBandIndex n) : B ∈ bandsAt n w ↔ (treeBandProjection n B w).support.Nonempty

Characterizes the finite set of bands occurring in a coefficient vector; used in the thinning recursion.

theorem OrderClosures.finiteBandProjection_apply (n : ℕ) (Λ : Finset (TreeBandIndex n)) (w : TreeCoefficients n) (t : TreeNode n) : (treeBandOfNode n t ∈ Λ → (finiteBandProjection n Λ w) t = w t) ∧ (treeBandOfNode n t ∉ Λ → (finiteBandProjection n Λ w) t = 0)

Gives the pointwise formula for projection onto finitely many bands; used to decompose coefficients in trimming and moderatedness.

theorem OrderClosures.finiteBandProjection_nonneg (n : ℕ) (Λ : Finset (TreeBandIndex n)) {w : TreeCoefficients n} (hw : 0 ≤ w) : 0 ≤ finiteBandProjection n Λ w

A finite band projection preserves nonnegativity.

theorem OrderClosures.finiteBandProjection_le (n : ℕ) (Λ : Finset (TreeBandIndex n)) {w : TreeCoefficients n} (hw : 0 ≤ w) : finiteBandProjection n Λ w ≤ w

A finite band projection decreases nonnegative coefficient vectors.

theorem OrderClosures.treeRho_finiteBandProjection (n : ℕ) (Λ : Finset (TreeBandIndex n)) (w : TreeCoefficients n) : treeRho n (finiteBandProjection n Λ w) = ∑ B ∈ Λ, treeRho n (treeBandProjection n B w)

Expresses the mass of a finite band projection as a finite sum; used for tail-mass estimates in the trimming lemma.

noncomputable def OrderClosures.treeBandParent (n : ℕ) : TreeBandIndex n → TreeNode n

Chooses the root or parent node representing a band; used to define the upshift of all coefficients in that band.

Equations

• OrderClosures.treeBandParent n none = OrderClosures.TreeNode.root n
• OrderClosures.treeBandParent n (some u) = ↑u

theorem OrderClosures.parent_eq_treeBandParent (n : ℕ) (t : TreeNode n) : t.parent = treeBandParent n (treeBandOfNode n t)

Identifies a nonroot node's parent with the representative of its band; used to analyze the support of the upshift.

noncomputable def OrderClosures.treeUpshift (n : ℕ) (w : TreeCoefficients n) : TreeCoefficients n

The upshift S_n, merging coefficients at their parents.

Equations

• OrderClosures.treeUpshift n w = Finsupp.mapDomain OrderClosures.TreeNode.parent w

noncomputable def OrderClosures.treeBandParents (n : ℕ) (Λ : Finset (TreeBandIndex n)) : Finset (TreeNode n)

The finite set of representative parents of a finite band family; used to bound the support of upshifted coefficients.

Equations

• OrderClosures.treeBandParents n Λ = Finset.image (OrderClosures.treeBandParent n) Λ

theorem OrderClosures.treeUpshift_support_subset_bandParents (n : ℕ) (Λ : Finset (TreeBandIndex n)) (w : TreeCoefficients n) : (treeUpshift n (finiteBandProjection n Λ w)).support ⊆ treeBandParents n Λ

Bounds the support of an upshift by the finite set of band parents; used to obtain a finite-dimensional convergent subsequence.

theorem OrderClosures.treeParent_weight_le (n : ℕ) (t : TreeNode n) : 2 ^ (-↑t.parent.level) ≤ 2 * 2 ^ (-↑t.level)

Compares the weight of a parent node with that of its child; used to bound the treeRho cost of upshifting.

theorem OrderClosures.treeCylinder_subset_parent (n : ℕ) (t : TreeNode n) : treeCylinder n t ⊆ treeCylinder n t.parent

Shows that a node cylinder lies inside its parent cylinder; used to prove that upshifting increases the associated tree operator.

theorem OrderClosures.treeFunction_le_parent (n : ℕ) (t : TreeNode n) : treeFunction n t ≤ treeFunction n t.parent

Converts cylinder inclusion into domination by the parent tree function; used in treeUpshift_basic.

theorem OrderClosures.treeUpshift_basic (n : ℕ) (w : TreeCoefficients n) (hw : 0 ≤ w) : treeRho n (treeUpshift n w) ≤ 2 * treeRho n w ∧ treeOperator n w ≤ treeOperator n (treeUpshift n w)

Paper Lemma lem:upshift-basic.

theorem OrderClosures.treeRho_bandProjection_le (n : ℕ) (B : TreeBandIndex n) (w : TreeCoefficients n) : treeRho n (treeBandProjection n B w) ≤ treeRho n w

A single band projection cannot increase treeRho; used to uniformly bound each coordinate in the sharp-subsequence extraction.

theorem OrderClosures.treeRho_finiteBandProjection_le (n : ℕ) (Λ : Finset (TreeBandIndex n)) (w : TreeCoefficients n) : treeRho n (finiteBandProjection n Λ w) ≤ treeRho n w

A projection onto finitely many bands cannot increase treeRho; used in the coefficient decomposition for component_moderated.

theorem OrderClosures.sum_treeRho_bandProjection_le (n : ℕ) (Λ : Finset (TreeBandIndex n)) (w : TreeCoefficients n) : ∑ B ∈ Λ, treeRho n (treeBandProjection n B w) ≤ treeRho n w

Bounds the total mass of any finite band family by the original mass; used to prove summability of limiting band masses in tree_trim.

theorem OrderClosures.tree_sharp_subsequence (n : ℕ) (w : ℕ → TreeCoefficients n) (C : ℝ) (hw : ∀ (m : ℕ), treeRho n (w m) ≤ C) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (B : TreeBandIndex n), ∃ (l : ℝ), Filter.Tendsto (fun (m : ℕ) => treeRho n (treeBandProjection n B (w (φ m)))) Filter.atTop (nhds l)

Paper Lemma lem:sharp-subsequence.

def OrderClosures.recurrentBands (n : ℕ) (w : ℕ → TreeCoefficients n) : Set (TreeBandIndex n)

The bands occurring in infinitely many supports of a sequence.

Equations

• OrderClosures.recurrentBands n w = {B : OrderClosures.TreeBandIndex n | {m : ℕ | (OrderClosures.treeBandProjection n B (w m)).support.Nonempty}.Infinite}

noncomputable def OrderClosures.lastBandOccurrence (n : ℕ) (w : ℕ → TreeCoefficients n) (B : TreeBandIndex n) : ℕ

Records a final support occurrence for each nonrecurrent band; used to construct a subsequence in which transient bands occur at most once.

Equations

• OrderClosures.lastBandOccurrence n w B = if h : {m : ℕ | (OrderClosures.treeBandProjection n B (w m)).support.Nonempty}.Finite then h.toFinset.sup id else 0

theorem OrderClosures.le_lastBandOccurrence (n : ℕ) (w : ℕ → TreeCoefficients n) (B : TreeBandIndex n) (hfinite : {m : ℕ | (treeBandProjection n B (w m)).support.Nonempty}.Finite) {m : ℕ} (hm : (treeBandProjection n B (w m)).support.Nonempty) : m ≤ lastBandOccurrence n w B

Bounds every occurrence of a nonrecurrent band by its recorded last index; used to choose a subsequence with transient bands occurring at most once.

theorem OrderClosures.tree_trim (n : ℕ) (x : ℕ → TreeComponent n) (w : ℕ → TreeCoefficients n) {ε : ℝ} (hε : 0 < ε) (hw : ∀ (m : ℕ), 0 ≤ w m) (hdom : ∀ (m : ℕ), ↑(x m) ≤ treeOperator n (w m)) (hrho : ∀ (m : ℕ), treeRho n (w m) < 1 + ε / 4) (hsharp : ∀ (B : TreeBandIndex n), ∃ (l : ℝ), Filter.Tendsto (fun (m : ℕ) => treeRho n (treeBandProjection n B (w m))) Filter.atTop (nhds l)) : ∃ (w' : ℕ → TreeCoefficients n), (∀ (m : ℕ), 0 ≤ w' m ∧ ↑(x m) ≤ treeOperator n (w' m) ∧ treeRho n (w' m) < 1 + ε / 2) ∧ (recurrentBands n w').Finite

Paper Lemma lem:trim.