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

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

Tail union for quantitative bad scales

This file contains the union bound over all bad scales at or above a level N. It is the quantitative tail-event layer used before constructing the random minimal scale; it deliberately does not introduce an eventual almost-sure stopping scale.

def HCPolySupport.Book.Ch05.Section57.badTailEvent {Ω : Type u_1} (Bad : ℕ → Set Ω) (N : ℕ) : Set Ω

The event that at least one bad scale occurs at or above N.

Equations

• HCPolySupport.Book.Ch05.Section57.badTailEvent Bad N = {ω : Ω | ∃ (K : ℕ), N ≤ K ∧ ω ∈ Bad K}

theorem HCPolySupport.Book.Ch05.Section57.badScaleEvent_antitone {Ω : Type u_1} {H : ℕ → ℕ → Ω → ℝ} {t α : ℝ} (hα : 0 ≤ α) {N K : ℕ} (hNK : N ≤ K) : badScaleEvent H t α K ⊆ badScaleEvent H t α N

theorem HCPolySupport.Book.Ch05.Section57.badTailEvent_badScaleEvent_subset {Ω : Type u_1} {H : ℕ → ℕ → Ω → ℝ} {t α : ℝ} (hα : 0 ≤ α) {N : ℕ} : badTailEvent (badScaleEvent H t α) N ⊆ badScaleEvent H t α N

theorem HCPolySupport.Book.Ch05.Section57.badTailEvent_eq_iUnion_shift {Ω : Type u_1} {Bad : ℕ → Set Ω} {N : ℕ} : badTailEvent Bad N = ⋃ (j : ℕ), Bad (N + j)

theorem HCPolySupport.Book.Ch05.Section57.measureReal_badTailEvent_le_tsum_shift {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {Bad : ℕ → Set Ω} {N : ℕ} (hBad : Summable fun (j : ℕ) => μ.real (Bad (N + j))) : μ.real (badTailEvent Bad N) ≤ ∑' (j : ℕ), μ.real (Bad (N + j))

Countable union bound for bad-tail events.

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

The concrete bad-tail event for the finite-probe bad-scale events.

Equations

• HCPolySupport.Book.Ch05.Section57.probeBadTailEvent H t α N = HCPolySupport.Book.Ch05.Section57.badTailEvent (HCPolySupport.Book.Ch05.Section57.badScaleEvent H t α) N

theorem HCPolySupport.Book.Ch05.Section57.measureReal_probeBadTailEvent_le_tsum_shift {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {H : ℕ → ℕ → Ω → ℝ} {t α : ℝ} {N : ℕ} (hBad : Summable fun (j : ℕ) => μ.real (badScaleEvent H t α (N + j))) : μ.real (probeBadTailEvent H t α N) ≤ ∑' (j : ℕ), μ.real (badScaleEvent H t α (N + j))

Union bound for the concrete finite-probe bad-tail event.