Coarse-graining support: Support.Book.Ch05.Theorems.Section57.BadScaleComponentSummation #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Summing split bad-scale components #
This file begins the passage from fixed-pair component estimates to bad-scale component estimates. The high-top branch has one geometric direction and one finite row multiplicity, so it uses the linear kernel union bound.
theorem
HCPolySupport.Book.Ch05.Section57.highTopBadScaleEvent_subset_linearRows
{Ω : Type u_1}
{H : ℕ → ℕ → Ω → ℝ}
{K a t α : ℝ}
{q : ℕ}
:
highTopBadScaleEvent H K a t α q ⊆ ⋃ (r : ℕ), ⋃ (j : Fin (r + 1)), highTopPairEvent H K a t α q (q + r) (q + ↑j)
theorem
HCPolySupport.Book.Ch05.Section57.highBottomBadScaleEvent_subset_constRows
{Ω : Type u_1}
{H : ℕ → ℕ → Ω → ℝ}
{K a t α : ℝ}
{q : ℕ}
:
highBottomBadScaleEvent H K a t α q ⊆ ⋃ (r : ℕ), ⋃ (j : Fin (q + 1)), highBottomPairEvent H K a t α q (q + r) (q - ↑j)
theorem
HCPolySupport.Book.Ch05.Section57.crudeBottomBadScaleEvent_subset_constRows
{Ω : Type u_1}
{H : ℕ → ℕ → Ω → ℝ}
{K a t α : ℝ}
{q : ℕ}
:
crudeBottomBadScaleEvent H K a t α q ⊆ ⋃ (r : ℕ), ⋃ (j : Fin (q + 1)), crudeBottomPairEvent H K a t α q (q + r) (q - ↑j)
theorem
HCPolySupport.Book.Ch05.Section57.measureReal_highTopBadScaleEvent_le_exp_linear_kernel_of_reindexed_bound
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{H : ℕ → ℕ → Ω → ℝ}
{K a t α : ℝ}
{q : ℕ}
{A ρ η C : ℝ}
(hC : 0 ≤ C)
(hA : 1 ≤ A)
(hρ : 1 < ρ)
(hη : 0 < η)
(hpair :
∀ (r : ℕ) (j : Fin (r + 1)), μ.real (highTopPairEvent H K a t α q (q + r) (q + ↑j)) ≤ C * Real.exp (-(A * ρ ^ r) ^ η))
:
theorem
HCPolySupport.Book.Ch05.Section57.measureReal_highTopBadScaleEvent_le_weighted_exp_linear_kernel_of_reindexed_bound
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{H : ℕ → ℕ → Ω → ℝ}
{K a t α : ℝ}
{q : ℕ}
{A ρ η C w : ℝ}
(hC : 0 ≤ C)
(hw : 0 < w)
(hA : 1 ≤ A)
(hρ : 1 < ρ)
(hη : 0 < η)
(hpair :
∀ (r : ℕ) (j : Fin (r + 1)),
μ.real (highTopPairEvent H K a t α q (q + r) (q + ↑j)) ≤ C * (w ^ r * Real.exp (-(A * ρ ^ r) ^ η)))
:
μ.real (highTopBadScaleEvent H K a t α q) ≤ C * (Real.exp (-A ^ η) * weightedLinearExpKernelConst w (ρ ^ η))
Weighted high-top summation. This is the no-loss version of the
linear-row component bound: the row-dependent finite-union prefactor is carried
as w ^ r and absorbed only by the weighted kernel.
theorem
HCPolySupport.Book.Ch05.Section57.measureReal_highBottomBadScaleEvent_le_exp_constRows_kernel_of_reindexed_bound
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{H : ℕ → ℕ → Ω → ℝ}
{K a t α : ℝ}
{q : ℕ}
{A ρ η C : ℝ}
(hC : 0 ≤ C)
(hA : 1 ≤ A)
(hρ : 1 < ρ)
(hη : 0 < η)
(hpair :
∀ (r : ℕ) (j : Fin (q + 1)),
μ.real (highBottomPairEvent H K a t α q (q + r) (q - ↑j)) ≤ C * Real.exp (-(A * ρ ^ r) ^ η))
:
theorem
HCPolySupport.Book.Ch05.Section57.measureReal_highBottomBadScaleEvent_le_weighted_exp_constRows_kernel_of_reindexed_bound
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{H : ℕ → ℕ → Ω → ℝ}
{K a t α : ℝ}
{q : ℕ}
{A ρ η C w : ℝ}
(hC : 0 ≤ C)
(hw : 0 < w)
(hA : 1 ≤ A)
(hρ : 1 < ρ)
(hη : 0 < η)
(hpair :
∀ (r : ℕ) (j : Fin (q + 1)),
μ.real (highBottomPairEvent H K a t α q (q + r) (q - ↑j)) ≤ C * (w ^ r * Real.exp (-(A * ρ ^ r) ^ η)))
:
Weighted high-bottom summation with a fixed finite row size.
theorem
HCPolySupport.Book.Ch05.Section57.measureReal_crudeBottomBadScaleEvent_le_exp_constRows_kernel_of_reindexed_bound
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{H : ℕ → ℕ → Ω → ℝ}
{K a t α : ℝ}
{q : ℕ}
{A ρ η C : ℝ}
(hC : 0 ≤ C)
(hA : 1 ≤ A)
(hρ : 1 < ρ)
(hη : 0 < η)
(hpair :
∀ (r : ℕ) (j : Fin (q + 1)),
μ.real (crudeBottomPairEvent H K a t α q (q + r) (q - ↑j)) ≤ C * Real.exp (-(A * ρ ^ r) ^ η))
:
theorem
HCPolySupport.Book.Ch05.Section57.measureReal_crudeBottomBadScaleEvent_le_weighted_exp_constRows_kernel_of_reindexed_bound
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{H : ℕ → ℕ → Ω → ℝ}
{K a t α : ℝ}
{q : ℕ}
{A ρ η C w : ℝ}
(hC : 0 ≤ C)
(hw : 0 < w)
(hA : 1 ≤ A)
(hρ : 1 < ρ)
(hη : 0 < η)
(hpair :
∀ (r : ℕ) (j : Fin (q + 1)),
μ.real (crudeBottomPairEvent H K a t α q (q + r) (q - ↑j)) ≤ C * (w ^ r * Real.exp (-(A * ρ ^ r) ^ η)))
:
Weighted crude-bottom summation with a fixed finite row size.