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

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

Assembling the bad-scale tail from the split components

This file combines the sharp bad-scale split with the component estimates. It contains no new probabilistic input: the only ingredients are the four-way union bound and the deterministic crude-top cutoff.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_badScaleEvent_le_of_component_bounds {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {H : ℕ → ℕ → Ω → ℝ} {K a t α : ℝ} {q : ℕ} {Rht Rhb Rcb Rct : ℝ} (hht : μ.real (highTopBadScaleEvent H K a t α q) ≤ Rht) (hhb : μ.real (highBottomBadScaleEvent H K a t α q) ≤ Rhb) (hcb : μ.real (crudeBottomBadScaleEvent H K a t α q) ≤ Rcb) (hct : μ.real (crudeTopBadScaleEvent H K a t α q) ≤ Rct) : μ.real (badScaleEvent H t α q) ≤ Rht + Rhb + Rcb + Rct

Pure assembly of the four split branches of a bad-scale event.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_badScaleEvent_le_of_component_bounds_crudeTop_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {H : ℕ → ℕ → Ω → ℝ} {K a t α : ℝ} {q : ℕ} {Rht Rhb Rcb : ℝ} (hht : μ.real (highTopBadScaleEvent H K a t α q) ≤ Rht) (hhb : μ.real (highBottomBadScaleEvent H K a t α q) ≤ Rhb) (hcb : μ.real (crudeBottomBadScaleEvent H K a t α q) ≤ Rcb) (hct : μ.real (crudeTopBadScaleEvent H K a t α q) = 0) : μ.real (badScaleEvent H t α q) ≤ Rht + Rhb + Rcb

Assembly of the full bad-scale event when the crude-top branch is empty.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_badScaleEvent_le_of_component_kernels_and_crudeTop_cutoff {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {H : ℕ → ℕ → Ω → ℝ} {K a t α : ℝ} {q : ℕ} {Rht Rhb Rcb : ℝ} (ha : 0 < a) (hα_nonneg : 0 ≤ α) (hαt : α < t) (hαa : α < a) (hq_large : have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1); L + 1 < (1 - α / a) * ↑q) (hht : μ.real (highTopBadScaleEvent H K a t α q) ≤ Rht) (hhb : μ.real (highBottomBadScaleEvent H K a t α q) ≤ Rhb) (hcb : μ.real (crudeBottomBadScaleEvent H K a t α q) ≤ Rcb) : μ.real (badScaleEvent H t α q) ≤ Rht + Rhb + Rcb

Full bad-scale bound from the three quantitative component bounds and the deterministic crude-top cutoff.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_badScaleEvent_le_kernel_sum_of_component_kernels {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {H : ℕ → ℕ → Ω → ℝ} {K a t α : ℝ} {q : ℕ} {Aht ρht τ Ahb ρhb Acb ρcb σ : ℝ} (ha : 0 < a) (hα_nonneg : 0 ≤ α) (hαt : α < t) (hαa : α < a) (hq_large : have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1); L + 1 < (1 - α / a) * ↑q) (hht : μ.real (highTopBadScaleEvent H K a t α q) ≤ Real.exp 1 * (Real.exp (-Aht ^ τ) * linearExpKernelConst ρht τ)) (hhb : μ.real (highBottomBadScaleEvent H K a t α q) ≤ ↑(q + 1) * Real.exp 1 * (Real.exp (-Ahb ^ τ) * geometricExpKernelConst ρhb τ)) (hcb : μ.real (crudeBottomBadScaleEvent H K a t α q) ≤ ↑(q + 1) * Real.exp 1 * (Real.exp (-Acb ^ σ) * geometricExpKernelConst ρcb σ)) : μ.real (badScaleEvent H t α q) ≤ Real.exp 1 * (Real.exp (-Aht ^ τ) * linearExpKernelConst ρht τ) + ↑(q + 1) * Real.exp 1 * (Real.exp (-Ahb ^ τ) * geometricExpKernelConst ρhb τ) + ↑(q + 1) * Real.exp 1 * (Real.exp (-Acb ^ σ) * geometricExpKernelConst ρcb σ)

Kernel-shaped assembly of the full bad-scale event. This is the manuscript four-way split after the crude-top component has been cut off: the right side is exactly the sum of the three surviving branch bounds.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_badScaleEvent_le_weighted_kernel_sum_of_component_kernels {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {H : ℕ → ℕ → Ω → ℝ} {K a t α : ℝ} {q : ℕ} {Aht ρht Ahb ρhb Acb ρcb ηhigh ηcrude Cht Chb Ccb w : ℝ} (ha : 0 < a) (hα_nonneg : 0 ≤ α) (hαt : α < t) (hαa : α < a) (hq_large : have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1); L + 1 < (1 - α / a) * ↑q) (hht : μ.real (highTopBadScaleEvent H K a t α q) ≤ Cht * (Real.exp (-Aht ^ ηhigh) * weightedLinearExpKernelConst w (ρht ^ ηhigh))) (hhb : μ.real (highBottomBadScaleEvent H K a t α q) ≤ Chb * (Real.exp (-Ahb ^ ηhigh) * weightedGeometricExpKernelConst w (ρhb ^ ηhigh))) (hcb : μ.real (crudeBottomBadScaleEvent H K a t α q) ≤ Ccb * (Real.exp (-Acb ^ ηcrude) * weightedGeometricExpKernelConst w (ρcb ^ ηcrude))) : μ.real (badScaleEvent H t α q) ≤ Cht * (Real.exp (-Aht ^ ηhigh) * weightedLinearExpKernelConst w (ρht ^ ηhigh)) + Chb * (Real.exp (-Ahb ^ ηhigh) * weightedGeometricExpKernelConst w (ρhb ^ ηhigh)) + Ccb * (Real.exp (-Acb ^ ηcrude) * weightedGeometricExpKernelConst w (ρcb ^ ηcrude))

Weighted-kernel assembly of the full bad-scale event. This is the no-log version used in the current proof: the finite maxima remain in the component constants, while the row weights are absorbed by the weighted superexponential kernels.