Coarse-graining support: Support.Book.Ch05.Theorems.Section57.BadScaleEntrySplit

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Splitting absolute bad scales at the annealed entry scale

The quantitative bad-scale estimate is proved after shifting the annealed entry scale to zero. The final quenched theorem also has to cover the finite bottom band below that entry scale. This file records the deterministic decomposition separating those two contributions.

def HCPolySupport.Book.Ch05.Section57.smallBottomBadScaleEvent {Ω : Type u_1} (H : ℕ → ℕ → Ω → ℝ) (Nentry : ℕ) (t α : ℝ) (N : ℕ) : Set Ω

Bad event contributed by pairs whose bottom scale is below the entry scale.

Equations

• HCPolySupport.Book.Ch05.Section57.smallBottomBadScaleEvent H Nentry t α N = {ω : Ω | ∃ (m : ℕ), ∃ n < Nentry, n < m ∧ N ≤ m ∧ 3 ^ (-t * ↑(m - n)) * H m n ω > 3 ^ (-α * ↑(m - N))}

theorem HCPolySupport.Book.Ch05.Section57.badScaleEvent_subset_smallBottom_union_shifted {Ω : Type u_1} {H : ℕ → ℕ → Ω → ℝ} {Nentry N : ℕ} {t α : ℝ} (hNentryN : Nentry ≤ N) : badScaleEvent H t α N ⊆ smallBottomBadScaleEvent H Nentry t α N ∪ badScaleEvent (fun (M K : ℕ) (ω : Ω) => H (Nentry + M) (Nentry + K) ω) t α (N - Nentry)

The absolute bad event splits into the small-bottom band and the shifted bad event above the entry scale.

theorem HCPolySupport.Book.Ch05.Section57.badTailEvent_subset_smallBottom_union_shifted {Ω : Type u_1} {H : ℕ → ℕ → Ω → ℝ} {Nentry N : ℕ} {t α : ℝ} (hNentryN : Nentry ≤ N) : badTailEvent (badScaleEvent H t α) N ⊆ badTailEvent (smallBottomBadScaleEvent H Nentry t α) N ∪ badTailEvent (badScaleEvent (fun (M K : ℕ) (ω : Ω) => H (Nentry + M) (Nentry + K) ω) t α) (N - Nentry)

Tail-event form of badScaleEvent_subset_smallBottom_union_shifted.