Thinning, transient bands, and component moderatedness

theorem OrderClosures.tree_thinning (n : ℕ) (w : ℕ → TreeCoefficients n) (Λ : Finset (TreeBandIndex n)) (hΛ : recurrentBands n w ⊆ ↑Λ) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ B ∉ Λ, {m : ℕ | (treeBandProjection n B (w (φ m))).support.Nonempty}.Subsingleton

Paper Lemma lem:thinning.

theorem OrderClosures.treeOperator_apply_eq_zero_of_outside_support (n : ℕ) (w : TreeCoefficients n) {α : TreeProduct n} (hα : α ∉ finiteCylinderUnion n w.support) : (treeOperator n w) α = 0

Shows that a tree operator vanishes outside the union of cylinders in its support; used by tree_transient to eliminate common positive lower bounds.

theorem OrderClosures.tree_transient (n : ℕ) (w : ℕ → TreeCoefficients n) (Λ : Finset (TreeBandIndex n)) (hnone : none ∈ Λ) (hdis : ∀ B ∉ Λ, {m : ℕ | (treeBandProjection n B (w m)).support.Nonempty}.Subsingleton) : have v := fun (m : ℕ) => w m - finiteBandProjection n Λ (w m); (Pairwise fun (i j : ℕ) => ParentDisjoint ↑(v i).support ↑(v j).support) ∧ ∀ (z : BoundedContinuousFunction (TreeProduct n) ℝ), 0 ≤ z → (∀ (m : ℕ), z ≤ treeOperator n (v m)) → z = 0

Paper Lemma lem:transient.

theorem OrderClosures.component_moderated (n : ℕ) (x : ℕ → TreeComponent n) (hxmono : Monotone x) (hxpos : ∀ (m : ℕ), 0 ≤ x m) (hxnorm : ∀ (m : ℕ), (componentLatticeNorm n).toFun (x m) ≤ 1) {ε : ℝ} (hε : 0 < ε) : ∃ (w : TreeCoefficients n), 0 ≤ w ∧ (∀ (m : ℕ), ↑(x m) ≤ treeOperator n w) ∧ treeRho n w ≤ 2 + ε

Paper Proposition prop:moderated.

theorem OrderClosures.component_weakFatou (n : ℕ) : IsWeakNakanoConstant (componentLatticeNorm n).toFun 2 ∧ HasWeakFatouProperty (componentLatticeNorm n).toFun 2

Paper Corollary cor:weak-fatou.