Coarse-graining support: Support.Book.Ch05.Theorems.Section57.UniformEndpointSynchronized #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Synchronized uniform-endpoint bad-scale inputs #
The endpoint bad-scale assembly must choose the high-branch constants, the deterministic crude cutoff constant, and the annealed entry scale only once. The lemmas in this file expose the endpoint high-bottom branch with those constants supplied externally.
theorem
HCPolySupport.Book.Ch05.Section57.measureReal_shiftedHighBottomPairProbability_le_soft_high_gammaInfinity
{d : ℕ}
[NeZero d]
{Cfluct Centry a : ℝ}
(params : QuantitativeCoarseGrainedEllipticityParams d)
(hCfluct : 0 < Cfluct)
(_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 = 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 : ℝ}
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct)
:
hInf.params = params →
∀ {q m n : ℕ},
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 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 pref := ↑S.card * ↑D.card;
have highA :=
3 ^ (b * ↑q - (b - t) * ↑(q - n) + (t - αbad) * ↑(m - q) - b * (L + 1)) / (2 * K * Cfluct * hInf.thetaHat ^ 2);
n < m →
q ≤ m →
0 < t →
αbad < t →
MeasureTheory.Measure.real P (highBottomPairEvent Hshift K a t αbad q m n) ≤ softPairTail pref highA 2
Localized high-bottom fixed-pair estimate at the uniform endpoint, with the raw localized bad-pair estimate supplied externally.
theorem
HCPolySupport.Book.Ch05.Section57.measureReal_shiftedHighBottomPairProbability_eq_zero_of_badPair_zero
{d : ℕ}
[NeZero d]
{Ccrude : ℝ}
(params : QuantitativeCoarseGrainedEllipticityParams d)
(hCcrude : 0 < Ccrude)
(hzeroRaw :
∀ {t αbad : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P) (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct),
hInf.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 scale := K * (Ccrude * hInf.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) = 0)
{Centry a t αbad : ℝ}
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct)
:
hInf.params = params →
∀ {q m n : ℕ},
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 crudeA := 3 ^ (t * ↑(q - n) + (t - αbad) * ↑(m - q)) / (K * Ccrude * hInf.thetaHat ^ 2);
n < m →
q ≤ m →
n ≤ q → αbad < t → 1 ≤ crudeA → MeasureTheory.Measure.real P (highBottomPairEvent Hshift K a t αbad q m n) = 0
Deterministic high-bottom fixed-pair cutoff at the uniform endpoint, with the raw endpoint crude bad-pair cutoff supplied externally.
theorem
HCPolySupport.Book.Ch05.Section57.shiftedHighBottomPairMeasure_le_rowGammaInfinity_of_bounds
{d : ℕ}
[NeZero d]
{Cfluct Ccrude Centry a : ℝ}
(params : QuantitativeCoarseGrainedEllipticityParams d)
(hCfluct : 0 < Cfluct)
(hCcrude : 0 < Ccrude)
(_hCentry : 0 < Centry)
(_ha : 0 < a)
(hhigh :
∀ {t αbad : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P) (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct),
hInf.params = params →
∀ {q m n : ℕ},
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 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 pref := ↑S.card * ↑D.card;
have highA :=
3 ^ (b * ↑q - (b - t) * ↑(q - n) + (t - αbad) * ↑(m - q) - b * (L + 1)) / (2 * K * Cfluct * hInf.thetaHat ^ 2);
n < m →
q ≤ m →
0 < t →
αbad < t →
MeasureTheory.Measure.real P (highBottomPairEvent Hshift K a t αbad q m n) ≤ softPairTail pref highA 2)
(hzero :
∀ {Centry' a' t αbad : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P) (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct),
hInf.params = params →
∀ {q m n : ℕ},
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 crudeA := 3 ^ (t * ↑(q - n) + (t - αbad) * ↑(m - q)) / (K * Ccrude * hInf.thetaHat ^ 2);
n < m →
q ≤ m →
n ≤ q →
αbad < t → 1 ≤ crudeA → MeasureTheory.Measure.real P (highBottomPairEvent Hshift K a' t αbad q m n) = 0)
{t αbad Den : ℝ}
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct)
:
hInf.params = params →
∀ {q r : ℕ} {j : Fin (q + 1)},
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 η := ↑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 ρ := 3 ^ (2 * (t - αbad) / η);
have Cpref := Real.exp 1 * max 1 ↑S.card;
have m := q + r;
have n := q - ↑j;
0 < t →
αbad < t →
t ≤ b →
0 < Den →
Dhigh ^ 2 * max 1 Dcrude ^ ((↑d - 2 * t) / t) ≤ Den ^ η →
MeasureTheory.Measure.real P (highBottomPairEvent Hshift K a t αbad q m n) ≤ Cpref * w ^ q * (w ^ r * Real.exp (-(A * ρ ^ r) ^ η))
Endpoint high-bottom fixed row estimate with all constants supplied externally.
theorem
HCPolySupport.Book.Ch05.Section57.shiftedHighBottomBadScaleProbability_le_weighted_kernel_gammaInfinity
{d : ℕ}
[NeZero d]
{Cfluct Ccrude Centry a : ℝ}
(params : QuantitativeCoarseGrainedEllipticityParams d)
(hrow :
∀ {t αbad Den : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P) (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct),
hInf.params = params →
∀ {q r : ℕ} {j : Fin (q + 1)},
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 η := ↑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 ρ := 3 ^ (2 * (t - αbad) / η);
have Cpref := Real.exp 1 * max 1 ↑S.card;
have m := q + r;
have n := q - ↑j;
0 < t →
αbad < t →
t ≤ b →
0 < Den →
Dhigh ^ 2 * max 1 Dcrude ^ ((↑d - 2 * t) / t) ≤ 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)
(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 η := ↑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 ρ := 3 ^ (2 * (t - αbad) / η);
have Cpref := Real.exp 1 * max 1 ↑S.card;
0 < t →
αbad < t →
t ≤ b →
0 < Den →
Dhigh ^ 2 * max 1 Dcrude ^ ((↑d - 2 * t) / t) ≤ Den ^ η →
1 ≤ A →
MeasureTheory.Measure.real P (highBottomBadScaleEvent Hshift K a t αbad q) ≤ ↑(q + 1) * (Cpref * w ^ q) * (Real.exp (-A ^ η) * weightedGeometricExpKernelConst w (ρ ^ η))
Endpoint high-bottom component estimate from synchronized row bounds.
theorem
HCPolySupport.Book.Ch05.Section57.shiftedCrudeBottomPairMeasure_eq_zero_of_pairZero
{d : ℕ}
[NeZero d]
{Ccrude : ℝ}
(params : QuantitativeCoarseGrainedEllipticityParams d)
(hCcrude : 0 < Ccrude)
(hzeroRaw :
∀ {t αbad : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P) (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct),
hInf.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 scale := K * (Ccrude * hInf.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) = 0)
{Centry a t αbad : ℝ}
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct)
:
hInf.params = params →
∀ {q r : ℕ} {j : Fin (q + 1)},
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 L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1);
have A := 3 ^ (t * ↑q - t * (L + 1)) / (K * Ccrude * hInf.thetaHat ^ 2);
have m := q + r;
have n := q - ↑j;
0 < a → 0 < t → αbad < t → 1 ≤ A → MeasureTheory.Measure.real P (crudeBottomPairEvent Hshift K a t αbad q m n) = 0
Endpoint crude-bottom fixed-pair cutoff with the raw endpoint crude bad-pair cutoff supplied externally.
theorem
HCPolySupport.Book.Ch05.Section57.shiftedCrudeBottomBadScaleMeasure_eq_zero_of_pairZero
{d : ℕ}
[NeZero d]
{Ccrude : ℝ}
(params : QuantitativeCoarseGrainedEllipticityParams d)
(hpair :
∀ {Centry a t αbad : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P) (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct),
hInf.params = params →
∀ {q r : ℕ} {j : Fin (q + 1)},
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 L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1);
have A := 3 ^ (t * ↑q - t * (L + 1)) / (K * Ccrude * hInf.thetaHat ^ 2);
have m := q + r;
have n := q - ↑j;
0 < a →
0 < t → αbad < t → 1 ≤ A → MeasureTheory.Measure.real P (crudeBottomPairEvent Hshift K a t αbad q m n) = 0)
{Centry 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 L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1);
have A := 3 ^ (t * ↑q - t * (L + 1)) / (K * Ccrude * hInf.thetaHat ^ 2);
0 < a → 0 < t → αbad < t → 1 ≤ A → MeasureTheory.Measure.real P (crudeBottomBadScaleEvent Hshift K a t αbad q) = 0
Endpoint crude-bottom component cutoff from synchronized fixed-pair cutoffs.