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

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

Deterministic splitting of bad-scale events

This file records the exact trichotomy used in the proof of Theorem t.homogenization.quenched: the localized high range, the crude bottom range, and the crude complementary top range.

noncomputable def HCPolySupport.Book.Ch05.Section57.selectedBadPairScale (K a t α : ℝ) (q m n : ℕ) : ℕ

The intermediate scale selected for a bad pair in the high-range argument.

Equations

• HCPolySupport.Book.Ch05.Section57.selectedBadPairScale K a t α q m n = ⌈(a * Real.log 3)⁻¹ * (Real.log (max (2 * K) 1) + (α * ↑(m - q) - t * ↑(m - n)) * Real.log 3)⌉₊

def HCPolySupport.Book.Ch05.Section57.highBadScaleEvent {Ω : Type u_1} (H : ℕ → ℕ → Ω → ℝ) (K a t α : ℝ) (q : ℕ) : Set Ω

High part of a bad-scale event: the selected intermediate scale is strictly below n, so the localized first-quenched estimate applies.

Equations

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

def HCPolySupport.Book.Ch05.Section57.highTopBadScaleEvent {Ω : Type u_1} (H : ℕ → ℕ → Ω → ℝ) (K a t α : ℝ) (q : ℕ) : Set Ω

High part in the sharp range where the bad scale lies below the localized scale. This branch keeps the q-scale concentration gain.

Equations

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

def HCPolySupport.Book.Ch05.Section57.highBottomBadScaleEvent {Ω : Type u_1} (H : ℕ → ℕ → Ω → ℝ) (K a t α : ℝ) (q : ℕ) : Set Ω

High part in the bottom range. The localized estimate still applies, but the sharp q ≤ n concentration gain is not available.

Equations

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

def HCPolySupport.Book.Ch05.Section57.crudeBottomBadScaleEvent {Ω : Type u_1} (H : ℕ → ℕ → Ω → ℝ) (K a t α : ℝ) (q : ℕ) : Set Ω

Crude bottom part: the selected localized scale is not available and the localized scale is below the bad scale.

Equations

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

def HCPolySupport.Book.Ch05.Section57.crudeTopBadScaleEvent {Ω : Type u_1} (H : ℕ → ℕ → Ω → ℝ) (K a t α : ℝ) (q : ℕ) : Set Ω

Crude top complement: the bad scale is below n, but the selected intermediate scale is not available below n.

Equations

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

theorem HCPolySupport.Book.Ch05.Section57.badScaleEvent_subset_split {Ω : Type u_1} {H : ℕ → ℕ → Ω → ℝ} {K a t α : ℝ} {q : ℕ} : badScaleEvent H t α q ⊆ highBadScaleEvent H K a t α q ∪ crudeBottomBadScaleEvent H K a t α q ∪ crudeTopBadScaleEvent H K a t α q

theorem HCPolySupport.Book.Ch05.Section57.badScaleEvent_subset_sharp_split {Ω : Type u_1} {H : ℕ → ℕ → Ω → ℝ} {K a t α : ℝ} {q : ℕ} : badScaleEvent H t α q ⊆ highTopBadScaleEvent H K a t α q ∪ highBottomBadScaleEvent H K a t α q ∪ crudeBottomBadScaleEvent H K a t α q ∪ crudeTopBadScaleEvent H K a t α q

theorem HCPolySupport.Book.Ch05.Section57.measureReal_badScaleEvent_le_split {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {H : ℕ → ℕ → Ω → ℝ} {K a t α : ℝ} {q : ℕ} : μ.real (badScaleEvent H t α q) ≤ μ.real (highBadScaleEvent H K a t α q) + μ.real (crudeBottomBadScaleEvent H K a t α q) + μ.real (crudeTopBadScaleEvent H K a t α q)

theorem HCPolySupport.Book.Ch05.Section57.measureReal_badScaleEvent_le_sharp_split {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {H : ℕ → ℕ → Ω → ℝ} {K a t α : ℝ} {q : ℕ} : μ.real (badScaleEvent H t α q) ≤ μ.real (highTopBadScaleEvent H K a t α q) + μ.real (highBottomBadScaleEvent H K a t α q) + μ.real (crudeBottomBadScaleEvent H K a t α q) + μ.real (crudeTopBadScaleEvent H K a t α q)