Coarse-graining support: Support.Book.Ch05.Theorems.Section57.BadScaleComponentBoundsHigh #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
High component bad-scale bounds #
This file rebuilds the high component estimates along the no-loss route. The finite descendant multiplicity is kept as a probability-level prefactor and is absorbed by the weighted exponential kernel in the final summation.
theorem
HCPolySupport.Book.Ch05.Section57.shiftedHighTopBadScaleMeasure_le_weightedKernel_of_pairBound
{d : ℕ}
[NeZero d]
{σ Cfluct Centry a : ℝ}
(hσ_pos : 0 < σ)
(params : QuantitativeCoarseGrainedEllipticityParams d)
(hCfluct : 0 < Cfluct)
(_hCentry : 0 < Centry)
(ha : 0 < a)
(hpair :
∀ {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 := ⌈(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;
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 : ℝ}
{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 c := min (t - αbad) (min (b - αbad) (min ((t - αbad) * (1 + b / a)) (b - αbad * (1 + b / a))));
have τ := min σ 2;
have A := 3 ^ (b * ↑q - b * (L + 1)) / (2 * K * Cfluct * hΓ.thetaHat ^ 2);
have ρ := 3 ^ c;
have w := ↑(3 ^ d);
0 < t →
αbad < t →
αbad < b →
αbad * (1 + b / a) < b →
1 ≤ A →
MeasureTheory.Measure.real P (highTopBadScaleEvent Hshift K a t αbad q) ≤ ↑S.card * (Real.exp (-A ^ τ) * weightedLinearExpKernelConst w (ρ ^ τ))
Sharp high-top bad-scale component estimate from a fixed high-pair tail bound. This helper exposes the constants so that the top and bottom high branches can be assembled with the same intermediate-scale exponent.
theorem
HCPolySupport.Book.Ch05.Section57.measureReal_shiftedHighTopBadScaleEvent_quenchedProbeEnvelope_le_weighted_kernel
{d : ℕ}
[NeZero d]
{σ : ℝ}
(hσ_pos : 0 < σ)
(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) (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 c := min (t - αbad) (min (b - αbad) (min ((t - αbad) * (1 + b / a)) (b - αbad * (1 + b / a))));
have τ := min σ 2;
have A := 3 ^ (b * ↑q - b * (L + 1)) / (2 * K * Cfluct * hΓ.thetaHat ^ 2);
have ρ := 3 ^ c;
have w := ↑(3 ^ d);
0 < t →
αbad < t →
αbad < b →
αbad * (1 + b / a) < b →
1 ≤ A →
MeasureTheory.Measure.real P (highTopBadScaleEvent Hshift K a t αbad q) ≤ ↑S.card * (Real.exp (-A ^ τ) * weightedLinearExpKernelConst w (ρ ^ τ))
Sharp high-top bad-scale component estimate with the finite descendant cardinality absorbed by the weighted linear kernel.