Coarse-graining support: Support.Book.Ch05.Theorems.Section57.BadScaleUnion #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Union bound for quantitative bad scales #
This file contains only the countable union bound which passes from the bad-scale event to its fixed-pair components. It is part of the quantitative tail proof and does not introduce a last-bad-scale construction.
theorem
HCPolySupport.Book.Ch05.Section57.measureReal_iUnion_nat_le_tsum
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{E : ℕ → Set Ω}
(hE : Summable fun (k : ℕ) => μ.real (E k))
:
theorem
HCPolySupport.Book.Ch05.Section57.measureReal_badScaleEvent_le_tsum_unpair_badPairEvent
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{H : ℕ → ℕ → Ω → ℝ}
{t α : ℝ}
{N : ℕ}
(hE : Summable fun (k : ℕ) => μ.real (badPairEvent H t α N (Nat.unpair k).1 (Nat.unpair k).2))
:
μ.real (badScaleEvent H t α N) ≤ ∑' (k : ℕ), μ.real (badPairEvent H t α N (Nat.unpair k).1 (Nat.unpair k).2)
The bad-scale event is bounded by the sum of the fixed-pair bad events.