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

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

The crude-bottom bad-scale component

This file proves the concrete crude-bottom row estimate and feeds it into the weighted constant-row summation lemma. The finite maxima remain as explicit cardinality prefactors.

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

Concrete crude-bottom row estimate.

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

Concrete crude-bottom component estimate obtained by summing the weighted row estimate.