Coarse-graining support: Support.Book.Ch05.Theorems.Section57.BadScaleComponentRows #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Row estimates for split bad-scale components #
The lemmas in this file are deliberately small. They convert a fixed-pair tail bound, a deterministic lower bound on the tail parameter, and a descendant-cardinality estimate into the weighted row estimates needed by the component summation lemmas.
theorem
HCPolySupport.Book.Ch05.Section57.measureReal_highBottomPairEvent_le_weighted_row_of_badPair_bound
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{H : ℕ → ℕ → Ω → ℝ}
{K a t α : ℝ}
{q m n r : ℕ}
{S D A ρ τ lam w : ℝ}
(hS : 0 ≤ S)
(hw : 0 ≤ w)
(hD : D ≤ w ^ q * w ^ r)
(hAρ_nonneg : 0 ≤ A * ρ ^ r)
(hlam : A * ρ ^ r ≤ lam)
(hτ : 0 < τ)
(hbad : μ.real (badPairEvent H t α q m n) ≤ S * (D * Real.exp (-lam ^ τ)))
:
High-bottom row estimate from a fixed-pair no-log bound and deterministic weight estimates.
theorem
HCPolySupport.Book.Ch05.Section57.measureReal_crudeBottomPairEvent_le_weighted_row_of_badPair_bound
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{H : ℕ → ℕ → Ω → ℝ}
{K a t α : ℝ}
{q m n r : ℕ}
{S D A ρ σ lam w : ℝ}
(hS : 0 ≤ S)
(hw : 0 ≤ w)
(hD : D ≤ w ^ q * w ^ r)
(hAρ_nonneg : 0 ≤ A * ρ ^ r)
(hlam : A * ρ ^ r ≤ lam)
(hσ : 0 < σ)
(hbad : μ.real (badPairEvent H t α q m n) ≤ S * (D * Real.exp (-lam ^ σ)))
:
Crude-bottom row estimate from a fixed-pair crude bound and deterministic weight estimates.