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

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

Bottom component bad-scale bounds

This file builds the concrete bottom row estimates used by the weighted component summation lemmas.

theorem HCPolySupport.Book.Ch05.Section57.highBottom_lam_lower {d : ℕ} [NeZero d] {K Cfluct θ a t α : ℝ} {q r : ℕ} {j : Fin (q + 1)} (hK : 0 < K) (hCfluct : 0 < Cfluct) (hθ : 0 < θ) (ha : 0 < a) (ht : 0 < t) (hαt : α < t) (hαb : α < ↑d / 2) (hαharm : α * (1 + ↑d / 2 / a) < ↑d / 2) : have m := q + r; have n := q - ↑j; have x := α * ↑(m - q) - t * ↑(m - n); have ℓ := ⌈(a * Real.log 3)⁻¹ * (Real.log (max (2 * K) 1) + x * Real.log 3)⌉₊; have b := ↑d / 2; have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1); have c := min t (min b (min (t - α) (min (b - α) (min ((t - α) * (1 + b / a)) (b - α * (1 + b / a)))))); have scale := Cfluct * 3 ^ (-↑d / 2 * ↑(n - ℓ)) * θ ^ 2; have T := 3 ^ (-x); have lam := T / (2 * K * scale); have A := 3 ^ (c * ↑q - b * (L + 1)) / (2 * K * Cfluct * θ ^ 2); have ρ := 3 ^ c; ℓ < n → n < m → A * ρ ^ r ≤ lam

Deterministic lower bound on the high-bottom tail parameter.

theorem HCPolySupport.Book.Ch05.Section57.crudeBottom_lam_lower {K C θ a t α : ℝ} {q r : ℕ} {j : Fin (q + 1)} (hK : 0 < K) (hC : 0 < C) (hθ : 0 < θ) (ha : 0 < a) (ht : 0 < t) (hαt : α < t) : have m := q + r; have n := q - ↑j; have x := α * ↑(m - q) - t * ↑(m - n); have ℓ := ⌈(a * Real.log 3)⁻¹ * (Real.log (max (2 * K) 1) + x * Real.log 3)⌉₊; have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1); have scale := K * (C * θ ^ 2); have T := 3 ^ (-x); have lam := T / scale; have A := 3 ^ (t * ↑q - t * (L + 1)) / (K * C * θ ^ 2); have ρ := 3 ^ (t - α); n ≤ ℓ → n < m → A * ρ ^ r ≤ lam

Deterministic lower bound on the crude-bottom tail parameter. The condition n ≤ ℓ is the complementary high-scale condition; together with n ≤ q it bounds n by the logarithmic offset, so the discount supplies the full t q gain.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_shiftedHighBottomPairEvent_quenchedProbeEnvelope_le_weighted_row_of_badPair_bound {d : ℕ} [NeZero d] {σ Cfluct Centry a : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) (hCfluct : 0 < Cfluct) (_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 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))) {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 b := ↑d / 2; have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1); have c := min t (min b (min (t - αbad) (min (b - αbad) (min ((t - αbad) * (1 + b / a)) (b - αbad * (1 + b / a)))))); have τ := min σ 2; have w := ↑(3 ^ d); have A := 3 ^ (c * ↑q - b * (L + 1)) / (2 * K * Cfluct * hΓ.thetaHat ^ 2); have ρ := 3 ^ c; have m := q + r; have n := q - ↑j; 0 < t → αbad < t → αbad < b → αbad * (1 + b / a) < b → 1 ≤ A → MeasureTheory.Measure.real P (highBottomPairEvent Hshift K a t αbad q m n) ≤ ↑S.card * w ^ q * (w ^ r * Real.exp (-(A * ρ ^ r) ^ τ))

