Coarse-graining support: Support.Book.Ch05.Theorems.Section57.UniformBadScaleTail #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Uniform endpoint bad-scale tail #
This file assembles the Γ∞ endpoint bad-scale estimate with synchronized
constants. The endpoint exponent is d, not the finite-σ interpolation.
theorem
HCPolySupport.Book.Ch05.Section57.measureReal_shiftedHighTopBadScaleProbability_le_weighted_kernel_gammaInfinity
{d : ℕ}
[NeZero d]
{Cfluct Centry a : ℝ}
(params : QuantitativeCoarseGrainedEllipticityParams d)
(hCfluct : 0 < Cfluct)
(_hCentry : 0 < Centry)
(ha : 0 < a)
(hraw :
∀ {t αbad : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct),
hΓ.sigma = 2 →
hΓ.params = params →
∀ {q m n : ℕ},
have K := quenchedProbeEnvelopeConst d;
have x := αbad * ↑(m - q) - t * ↑(m - n);
have ell := ⌈(a * Real.log 3)⁻¹ * (Real.log (max (2 * K) 1) + x * Real.log 3)⌉₊;
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 2;
have scale := Cfluct * 3 ^ (-↑d / 2 * ↑(n - ell)) * hΓ.thetaHat ^ 2;
have T := Real.rpow 3 (-x);
have lam := T / (2 * K * scale);
ell < n →
n < m →
q ≤ m →
1 ≤ lam →
MeasureTheory.Measure.real P (badPairEvent Hshift t αbad q m n) ≤ ↑S.card * (↑D.card * Real.exp (-lam ^ tau)))
{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 ctop := min (t - αbad) (min (b - αbad) (min ((t - αbad) * (1 + b / a)) (b - αbad * (1 + b / a))));
have η := ↑d;
have w := ↑(3 ^ d);
have Dhigh := 2 * K * Cfluct * hInf.thetaHat ^ 2;
have A := 3 ^ (↑q - (L + 1)) / Den;
have ρtop := 3 ^ ctop;
0 < t →
αbad < t →
αbad < b →
αbad * (1 + b / a) < b →
0 < Den →
Dhigh ^ 2 ≤ Den ^ η →
1 ≤ A →
MeasureTheory.Measure.real P (highTopBadScaleEvent Hshift K a t αbad q) ≤ ↑S.card * (Real.exp (-A ^ η) * weightedLinearExpKernelConst w (ρtop ^ 2))
Endpoint high-top component estimate with the raw high bad-pair bound supplied externally.
theorem
HCPolySupport.Book.Ch05.Section57.measureReal_shiftedBadScaleEvent_quenchedProbeEnvelope_le_uniformEndpoint_component_sum
{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 ctop := min (t - αbad) (min (b - αbad) (min ((t - αbad) * (1 + b / a)) (b - αbad * (1 + b / a))));
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 Acrude := 3 ^ (t * ↑q - t * (L + 1)) / Dcrude;
have ρtop := 3 ^ ctop;
have ρbottom := 3 ^ (2 * (t - αbad) / η);
have Cbottom := Real.exp 1 * max 1 ↑S.card;
0 < t →
0 ≤ αbad →
αbad < t →
αbad < b →
αbad * (1 + b / a) < b →
αbad < a →
t ≤ b →
0 < Den →
Dhigh ^ 2 ≤ Den ^ η →
Dhigh ^ 2 * max 1 Dcrude ^ ((↑d - 2 * t) / t) ≤ Den ^ η →
1 ≤ A →
1 ≤ Acrude →
(have Lcut := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1);
Lcut + 1 < (1 - αbad / a) * ↑q) →
MeasureTheory.Measure.real P (badScaleEvent Hshift t αbad q) ≤ ↑S.card * (Real.exp (-A ^ η) * weightedLinearExpKernelConst w (ρtop ^ 2)) + ↑(q + 1) * (Cbottom * w ^ q) * (Real.exp (-A ^ η) * weightedGeometricExpKernelConst w (ρbottom ^ η))
Synchronized endpoint bad-scale component sum before deterministic threshold selection.
theorem
HCPolySupport.Book.Ch05.Section57.measureReal_shiftedBadScaleEvent_quenchedProbeEnvelope_le_uniformEndpoint_selected_denominator
{d : ℕ}
[NeZero d]
(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) (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 ctop := min (t - αbad) (min (b - αbad) (min ((t - αbad) * (1 + b / a)) (b - αbad * (1 + b / a))));
have η := ↑d;
have w := ↑(3 ^ d);
have Dhigh := 2 * K * Cfluct * hInf.thetaHat ^ 2;
have Dcrude := K * Ccrude * hInf.thetaHat ^ 2;
have Den := uniformEndpointHighDenominator Dhigh Dcrude t η;
have A := 3 ^ (↑q - (L + 1)) / Den;
have Acrude := 3 ^ (t * ↑q - t * (L + 1)) / Dcrude;
have ρtop := 3 ^ ctop;
have ρbottom := 3 ^ (2 * (t - αbad) / η);
have Cbottom := Real.exp 1 * max 1 ↑S.card;
0 < t →
0 ≤ αbad →
αbad < t →
αbad < b →
αbad * (1 + b / a) < b →
αbad < a →
t ≤ b →
1 ≤ A →
1 ≤ Acrude →
(have Lcut := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1);
Lcut + 1 < (1 - αbad / a) * ↑q) →
MeasureTheory.Measure.real P (badScaleEvent Hshift t αbad q) ≤ ↑S.card * (Real.exp (-A ^ η) * weightedLinearExpKernelConst w (ρtop ^ 2)) + ↑(q + 1) * (Cbottom * w ^ q) * (Real.exp (-A ^ η) * weightedGeometricExpKernelConst w (ρbottom ^ η))
Endpoint component sum after selecting the common high denominator. The crude-bottom cutoff remains an explicit deterministic side condition.