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

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

Kernel union bounds for fixed-pair events

This file turns two-parameter stretched-exponential fixed-pair bounds into countable union bounds over the paired natural indices.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_iUnion_unpair_le_exp_two_kernel {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {E : ℕ → ℕ → Set Ω} {A ρ₁ ρ₂ η C : ℝ} (hC : 0 ≤ C) (hA : 1 ≤ A) (hρ₁ : 1 < ρ₁) (hρ₂ : 1 < ρ₂) (hη : 0 < η) (hE : ∀ (i j : ℕ), μ.real (E i j) ≤ C * Real.exp (-(A * ρ₁ ^ i * ρ₂ ^ j) ^ η)) : μ.real (⋃ (k : ℕ), E (Nat.unpair k).1 (Nat.unpair k).2) ≤ C * (Real.exp (-A ^ η) * geometricExpKernelConst ρ₁ η * geometricExpKernelConst ρ₂ η)

theorem HCPolySupport.Book.Ch05.Section57.measureReal_iUnion_linearRows_le_exp_linear_kernel {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {E : (r : ℕ) → Fin (r + 1) → Set Ω} {A ρ η C : ℝ} (hC : 0 ≤ C) (hA : 1 ≤ A) (hρ : 1 < ρ) (hη : 0 < η) (hE : ∀ (r : ℕ) (j : Fin (r + 1)), μ.real (E r j) ≤ C * Real.exp (-(A * ρ ^ r) ^ η)) : μ.real (⋃ (r : ℕ), ⋃ (j : Fin (r + 1)), E r j) ≤ C * (Real.exp (-A ^ η) * linearExpKernelConst ρ η)

theorem HCPolySupport.Book.Ch05.Section57.measureReal_iUnion_constRows_le_exp_kernel {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {Q : ℕ} {E : ℕ → Fin Q → Set Ω} {A ρ η C : ℝ} (hC : 0 ≤ C) (hA : 1 ≤ A) (hρ : 1 < ρ) (hη : 0 < η) (hE : ∀ (r : ℕ) (j : Fin Q), μ.real (E r j) ≤ C * Real.exp (-(A * ρ ^ r) ^ η)) : μ.real (⋃ (r : ℕ), ⋃ (j : Fin Q), E r j) ≤ ↑Q * C * (Real.exp (-A ^ η) * geometricExpKernelConst ρ η)

theorem HCPolySupport.Book.Ch05.Section57.measureReal_iUnion_linearRows_le_weighted_exp_linear_kernel {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {E : (r : ℕ) → Fin (r + 1) → Set Ω} {A ρ η C w : ℝ} (hC : 0 ≤ C) (hw : 0 < w) (hA : 1 ≤ A) (hρ : 1 < ρ) (hη : 0 < η) (hE : ∀ (r : ℕ) (j : Fin (r + 1)), μ.real (E r j) ≤ C * (w ^ r * Real.exp (-(A * ρ ^ r) ^ η))) : μ.real (⋃ (r : ℕ), ⋃ (j : Fin (r + 1)), E r j) ≤ C * (Real.exp (-A ^ η) * weightedLinearExpKernelConst w (ρ ^ η))

Linear-row union bound with an exponential finite-union prefactor kept outside the stochastic scale. The weighted superexponential kernel absorbs the prefactor without weakening the leading A exponent.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_iUnion_constRows_le_weighted_exp_kernel {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {Q : ℕ} {E : ℕ → Fin Q → Set Ω} {A ρ η C w : ℝ} (hC : 0 ≤ C) (hw : 0 < w) (hA : 1 ≤ A) (hρ : 1 < ρ) (hη : 0 < η) (hE : ∀ (r : ℕ) (j : Fin Q), μ.real (E r j) ≤ C * (w ^ r * Real.exp (-(A * ρ ^ r) ^ η))) : μ.real (⋃ (r : ℕ), ⋃ (j : Fin Q), E r j) ≤ ↑Q * C * (Real.exp (-A ^ η) * weightedGeometricExpKernelConst w (ρ ^ η))

Constant-row version of the weighted finite-union kernel bound.