Coarse-graining support: Support.Book.Ch05.Theorems.Section57.BadScaleTailRawCrude #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Raw-constant crude-bottom component #
This file exposes the crude-bottom component estimate with the raw crude fixed-pair estimate supplied externally. It is used to keep the crude branch constant synchronized with the mixed high-bottom branch in the final bad-scale assembly.
theorem
HCPolySupport.Book.Ch05.Section57.measureReal_shiftedBottomBadScaleProbability_le_weighted_kernel
{d : ℕ}
[NeZero d]
{σ Ccrude : ℝ}
(hσ_pos : 0 < σ)
(hCcrude : 0 < Ccrude)
(params : QuantitativeCoarseGrainedEllipticityParams d)
(hcrudeRaw :
∀ {t αbad : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct),
hΓ.sigma = σ →
hΓ.params = params →
∀ {N0 q m n : ℕ},
have K := quenchedProbeEnvelopeConst d;
have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (N0 + M) (N0 + N) aω;
have x := αbad * ↑(m - q) - t * ↑(m - n);
have D := descendantsAtScale (originCube d ↑(N0 + m)) ↑(N0 + n);
have S := Finset.univ;
have scale := K * (Ccrude * hΓ.thetaHat ^ 2);
have T := Real.rpow 3 (-x);
have lam := T / scale;
n < m →
q ≤ m →
1 ≤ lam →
MeasureTheory.Measure.real P (badPairEvent Hshift t αbad q m n) ≤ ↑S.card * (↑D.card * Real.exp (-lam ^ σ)))
{Centry 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 L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1);
have w := ↑(3 ^ d);
have A := 3 ^ (t * ↑q - t * (L + 1)) / (K * Ccrude * hΓ.thetaHat ^ 2);
have ρ := 3 ^ (t - αbad);
0 < a →
0 < t →
αbad < t →
1 ≤ A →
MeasureTheory.Measure.real P (crudeBottomBadScaleEvent Hshift K a t αbad q) ≤ ↑(q + 1) * (↑S.card * w ^ q) * (Real.exp (-A ^ σ) * weightedGeometricExpKernelConst w (ρ ^ σ))
Crude-bottom component estimate using a supplied raw crude fixed-pair tail.