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

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

Tail collapse for the small-bottom band

This file converts the weighted kernel bound for the finite band n < Nentry into the same stretched-exponential bad-scale tail used by the shifted large-scale branch.

theorem HCPolySupport.Book.Ch05.Section57.smallBottomBadScaleEvent_antitone {Ω : Type u_1} {H : ℕ → ℕ → Ω → ℝ} {Nentry : ℕ} {t α : ℝ} (hα : 0 ≤ α) {N K : ℕ} (hNK : N ≤ K) : smallBottomBadScaleEvent H Nentry t α K ⊆ smallBottomBadScaleEvent H Nentry t α N

The small-bottom bad-scale events are antitone in the bad scale.

theorem HCPolySupport.Book.Ch05.Section57.badTailEvent_smallBottomBadScaleEvent_subset {Ω : Type u_1} {H : ℕ → ℕ → Ω → ℝ} {Nentry : ℕ} {t α : ℝ} (hα : 0 ≤ α) {N : ℕ} : badTailEvent (smallBottomBadScaleEvent H Nentry t α) N ⊆ smallBottomBadScaleEvent H Nentry t α N

Tail form of small-bottom monotonicity.

noncomputable def HCPolySupport.Book.Ch05.Section57.smallBottomTailDenominator (scale η σ : ℝ) : ℝ

Denominator which rewrites the crude small-bottom sigma * t tail in the common interpolated exponent.

Equations

• HCPolySupport.Book.Ch05.Section57.smallBottomTailDenominator scale η σ = max 1 scale ^ (σ / η)

theorem HCPolySupport.Book.Ch05.Section57.smallBottomTailDenominator_pos {scale η σ : ℝ} : 0 < smallBottomTailDenominator scale η σ

theorem HCPolySupport.Book.Ch05.Section57.one_le_smallBottomTailDenominator {scale η σ : ℝ} (hη : 0 < η) (hσ : 0 ≤ σ) : 1 ≤ smallBottomTailDenominator scale η σ

theorem HCPolySupport.Book.Ch05.Section57.scale_rpow_le_smallBottomTailDenominator_pow_eta {scale η σ : ℝ} (hscale : 0 < scale) (hη : 0 < η) (hσ : 0 < σ) : scale ^ σ ≤ smallBottomTailDenominator scale η σ ^ η

theorem HCPolySupport.Book.Ch05.Section57.smallBottomTailDenominator_rpow_le_crude_scale {scale η σ t : ℝ} {q : ℕ} (hscale : 0 < scale) (hη : 0 < η) (hσ : 0 < σ) (hη_le : η ≤ σ * t) : (3 ^ ↑q / smallBottomTailDenominator scale η σ) ^ η ≤ (3 ^ (t * ↑q) / scale) ^ σ

The small-bottom denominator converts the crude sigma * t scale into the common interpolated exponent.

theorem HCPolySupport.Book.Ch05.Section57.exists_quantitative_threshold_smallBottomBadTail_quenchedProbeEnvelope_le_interpolated_tail {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Ccrude : ℝ), 0 < Ccrude ∧ ∀ {t α : ℝ}, have K := quenchedProbeEnvelopeConst d; have S := Finset.univ; have η := finiteQuenchedTailExponent d σ t; have w := ↑(3 ^ d); have W := max 1 w; have ρgap := 3 ^ η; have C₀ := 2 + Real.log W; 0 < t → 0 ≤ α → α < t → ∃ (R : ℕ), (∀ (q : ℕ), R ≤ q → C₀ * ↑q ≤ Real.exp (Real.log ρgap / 2 * ↑q)) ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → ∀ {Nentry : ℕ}, have H := quenchedProbeEnvelope hP hStruct; have scale := K * (Ccrude * hΓ.thetaHat ^ 2); have ρsmall := 3 ^ (t - α); have Ksmall := weightedGeometricExpKernelConst w (ρsmall ^ σ); have pref := ↑Nentry * ↑S.card * w ^ Nentry; have M := max 1 (max 0 (pref * Ksmall)); have Blead := smallBottomTailDenominator scale η σ; have Btail := 2 * Blead; have cgap := Blead ^ (-η) - Btail ^ (-η); have Qpref := max ⌈max 0 (Real.log M)⌉₊ (max R ⌈2 * max 0 (-Real.log cgap) / Real.log ρgap⌉₊); have Qlead := ⌈Real.log Blead / Real.log 3⌉₊; have Q := max Qpref Qlead; ∀ (q : ℕ), Q ≤ q → MeasureTheory.Measure.real P (badTailEvent (smallBottomBadScaleEvent H Nentry t α) (Nentry + q)) ≤ Real.exp (-(3 ^ ↑q / Btail) ^ η)

Quantitative small-bottom bad-tail bound with the fixed prefactor-growth threshold chosen before the law.