Coarse-graining support: Support.Book.Ch05.Theorems.Section57.BadScaleTailRaw #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Raw-constant bad-scale component inputs #
This file exposes the mixed high-bottom fixed-pair estimate with the raw high and crude pair estimates supplied as hypotheses. This keeps the constants used by the top, mixed-bottom, and crude-bottom branches synchronized for the final bad-scale assembly.
theorem
HCPolySupport.Book.Ch05.Section57.shiftedHighBottomPairMeasure_le_softMax_of_pairBounds
{d : ℕ}
[NeZero d]
{σ Cfluct Ccrude Centry a : ℝ}
(hσ_pos : 0 < σ)
(params : QuantitativeCoarseGrainedEllipticityParams d)
(hCfluct : 0 < Cfluct)
(hCcrude : 0 < Ccrude)
(_hCentry : 0 < Centry)
(ha : 0 < a)
(hhighRaw :
∀ {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)))
(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 ^ σ)))
{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 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 b := ↑d / 2;
have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1);
have tau := min σ 2;
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 * hΓ.thetaHat ^ 2);
have crudeA := 3 ^ (t * ↑(q - n) + (t - αbad) * ↑(m - q)) / (K * Ccrude * hΓ.thetaHat ^ 2);
n < m →
q ≤ m →
0 < t →
αbad < t →
MeasureTheory.Measure.real P (highBottomPairEvent Hshift K a t αbad q m n) ≤ max 1 pref * Real.exp (1 - max (max 1 highA ^ tau) (max 1 crudeA ^ σ))
Exact fixed-pair mixed-bottom estimate with the high and crude raw pair estimates supplied externally, so downstream assembly can use one shared set of constants.
theorem
HCPolySupport.Book.Ch05.Section57.shiftedHighBottomPairProbability_le_interpolatedWeightedRow_of_softMaximum
{d : ℕ}
[NeZero d]
{σ Cfluct Ccrude Centry a : ℝ}
(hσ_pos : 0 < σ)
(params : QuantitativeCoarseGrainedEllipticityParams d)
(hCfluct : 0 < Cfluct)
(hCcrude : 0 < Ccrude)
(_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 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 b := ↑d / 2;
have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1);
have tau := min σ 2;
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 * hΓ.thetaHat ^ 2);
have crudeA := 3 ^ (t * ↑(q - n) + (t - αbad) * ↑(m - q)) / (K * Ccrude * hΓ.thetaHat ^ 2);
n < m →
q ≤ m →
0 < t →
αbad < t →
MeasureTheory.Measure.real P (highBottomPairEvent Hshift K a t αbad q m n) ≤ max 1 pref * Real.exp (1 - max (max 1 highA ^ tau) (max 1 crudeA ^ σ)))
{t αbad Den : ℝ}
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct)
:
hΓ.sigma = σ →
hΓ.params = params →
∀ {q r : ℕ} {j : Fin (q + 1)},
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 τ := finiteQuenchedTailTau σ;
have η := finiteQuenchedTailExponent d σ t;
have w := ↑(3 ^ d);
have Dhigh := 2 * K * Cfluct * hΓ.thetaHat ^ 2;
have Dcrude := K * Ccrude * hΓ.thetaHat ^ 2;
have A := 3 ^ (↑q - τ * b * (L + 1) / η) / Den;
have ρ := 3 ^ (τ * (t - αbad) / η);
have Cpref := Real.exp 1 * max 1 ↑S.card;
have m := q + r;
have n := q - ↑j;
0 < t →
t ≤ b →
αbad < t →
0 < Den →
Dhigh ^ τ ≤ Den ^ η →
Dcrude ^ σ ≤ Den ^ η →
MeasureTheory.Measure.real P (highBottomPairEvent Hshift K a t αbad q m n) ≤ Cpref * w ^ q * (w ^ r * Real.exp (-(A * ρ ^ r) ^ η))
Convert the synchronized mixed-bottom soft fixed-pair estimate into the weighted row estimate with the corrected finite exponent.
theorem
HCPolySupport.Book.Ch05.Section57.shiftedHighBottomBadScaleProbability_le_interpolated_weighted_kernel_of_rowBound
{d : ℕ}
[NeZero d]
{σ Cfluct Ccrude Centry a : ℝ}
(hσ_pos : 0 < σ)
(params : QuantitativeCoarseGrainedEllipticityParams d)
(hrow :
∀ {t αbad Den : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct),
hΓ.sigma = σ →
hΓ.params = params →
∀ {q r : ℕ} {j : Fin (q + 1)},
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 τ := finiteQuenchedTailTau σ;
have η := finiteQuenchedTailExponent d σ t;
have w := ↑(3 ^ d);
have Dhigh := 2 * K * Cfluct * hΓ.thetaHat ^ 2;
have Dcrude := K * Ccrude * hΓ.thetaHat ^ 2;
have A := 3 ^ (↑q - τ * b * (L + 1) / η) / Den;
have ρ := 3 ^ (τ * (t - αbad) / η);
have Cpref := Real.exp 1 * max 1 ↑S.card;
have m := q + r;
have n := q - ↑j;
0 < t →
t ≤ b →
αbad < t →
0 < Den →
Dhigh ^ τ ≤ Den ^ η →
Dcrude ^ σ ≤ Den ^ η →
MeasureTheory.Measure.real P (highBottomPairEvent Hshift K a t αbad q m n) ≤ Cpref * w ^ q * (w ^ r * Real.exp (-(A * ρ ^ r) ^ η)))
{t αbad Den : ℝ}
{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 τ := finiteQuenchedTailTau σ;
have η := finiteQuenchedTailExponent d σ t;
have w := ↑(3 ^ d);
have Dhigh := 2 * K * Cfluct * hΓ.thetaHat ^ 2;
have Dcrude := K * Ccrude * hΓ.thetaHat ^ 2;
have A := 3 ^ (↑q - τ * b * (L + 1) / η) / Den;
have ρ := 3 ^ (τ * (t - αbad) / η);
have Cpref := Real.exp 1 * max 1 ↑S.card;
0 < t →
t ≤ b →
αbad < t →
0 < Den →
Dhigh ^ τ ≤ Den ^ η →
Dcrude ^ σ ≤ Den ^ η →
1 ≤ A →
MeasureTheory.Measure.real P (highBottomBadScaleEvent Hshift K a t αbad q) ≤ ↑(q + 1) * (Cpref * w ^ q) * (Real.exp (-A ^ η) * weightedGeometricExpKernelConst w (ρ ^ η))
Sum synchronized mixed-bottom row estimates into the high-bottom component bound, still without choosing new constants.