Coarse-graining support: Support.Book.Ch05.Theorems.Section57.UniformCrudeBottom

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

The crude bottom-scale branch at the uniform endpoint

Under Γ_∞, the crude branch is deterministic: the localized normalized probe maximum is almost surely bounded by a constant multiple of thetaHat^2. Consequently the corresponding bad-pair event is empty modulo null sets once the crude threshold is at least this deterministic scale.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_shiftedCrude_badPairEvent_quenchedProbeEnvelope_eq_zero_of_gammaInfinity {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (C : ℝ), 0 < C ∧ ∀ {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 * (C * 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

Endpoint crude fixed bad-pair estimate. The right side is exactly zero: the endpoint replaces the finite-σ crude tail by deterministic boundedness.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_shiftedCrudeBottomPairEvent_quenchedProbeEnvelope_le_weighted_row_gammaInfinity {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Ccrude : ℝ), 0 < Ccrude ∧ ∀ {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 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 * hInf.thetaHat ^ 2); have ρ := 3 ^ (t - αbad); 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) ≤ ↑S.card * w ^ q * (w ^ r * Real.exp (-(A * ρ ^ r) ^ ↑d))

Endpoint concrete crude-bottom row estimate.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_shiftedCrudeBottomPairEvent_quenchedProbeEnvelope_eq_zero_gammaInfinity {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Ccrude : ℝ), 0 < Ccrude ∧ ∀ {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 concrete crude-bottom row cutoff. Once the crude row parameter is at least one, every fixed crude-bottom pair has zero probability.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_shiftedCrudeBottomBadScaleEvent_quenchedProbeEnvelope_eq_zero_gammaInfinity {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Ccrude : ℝ), 0 < Ccrude ∧ ∀ {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.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_shiftedCrudeBottomBadScaleEvent_quenchedProbeEnvelope_le_weighted_kernel_gammaInfinity {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Ccrude : ℝ), 0 < Ccrude ∧ ∀ {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 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 * hInf.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 ^ ↑d) * weightedGeometricExpKernelConst w (ρ ^ ↑d))

Endpoint crude-bottom component estimate after summing the weighted rows.