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

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

The small-bottom band below the annealed entry scale

This file starts the quantitative treatment of the finite band n < N0 in the final quenched theorem. The first lemma is the concrete crude fixed-pair row estimate in absolute variables.

theorem HCPolySupport.Book.Ch05.Section57.smallBottomBadScaleEvent_subset_rows {Ω : Type u_1} {H : ℕ → ℕ → Ω → ℝ} {Nentry q : ℕ} {t α : ℝ} : smallBottomBadScaleEvent H Nentry t α (Nentry + q) ⊆ ⋃ (r : ℕ), ⋃ (j : Fin Nentry), badPairEvent H t α (Nentry + q) (Nentry + q + r) ↑j

Reindex the small-bottom event into rows above the bad scale and the finite set of bottom levels below Nentry.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_smallBottomPairEvent_quenchedProbeEnvelope_le_weighted_row {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Ccrude : ℝ), 0 < Ccrude ∧ ∀ {t α : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → ∀ {Nentry q r n : ℕ}, have K := quenchedProbeEnvelopeConst d; have H := quenchedProbeEnvelope hP hStruct; have S := Finset.univ; have w := ↑(3 ^ d); have scale := K * (Ccrude * hΓ.thetaHat ^ 2); have A := 3 ^ (t * ↑q) / scale; have ρ := 3 ^ (t - α); have N := Nentry + q; have m := N + r; 0 < t → α < t → n < Nentry → 1 ≤ A → MeasureTheory.Measure.real P (badPairEvent H t α N m n) ≤ ↑S.card * w ^ Nentry * w ^ q * (w ^ r * Real.exp (-(A * ρ ^ r) ^ σ))

Concrete crude fixed-pair row estimate for pairs whose bottom scale is below the entry scale. Here q is the distance from the entry scale to the bad scale and r is the distance above the bad scale.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_smallBottomBadScaleEvent_quenchedProbeEnvelope_le_weighted_kernel {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Ccrude : ℝ), 0 < Ccrude ∧ ∀ {t α : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → ∀ {Nentry q : ℕ}, have K := quenchedProbeEnvelopeConst d; have H := quenchedProbeEnvelope hP hStruct; have S := Finset.univ; have w := ↑(3 ^ d); have scale := K * (Ccrude * hΓ.thetaHat ^ 2); have A := 3 ^ (t * ↑q) / scale; have ρ := 3 ^ (t - α); have N := Nentry + q; 0 < t → α < t → 1 ≤ A → MeasureTheory.Measure.real P (smallBottomBadScaleEvent H Nentry t α N) ≤ ↑Nentry * (↑S.card * w ^ Nentry * w ^ q) * (Real.exp (-A ^ σ) * weightedGeometricExpKernelConst w (ρ ^ σ))

Sum the small-bottom fixed-pair row estimate over the rows and the finite bottom band.