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

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

The mixed high-bottom branch at the uniform endpoint

The endpoint high-bottom branch keeps the localized Γ_2 concentration mechanism and adds the deterministic Γ_∞ crude cutoff. The final row collapse is built on these two separate inputs.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_shiftedHighBottomPairEvent_quenchedProbeEnvelope_le_soft_high_gammaInfinity {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Cfluct : ℝ) (Centry : ℝ) (a : ℝ), 0 < Cfluct ∧ 0 < Centry ∧ 0 < a ∧ ∀ {t αbad : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct), hInf.params = params → ∀ {q m n : ℕ}, have K := quenchedProbeEnvelopeConst d; have N0 := annealedAlgebraicEntryScale P hInf.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 pref := ↑S.card * ↑D.card; have highA := 3 ^ (b * ↑q - (b - t) * ↑(q - n) + (t - αbad) * ↑(m - q) - b * (L + 1)) / (2 * K * Cfluct * hInf.thetaHat ^ 2); n < m → q ≤ m → 0 < t → αbad < t → MeasureTheory.Measure.real P (highBottomPairEvent Hshift K a t αbad q m n) ≤ softPairTail pref highA 2

The localized high estimate in the high-bottom branch, specialized to the uniform endpoint by forgetting Γ_∞ to finite Γ_2.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_shiftedHighBottomPairEvent_quenchedProbeEnvelope_eq_zero_of_crudeA_one_gammaInfinity {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Ccrude : ℝ), 0 < Ccrude ∧ ∀ {Centry a t αbad : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct), hInf.params = params → ∀ {q m n : ℕ}, have K := quenchedProbeEnvelopeConst d; have N0 := annealedAlgebraicEntryScale P hInf.toQuantitativeCoarseGrainedEllipticity Centry; have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (N0 + M) (N0 + N) aω; have crudeA := 3 ^ (t * ↑(q - n) + (t - αbad) * ↑(m - q)) / (K * Ccrude * hInf.thetaHat ^ 2); n < m → q ≤ m → n ≤ q → αbad < t → 1 ≤ crudeA → MeasureTheory.Measure.real P (highBottomPairEvent Hshift K a t αbad q m n) = 0

The deterministic crude cutoff in the high-bottom branch. If the crude tail parameter is at least one, the bad-pair event, hence the high-bottom subevent, has zero probability.

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

Convert a one-branch softened fixed-pair estimate into the weighted row shape used by the endpoint bottom summation.

theorem HCPolySupport.Book.Ch05.Section57.uniformEndpoint_highBottom_tailParameter_rpow_le_high {d q r : ℕ} [NeZero d] {j : Fin (q + 1)} {t α L Dhigh Dcrude Den : ℝ} (ht : 0 < t) (hαt : α < t) (htb : t ≤ ↑d / 2) (hDhigh : 0 < Dhigh) (hDcrude : 0 < Dcrude) (hDen : 0 < Den) (hDen_dom : Dhigh ^ 2 * max 1 Dcrude ^ ((↑d - 2 * t) / t) ≤ Den ^ ↑d) (hcrude : 3 ^ (t * ↑(q - (q - ↑j)) + (t - α) * ↑(q + r - q)) / Dcrude < 1) : have b := ↑d / 2; have m := q + r; have n := q - ↑j; have highA := 3 ^ (b * ↑q - (b - t) * ↑(q - n) + (t - α) * ↑(m - q) - b * (L + 1)) / Dhigh; have A := 3 ^ (↑q - (L + 1)) / Den; have ρ := 3 ^ (2 * (t - α) / ↑d); (A * ρ ^ r) ^ ↑d ≤ max 1 highA ^ 2

Endpoint high-bottom deterministic tail-parameter comparison.

When the crude cutoff has not fired, the crude denominator pays for the missing high-branch factor 3 ^ ((d - 2t) * (q - n)).

theorem HCPolySupport.Book.Ch05.Section57.measureReal_shiftedHighBottomPairEvent_quenchedProbeEnvelope_le_weighted_row_gammaInfinity {d : ℕ} [NeZero d] (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) (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct), hInf.params = params → ∀ {q r : ℕ} {j : Fin (q + 1)}, have K := quenchedProbeEnvelopeConst d; have N0 := annealedAlgebraicEntryScale P hInf.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 η := ↑d; have w := ↑(3 ^ d); have Dhigh := 2 * K * Cfluct * hInf.thetaHat ^ 2; have Dcrude := K * Ccrude * hInf.thetaHat ^ 2; have A := 3 ^ (↑q - (L + 1)) / Den; have ρ := 3 ^ (2 * (t - αbad) / η); have Cpref := Real.exp 1 * max 1 ↑S.card; have m := q + r; have n := q - ↑j; 0 < t → αbad < t → t ≤ b → 0 < Den → Dhigh ^ 2 * max 1 Dcrude ^ ((↑d - 2 * t) / t) ≤ Den ^ η → MeasureTheory.Measure.real P (highBottomPairEvent Hshift K a t αbad q m n) ≤ Cpref * w ^ q * (w ^ r * Real.exp (-(A * ρ ^ r) ^ η))

Endpoint high-bottom fixed row estimate. The only side condition is the explicit domination of the high denominator and the crude cutoff denominator by the selected endpoint denominator.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_shiftedHighBottomBadScaleEvent_quenchedProbeEnvelope_le_weighted_kernel_gammaInfinity {d : ℕ} [NeZero d] (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) (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct), hInf.params = params → ∀ {q : ℕ}, have K := quenchedProbeEnvelopeConst d; have N0 := annealedAlgebraicEntryScale P hInf.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 η := ↑d; have w := ↑(3 ^ d); have Dhigh := 2 * K * Cfluct * hInf.thetaHat ^ 2; have Dcrude := K * Ccrude * hInf.thetaHat ^ 2; have A := 3 ^ (↑q - (L + 1)) / Den; have ρ := 3 ^ (2 * (t - αbad) / η); have Cpref := Real.exp 1 * max 1 ↑S.card; 0 < t → αbad < t → t ≤ b → 0 < Den → Dhigh ^ 2 * max 1 Dcrude ^ ((↑d - 2 * t) / t) ≤ Den ^ η → 1 ≤ A → MeasureTheory.Measure.real P (highBottomBadScaleEvent Hshift K a t αbad q) ≤ ↑(q + 1) * (Cpref * w ^ q) * (Real.exp (-A ^ η) * weightedGeometricExpKernelConst w (ρ ^ η))

Endpoint high-bottom component estimate after summing the fixed rows.