Concrete high-bottom row estimate from a fixed high-pair tail bound.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_shiftedHighBottomPairEvent_quenchedProbeEnvelope_le_weighted_row {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Cfluct : ℝ) (Centry : ℝ) (a : ℝ), 0 < Cfluct ∧ 0 < Centry ∧ 0 < 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 b := ↑d / 2; have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1); have c := min t (min b (min (t - αbad) (min (b - αbad) (min ((t - αbad) * (1 + b / a)) (b - αbad * (1 + b / a)))))); have τ := min σ 2; have w := ↑(3 ^ d); have A := 3 ^ (c * ↑q - b * (L + 1)) / (2 * K * Cfluct * hΓ.thetaHat ^ 2); have ρ := 3 ^ c; have m := q + r; have n := q - ↑j; 0 < t → αbad < t → αbad < b → αbad * (1 + b / a) < b → 1 ≤ A → MeasureTheory.Measure.real P (highBottomPairEvent Hshift K a t αbad q m n) ≤ ↑S.card * w ^ q * (w ^ r * Real.exp (-(A * ρ ^ r) ^ τ))

Concrete high-bottom row estimate.

theorem HCPolySupport.Book.Ch05.Section57.shiftedHighBottomBadScaleMeasure_le_weightedKernel_of_rowBound {d : ℕ} [NeZero d] {σ Cfluct Centry a : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) (_hCfluct : 0 < Cfluct) (_hCentry : 0 < Centry) (_ha : 0 < a) (hrow : ∀ {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 b := ↑d / 2; have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1); have c := min t (min b (min (t - αbad) (min (b - αbad) (min ((t - αbad) * (1 + b / a)) (b - αbad * (1 + b / a)))))); have τ := min σ 2; have w := ↑(3 ^ d); have A := 3 ^ (c * ↑q - b * (L + 1)) / (2 * K * Cfluct * hΓ.thetaHat ^ 2); have ρ := 3 ^ c; have m := q + r; have n := q - ↑j; 0 < t → αbad < t → αbad < b → αbad * (1 + b / a) < b → 1 ≤ A → MeasureTheory.Measure.real P (highBottomPairEvent Hshift K a t αbad q m n) ≤ ↑S.card * w ^ q * (w ^ r * Real.exp (-(A * ρ ^ r) ^ τ))) {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 b := ↑d / 2; have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1); have c := min t (min b (min (t - αbad) (min (b - αbad) (min ((t - αbad) * (1 + b / a)) (b - αbad * (1 + b / a)))))); have τ := min σ 2; have w := ↑(3 ^ d); have A := 3 ^ (c * ↑q - b * (L + 1)) / (2 * K * Cfluct * hΓ.thetaHat ^ 2); have ρ := 3 ^ c; 0 < t → αbad < t → αbad < b → αbad * (1 + b / a) < b → 1 ≤ A → MeasureTheory.Measure.real P (highBottomBadScaleEvent Hshift K a t αbad q) ≤ ↑(q + 1) * (↑S.card * w ^ q) * (Real.exp (-A ^ τ) * weightedGeometricExpKernelConst w (ρ ^ τ))

Concrete high-bottom component estimate obtained by summing a fixed weighted row estimate.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_shiftedHighBottomBadScaleEvent_quenchedProbeEnvelope_le_weighted_kernel {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Cfluct : ℝ) (Centry : ℝ) (a : ℝ), 0 < Cfluct ∧ 0 < Centry ∧ 0 < 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 b := ↑d / 2; have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1); have c := min t (min b (min (t - αbad) (min (b - αbad) (min ((t - αbad) * (1 + b / a)) (b - αbad * (1 + b / a)))))); have τ := min σ 2; have w := ↑(3 ^ d); have A := 3 ^ (c * ↑q - b * (L + 1)) / (2 * K * Cfluct * hΓ.thetaHat ^ 2); have ρ := 3 ^ c; 0 < t → αbad < t → αbad < b → αbad * (1 + b / a) < b → 1 ≤ A → MeasureTheory.Measure.real P (highBottomBadScaleEvent Hshift K a t αbad q) ≤ ↑(q + 1) * (↑S.card * w ^ q) * (Real.exp (-A ^ τ) * weightedGeometricExpKernelConst w (ρ ^ τ))

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