Coarse-graining support: Support.Book.Ch05.Theorems.Section57.UniformBadScaleTailCollapse #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Collapse of the uniform endpoint bad-scale tail #
This file turns the synchronized endpoint component estimate into one
stretched-exponential bad-scale tail with exponent d, up to explicit
deterministic threshold and prefactor-gap conditions.
theorem
HCPolySupport.Book.Ch05.Section57.measureReal_badScaleEvent_le_exp_tail_of_uniformEndpoint_component_sum
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{H : ℕ → ℕ → Ω → ℝ}
{t α : ℝ}
{q : ℕ}
{S qPlus Cbottom wq Ktop Kbottom A Alead Atail η : ℝ}
(hcomponent :
μ.real (badScaleEvent H t α q) ≤ S * (Real.exp (-A ^ η) * Ktop) + qPlus * (Cbottom * wq) * (Real.exp (-A ^ η) * Kbottom))
(hAlead_A : Alead ≤ A ^ η)
(hpref : max 0 (S * Ktop) + max 0 (qPlus * (Cbottom * wq) * Kbottom) ≤ Real.exp (Alead - Atail))
:
theorem
HCPolySupport.Book.Ch05.Section57.measureReal_shiftedBadScaleEvent_quenchedProbeEnvelope_le_uniformEndpoint_tail_of_prefactor_gap
{d : ℕ}
[NeZero d]
(params : QuantitativeCoarseGrainedEllipticityParams d)
:
∃ (Cfluct : ℝ) (Ccrude : ℝ) (Centry : ℝ) (a : ℝ),
0 < Cfluct ∧ 0 < Ccrude ∧ 0 < Centry ∧ 0 < a ∧ ∀ {t αbad Btail : ℝ} {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 Blead := Den * 3 ^ (L + 1);
have Acrude := 3 ^ (t * ↑q - t * (L + 1)) / Dcrude;
have Alead := (3 ^ ↑q / Blead) ^ η;
have Atail := (3 ^ ↑q / Btail) ^ η;
have ρtop := 3 ^ ctop;
have ρbottom := 3 ^ (2 * (t - αbad) / η);
have Cbottom := Real.exp 1 * max 1 ↑S.card;
have Ctop := ↑S.card * weightedLinearExpKernelConst w (ρtop ^ 2);
have ChighBottom := ↑(q + 1) * (Cbottom * w ^ q) * weightedGeometricExpKernelConst w (ρbottom ^ η);
0 < t →
0 ≤ αbad →
αbad < t →
αbad < b →
αbad * (1 + b / a) < b →
αbad < a →
t ≤ b →
0 < Btail →
1 ≤ 3 ^ ↑q / Blead →
1 ≤ Acrude →
(have Lcut := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1);
Lcut + 1 < (1 - αbad / a) * ↑q) →
max 0 Ctop + max 0 ChighBottom ≤ Real.exp (Alead - Atail) →
MeasureTheory.Measure.real P (badScaleEvent Hshift t αbad q) ≤ Real.exp (-Atail)
Uniform endpoint bad-scale tail after selected denominator, with the deterministic prefactor gap still explicit.
theorem
HCPolySupport.Book.Ch05.Section57.shiftedBadScaleProbability_le_uniformEndpoint_tail
{d : ℕ}
[NeZero d]
(params : QuantitativeCoarseGrainedEllipticityParams d)
:
∃ (Cfluct : ℝ) (Ccrude : ℝ) (Centry : ℝ) (a : ℝ),
0 < Cfluct ∧ 0 < Ccrude ∧ 0 < Centry ∧ 0 < a ∧ ∀ {t αbad Btail : ℝ} {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 Blead := Den * 3 ^ (L + 1);
have Alead := (3 ^ ↑q / Blead) ^ η;
have Atail := (3 ^ ↑q / Btail) ^ η;
have ρtop := 3 ^ ctop;
have ρbottom := 3 ^ (2 * (t - αbad) / η);
have Cbottom := Real.exp 1 * max 1 ↑S.card;
have Ctop := ↑S.card * weightedLinearExpKernelConst w (ρtop ^ 2);
have ChighBottom := ↑(q + 1) * (Cbottom * w ^ q) * weightedGeometricExpKernelConst w (ρbottom ^ η);
0 < t →
0 ≤ αbad →
αbad < t →
αbad < b →
αbad * (1 + b / a) < b →
αbad < a →
t ≤ b →
0 < Btail →
⌈Real.log Blead / Real.log 3⌉₊ ≤ q →
⌈(Real.log Dcrude + t * (L + 1) * Real.log 3) / (t * Real.log 3)⌉₊ ≤ q →
⌈(L + 1) / (1 - αbad / a) + 1⌉₊ ≤ q →
max 0 Ctop + max 0 ChighBottom ≤ Real.exp (Alead - Atail) →
MeasureTheory.Measure.real P (badScaleEvent Hshift t αbad q) ≤ Real.exp (-Atail)
Endpoint tail after discharging the lead, crude-bottom, and crude-top threshold side conditions by explicit ceilings.