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

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

Two-branch bad-scale tails

This file starts the theorem-facing bad-scale tail assembly. The first step is still fixed-pair: in the mixed bottom range, use the localized and crude mechanisms separately for the same selected scale and then keep the better of the two tails by taking the maximum of their stretched-exponential exponents.

theorem HCPolySupport.Book.Ch05.Section57.sub_nonneg_le_max_sub_left_of_le_max {x y z c : ℝ} (hc : 0 ≤ c) (h : x ≤ max y z) : x - c ≤ max (y - c) z

If a quantity is bounded by max y z, then subtracting a nonnegative offset only from the left branch still controls the offset quantity.

theorem HCPolySupport.Book.Ch05.Section57.rpow_three_row_parameter_div_eq {q r : ℕ} {offset row Den η : ℝ} (hη : 0 < η) : 3 ^ (↑q - offset / η) / Den * (3 ^ (row / η)) ^ r = 3 ^ ((η * ↑q - offset + row * ↑r) / η) / Den

Multiplicative row parameters written as a single triadic exponent.

theorem HCPolySupport.Book.Ch05.Section57.rpow_three_div_den_le_branch_max_of_exponent_le_max {X Xhigh Xcrude Dhigh Dcrude Den η τ σ : ℝ} (hη : 0 < η) (hτ : 0 < τ) (hσ : 0 < σ) (hDhigh : 0 < Dhigh) (hDcrude : 0 < Dcrude) (hDen : 0 < Den) (hDen_high : Dhigh ^ τ ≤ Den ^ η) (hDen_crude : Dcrude ^ σ ≤ Den ^ η) (hX : X ≤ max Xhigh Xcrude) : (3 ^ (X / η) / Den) ^ η ≤ max (max 1 (3 ^ (Xhigh / τ) / Dhigh) ^ τ) (max 1 (3 ^ (Xcrude / σ) / Dcrude) ^ σ)

Deterministic comparison turning an exponent-level maximum into a tail-parameter maximum, with explicit denominator domination.

theorem HCPolySupport.Book.Ch05.Section57.le_weighted_row_of_le_soft_maxExponent {x pref highA crudeA τ σ A ρ η C w : ℝ} {q r : ℕ} (hx : x ≤ max 1 pref * Real.exp (1 - max (max 1 highA ^ τ) (max 1 crudeA ^ σ))) (hpref : max 1 pref ≤ C * w ^ q * w ^ r) (hC : 0 ≤ C) (hw : 0 ≤ w) (hpow : (A * ρ ^ r) ^ η ≤ max (max 1 highA ^ τ) (max 1 crudeA ^ σ)) : x ≤ Real.exp 1 * C * w ^ q * (w ^ r * Real.exp (-(A * ρ ^ r) ^ η))

Convert a max-exponent soft fixed-pair estimate into the weighted row shape used by the bad-scale summation lemmas.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_shiftedHighBottomPairEvent_quenchedProbeEnvelope_le_soft_max_mixed {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 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 b := ↑d / 2; have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1); have tau := min σ 2; have pref := ↑S.card * ↑D.card; have highA := 3 ^ (b * ↑q - (b - t) * ↑(q - n) + (t - αbad) * ↑(m - q) - b * (L + 1)) / (2 * K * Cfluct * hΓ.thetaHat ^ 2); have crudeA := 3 ^ (t * ↑(q - n) + (t - αbad) * ↑(m - q)) / (K * Ccrude * hΓ.thetaHat ^ 2); n < m → q ≤ m → 0 < t → αbad < t → MeasureTheory.Measure.real P (highBottomPairEvent Hshift K a t αbad q m n) ≤ max 1 pref * Real.exp (1 - max (max 1 highA ^ tau) (max 1 crudeA ^ σ))

Exact fixed-pair mixed-bottom estimate with the better of the localized and crude mechanisms retained as a maximum of exponents.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_shiftedHighBottomPairProbability_le_interpolated_weighted_row {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Cfluct : ℝ) (Ccrude : ℝ) (Centry : ℝ) (a : ℝ), 0 < Cfluct ∧ 0 < Ccrude ∧ 0 < Centry ∧ 0 < a ∧ ∀ {t αbad Den : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → ∀ {q r : ℕ} {j : Fin (q + 1)}, have K := quenchedProbeEnvelopeConst d; have N0 := annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity Centry; have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (N0 + M) (N0 + N) aω; have S := Finset.univ; have b := ↑d / 2; have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1); have τ := finiteQuenchedTailTau σ; have η := finiteQuenchedTailExponent d σ t; have w := ↑(3 ^ d); have Dhigh := 2 * K * Cfluct * hΓ.thetaHat ^ 2; have Dcrude := K * Ccrude * hΓ.thetaHat ^ 2; have A := 3 ^ (↑q - τ * b * (L + 1) / η) / Den; have ρ := 3 ^ (τ * (t - αbad) / η); have Cpref := Real.exp 1 * max 1 ↑S.card; have m := q + r; have n := q - ↑j; 0 < t → t ≤ b → αbad < t → 0 < Den → Dhigh ^ τ ≤ Den ^ η → Dcrude ^ σ ≤ Den ^ η → MeasureTheory.Measure.real P (highBottomPairEvent Hshift K a t αbad q m n) ≤ Cpref * w ^ q * (w ^ r * Real.exp (-(A * ρ ^ r) ^ η))

Concrete mixed-bottom fixed-pair estimate in the weighted row shape, with the corrected finite bad-scale exponent. The only remaining denominator conditions are explicit algebraic domination conditions for the chosen normalizing denominator Den.

theorem HCPolySupport.Book.Ch05.Section57.shiftedHighBottomBadScaleProbability_le_interpolated_weighted_kernel {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Cfluct : ℝ) (Ccrude : ℝ) (Centry : ℝ) (a : ℝ), 0 < Cfluct ∧ 0 < Ccrude ∧ 0 < Centry ∧ 0 < a ∧ ∀ {t αbad Den : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → ∀ {q : ℕ}, have K := quenchedProbeEnvelopeConst d; have N0 := annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity Centry; have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (N0 + M) (N0 + N) aω; have S := Finset.univ; have b := ↑d / 2; have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1); have τ := finiteQuenchedTailTau σ; have η := finiteQuenchedTailExponent d σ t; have w := ↑(3 ^ d); have Dhigh := 2 * K * Cfluct * hΓ.thetaHat ^ 2; have Dcrude := K * Ccrude * hΓ.thetaHat ^ 2; have A := 3 ^ (↑q - τ * b * (L + 1) / η) / Den; have ρ := 3 ^ (τ * (t - αbad) / η); have Cpref := Real.exp 1 * max 1 ↑S.card; 0 < t → t ≤ b → αbad < t → 0 < Den → Dhigh ^ τ ≤ Den ^ η → Dcrude ^ σ ≤ Den ^ η → 1 ≤ A → MeasureTheory.Measure.real P (highBottomBadScaleEvent Hshift K a t αbad q) ≤ ↑(q + 1) * (Cpref * w ^ q) * (Real.exp (-A ^ η) * weightedGeometricExpKernelConst w (ρ ^ η))

Summed high-bottom component estimate with the corrected finite interpolated exponent, conditional only on the explicit denominator choice and the deterministic lower cutoff 1 <= A.