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

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

Fixed-pair two-branch bad-scale estimates

This file starts the note-facing bad-scale proof at the fixed-pair level. A bad pair is split into the localized branch, where the selected intermediate scale lies below n, and the crude branch, where it does not. The concrete estimate at the end uses the actual Section 5.7 localized and crude tail inputs; it does not assume the desired bad-scale tail.

def HCPolySupport.Book.Ch05.Section57.highPairBranchEvent {Ω : Type u_1} (H : ℕ → ℕ → Ω → ℝ) (K a t α : ℝ) (q m n : ℕ) : Set Ω

Fixed-pair localized branch: the selected intermediate scale is below n.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.Book.Ch05.Section57.crudePairBranchEvent {Ω : Type u_1} (H : ℕ → ℕ → Ω → ℝ) (K a t α : ℝ) (q m n : ℕ) : Set Ω

Fixed-pair crude branch: the selected intermediate scale is not below n.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch05.Section57.badPairEvent_subset_pair_branch_union {Ω : Type u_1} {H : ℕ → ℕ → Ω → ℝ} {K a t α : ℝ} {q m n : ℕ} : badPairEvent H t α q m n ⊆ highPairBranchEvent H K a t α q m n ∪ crudePairBranchEvent H K a t α q m n

noncomputable def HCPolySupport.Book.Ch05.Section57.softPairTail (pref lam η : ℝ) : ℝ

A softened fixed-pair tail. If the tail parameter is below one this is just a probability-one bound; if it is at least one it is the usual exponential tail, with a harmless factor exp 1 folded in.

Equations

• HCPolySupport.Book.Ch05.Section57.softPairTail pref lam η = max 1 pref * Real.exp (1 - max 1 lam ^ η)

theorem HCPolySupport.Book.Ch05.Section57.softPairTail_nonneg {pref lam η : ℝ} : 0 ≤ softPairTail pref lam η

theorem HCPolySupport.Book.Ch05.Section57.one_le_softPairTail_of_not_one_le_lam {pref lam η : ℝ} (hlam : ¬1 ≤ lam) : 1 ≤ softPairTail pref lam η

theorem HCPolySupport.Book.Ch05.Section57.pref_mul_exp_le_softPairTail_of_one_le_lam {pref lam η : ℝ} (_hpref : 0 ≤ pref) (hlam : 1 ≤ lam) : pref * Real.exp (-lam ^ η) ≤ softPairTail pref lam η

theorem HCPolySupport.Book.Ch05.Section57.softPairTail_mono_lam {pref lam₁ lam₂ η : ℝ} (hη : 0 < η) (hlam : lam₁ ≤ lam₂) : softPairTail pref lam₂ η ≤ softPairTail pref lam₁ η

theorem HCPolySupport.Book.Ch05.Section57.min_softPairTail_le_maxExponent {pref lam₁ lam₂ η₁ η₂ : ℝ} : min (softPairTail pref lam₁ η₁) (softPairTail pref lam₂ η₂) ≤ max 1 pref * Real.exp (1 - max (max 1 lam₁ ^ η₁) (max 1 lam₂ ^ η₂))

Taking the better of two soft fixed-pair tails replaces the two exponents by their maximum.

theorem HCPolySupport.Book.Ch05.Section57.le_maxExponent_softPairTail_of_le_both {x pref lam₁ lam₂ η₁ η₂ : ℝ} (h₁ : x ≤ softPairTail pref lam₁ η₁) (h₂ : x ≤ softPairTail pref lam₂ η₂) : x ≤ max 1 pref * Real.exp (1 - max (max 1 lam₁ ^ η₁) (max 1 lam₂ ^ η₂))

theorem HCPolySupport.Book.Ch05.Section57.measureReal_highPairBranchEvent_le_softTail {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {H : ℕ → ℕ → Ω → ℝ} {K a t α : ℝ} {q m n : ℕ} {pref lam η : ℝ} (hpref : 0 ≤ pref) (htail : selectedBadPairScale K a t α q m n < n → 1 ≤ lam → μ.real (badPairEvent H t α q m n) ≤ pref * Real.exp (-lam ^ η)) : μ.real (highPairBranchEvent H K a t α q m n) ≤ softPairTail pref lam η

theorem HCPolySupport.Book.Ch05.Section57.measureReal_crudePairBranchEvent_le_softTail {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {H : ℕ → ℕ → Ω → ℝ} {K a t α : ℝ} {q m n : ℕ} {pref lam η : ℝ} (hpref : 0 ≤ pref) (htail : n ≤ selectedBadPairScale K a t α q m n → 1 ≤ lam → μ.real (badPairEvent H t α q m n) ≤ pref * Real.exp (-lam ^ η)) : μ.real (crudePairBranchEvent H K a t α q m n) ≤ softPairTail pref lam η

theorem HCPolySupport.Book.Ch05.Section57.measureReal_badPairEvent_le_soft_two_branch {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {H : ℕ → ℕ → Ω → ℝ} {K a t α : ℝ} {q m n : ℕ} {prefHigh lamHigh ηHigh prefCrude lamCrude ηCrude : ℝ} (hprefHigh : 0 ≤ prefHigh) (hprefCrude : 0 ≤ prefCrude) (hhigh : selectedBadPairScale K a t α q m n < n → 1 ≤ lamHigh → μ.real (badPairEvent H t α q m n) ≤ prefHigh * Real.exp (-lamHigh ^ ηHigh)) (hcrude : n ≤ selectedBadPairScale K a t α q m n → 1 ≤ lamCrude → μ.real (badPairEvent H t α q m n) ≤ prefCrude * Real.exp (-lamCrude ^ ηCrude)) : μ.real (badPairEvent H t α q m n) ≤ softPairTail prefHigh lamHigh ηHigh + softPairTail prefCrude lamCrude ηCrude

theorem HCPolySupport.Book.Ch05.Section57.measureReal_shiftedBadPairEvent_quenchedProbeEnvelope_le_soft_two_branch {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Cfluct : ℝ) (Ccrude : ℝ) (Centry : ℝ) (a : ℝ), 0 < Cfluct ∧ 0 < Ccrude ∧ 0 < Centry ∧ 0 < a ∧ ∀ {t αbad : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → ∀ {q m n : ℕ}, have K := quenchedProbeEnvelopeConst d; have x := αbad * ↑(m - q) - t * ↑(m - n); have ell := selectedBadPairScale K a t αbad q m n; have N0 := annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity Centry; have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (N0 + M) (N0 + N) aω; have D := descendantsAtScale (originCube d ↑(N0 + m)) ↑(N0 + n); have S := Finset.univ; have tau := min σ 2; have highScale := Cfluct * 3 ^ (-↑d / 2 * ↑(n - ell)) * hΓ.thetaHat ^ 2; have T := Real.rpow 3 (-x); have highLam := T / (2 * K * highScale); have crudeScale := K * (Ccrude * hΓ.thetaHat ^ 2); have crudeLam := T / crudeScale; have pref := ↑S.card * ↑D.card; n < m → q ≤ m → MeasureTheory.Measure.real P (badPairEvent Hshift t αbad q m n) ≤ softPairTail pref highLam tau + softPairTail pref crudeLam σ

Concrete fixed-pair two-branch estimate for the shifted finite-probe envelope. The two branches are still expressed with their raw tail parameters; the next deterministic step lowers these parameters to the manuscript 3^(b*q) and 3^(t*q) scales before summing.