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

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

Collapse of synchronized bad-scale components to one tail

This file contains the deterministic final step after the three bad-scale components have been estimated with synchronized constants. The probabilistic input is the selected-denominator component theorem from BadScaleTailJoint; the remaining hypotheses are purely large-scale/prefactor inequalities.

theorem HCPolySupport.Book.Ch05.Section57.three_exp_terms_le_exp_of_prefactor_gap {c₁ c₂ c₃ A Ac T₀ T : ℝ} (hc₁ : 0 ≤ c₁) (hc₂ : 0 ≤ c₂) (hc₃ : 0 ≤ c₃) (hA : T₀ ≤ A) (hAc : T₀ ≤ Ac) (hpref : c₁ + c₂ + c₃ ≤ Real.exp (T₀ - T)) : c₁ * Real.exp (-A) + c₂ * Real.exp (-A) + c₃ * Real.exp (-Ac) ≤ Real.exp (-T)

theorem HCPolySupport.Book.Ch05.Section57.rpow_three_sub_div_eq_div_mul_rpow {x O Den : ℝ} (hDen : Den ≠ 0) : 3 ^ (x - O) / Den = 3 ^ x / (Den * 3 ^ O)

theorem HCPolySupport.Book.Ch05.Section57.rpow_div_le_rpow_div_of_den_le {x D₁ D₂ η : ℝ} (hx : 0 ≤ x) (hD₁ : 0 < D₁) (hD₂ : 0 < D₂) (hD : D₁ ≤ D₂) (hη : 0 < η) : (x / D₂) ^ η ≤ (x / D₁) ^ η

theorem HCPolySupport.Book.Ch05.Section57.selected_tail_parameter_power_le_high {q : ℕ} {Den B η O : ℝ} (hDen : 0 < Den) (hB : 0 < B) (hη : 0 < η) (hden : Den * 3 ^ O ≤ B) : (3 ^ ↑q / B) ^ η ≤ (3 ^ (↑q - O) / Den) ^ η

theorem HCPolySupport.Book.Ch05.Section57.measureReal_badScaleEvent_le_exp_tail_of_component_prefactor_gap {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {H : ℕ → ℕ → Ω → ℝ} {t α : ℝ} {q : ℕ} {Ctop ChighBottom CcrudeBottom A Acrude Alead Atail η : ℝ} (hcomponent : μ.real (badScaleEvent H t α q) ≤ Ctop * Real.exp (-A ^ η) + ChighBottom * Real.exp (-A ^ η) + CcrudeBottom * Real.exp (-Acrude ^ η)) (hAlead_A : Alead ≤ A ^ η) (hAlead_Acrude : Alead ≤ Acrude ^ η) (hpref : max 0 Ctop + max 0 ChighBottom + max 0 CcrudeBottom ≤ Real.exp (Alead - Atail)) : μ.real (badScaleEvent H t α q) ≤ Real.exp (-Atail)

Deterministic component collapse in the exact algebraic shape produced by the synchronized selected-denominator estimate.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_badScaleEvent_le_exp_tail_of_selected_component_sum {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {H : ℕ → ℕ → Ω → ℝ} {t α : ℝ} {q : ℕ} {S qPlus Cbottom wq Ktop Kbottom Kcrude A Acrude Alead Atail η : ℝ} (hcomponent : μ.real (badScaleEvent H t α q) ≤ S * (Real.exp (-A ^ η) * Ktop) + qPlus * (Cbottom * wq) * (Real.exp (-A ^ η) * Kbottom) + qPlus * (S * wq) * (Real.exp (-Acrude ^ η) * Kcrude)) (hAlead_A : Alead ≤ A ^ η) (hAlead_Acrude : Alead ≤ Acrude ^ η) (hpref : max 0 (S * Ktop) + max 0 (qPlus * (Cbottom * wq) * Kbottom) + max 0 (qPlus * (S * wq) * Kcrude) ≤ Real.exp (Alead - Atail)) : μ.real (badScaleEvent H t α q) ≤ Real.exp (-Atail)

Same deterministic collapse, with the component sum written in the selected-denominator theorem's native factorization.