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

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

Union bounds for the split bad-scale components

The bad-scale proof estimates each deterministic branch by summing its fixed-pair events. This file contains only those set identities and union bounds.

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

The fixed-pair bad event in the top branch q ≤ n, with the selected bad-pair scale strictly below n.

Equations

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

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

The fixed-pair bad event in the bottom branch n ≤ q, with the selected bad-pair scale strictly below n.

Equations

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

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

The fixed-pair bad event in the bottom branch n ≤ q, with n no larger than the selected bad-pair scale.

Equations

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

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

The fixed-pair bad event in the top branch q ≤ n, with n no larger than the selected bad-pair scale.

Equations

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

theorem HCPolySupport.Book.Ch05.Section57.highTopBadScaleEvent_eq_iUnion_unpair {Ω : Type u_1} {H : ℕ → ℕ → Ω → ℝ} {K a t α : ℝ} {q : ℕ} : highTopBadScaleEvent H K a t α q = ⋃ (k : ℕ), highTopPairEvent H K a t α q (Nat.unpair k).1 (Nat.unpair k).2

theorem HCPolySupport.Book.Ch05.Section57.highBottomBadScaleEvent_eq_iUnion_unpair {Ω : Type u_1} {H : ℕ → ℕ → Ω → ℝ} {K a t α : ℝ} {q : ℕ} : highBottomBadScaleEvent H K a t α q = ⋃ (k : ℕ), highBottomPairEvent H K a t α q (Nat.unpair k).1 (Nat.unpair k).2

theorem HCPolySupport.Book.Ch05.Section57.crudeBottomBadScaleEvent_eq_iUnion_unpair {Ω : Type u_1} {H : ℕ → ℕ → Ω → ℝ} {K a t α : ℝ} {q : ℕ} : crudeBottomBadScaleEvent H K a t α q = ⋃ (k : ℕ), crudeBottomPairEvent H K a t α q (Nat.unpair k).1 (Nat.unpair k).2

theorem HCPolySupport.Book.Ch05.Section57.crudeTopBadScaleEvent_eq_iUnion_unpair {Ω : Type u_1} {H : ℕ → ℕ → Ω → ℝ} {K a t α : ℝ} {q : ℕ} : crudeTopBadScaleEvent H K a t α q = ⋃ (k : ℕ), crudeTopPairEvent H K a t α q (Nat.unpair k).1 (Nat.unpair k).2

theorem HCPolySupport.Book.Ch05.Section57.measureReal_highTopBadScaleEvent_le_tsum_unpair {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {H : ℕ → ℕ → Ω → ℝ} {K a t α : ℝ} {q : ℕ} (hsum : Summable fun (k : ℕ) => μ.real (highTopPairEvent H K a t α q (Nat.unpair k).1 (Nat.unpair k).2)) : μ.real (highTopBadScaleEvent H K a t α q) ≤ ∑' (k : ℕ), μ.real (highTopPairEvent H K a t α q (Nat.unpair k).1 (Nat.unpair k).2)

theorem HCPolySupport.Book.Ch05.Section57.measureReal_highBottomBadScaleEvent_le_tsum_unpair {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {H : ℕ → ℕ → Ω → ℝ} {K a t α : ℝ} {q : ℕ} (hsum : Summable fun (k : ℕ) => μ.real (highBottomPairEvent H K a t α q (Nat.unpair k).1 (Nat.unpair k).2)) : μ.real (highBottomBadScaleEvent H K a t α q) ≤ ∑' (k : ℕ), μ.real (highBottomPairEvent H K a t α q (Nat.unpair k).1 (Nat.unpair k).2)

theorem HCPolySupport.Book.Ch05.Section57.measureReal_crudeBottomBadScaleEvent_le_tsum_unpair {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {H : ℕ → ℕ → Ω → ℝ} {K a t α : ℝ} {q : ℕ} (hsum : Summable fun (k : ℕ) => μ.real (crudeBottomPairEvent H K a t α q (Nat.unpair k).1 (Nat.unpair k).2)) : μ.real (crudeBottomBadScaleEvent H K a t α q) ≤ ∑' (k : ℕ), μ.real (crudeBottomPairEvent H K a t α q (Nat.unpair k).1 (Nat.unpair k).2)

theorem HCPolySupport.Book.Ch05.Section57.measureReal_crudeTopBadScaleEvent_le_tsum_unpair {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {H : ℕ → ℕ → Ω → ℝ} {K a t α : ℝ} {q : ℕ} (hsum : Summable fun (k : ℕ) => μ.real (crudeTopPairEvent H K a t α q (Nat.unpair k).1 (Nat.unpair k).2)) : μ.real (crudeTopBadScaleEvent H K a t α q) ≤ ∑' (k : ℕ), μ.real (crudeTopPairEvent H K a t α q (Nat.unpair k).1 (Nat.unpair k).2)