High-contrast homogenization: Provider.Quenched.QuenchedBadTail

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The bad-tail estimate of the quenched endgame

Summing the one-generation estimate over all later generations produces the endpoint-safe radius of e.random.final.scale in the form consumed by the abstract normalized minimal scale: a stretched-exponential bound for the bad-tail event whose exponent is exactly the one carried by the finite-range gauge. The last theorem selects the normalized mixing scale of e.random.final.scale together with the pathwise certificate belonging to that same scale.

noncomputable def HCPolySupport.HighContrast.Quenched.badTailExponent (nstar : ℕ) (theta mu cd Cblk : ℝ) (qfb b n : ℕ) : ℝ

The per-generation exponent of the bad-tail estimate.

Equations

• HCPolySupport.HighContrast.Quenched.badTailExponent nstar theta mu cd Cblk qfb b n = cd * 3 ^ (2 * mu * (↑n - ↑nstar - HCPolySupport.HighContrast.Quenched.badTailOffset theta Cblk qfb b))

theorem HCPolySupport.HighContrast.Quenched.measureReal_badTailEvent_rowBadEvent_le {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {nstar qfb b : ℕ} {R B F : ℕ → Ω → ℝ} {theta mu cd delta Cblk : ℝ} (htheta : 0 < theta) (hmu : 0 < mu) (hcd : 0 < cd) (hdelta : 0 < delta) (hCblk : 0 < Cblk) (hRtail : ∀ (n q : ℕ), nstar ≤ n → P.real {ω : Ω | 3 ^ (n + q + b) < R n ω} ≤ Real.exp (-(cd * 3 ^ (2 * mu * ↑q)))) (hBdecay : ∀ᵐ (ω : Ω) ∂P, ∀ (m : ℕ), nstar ≤ m → B m ω ≤ Cblk * delta * 3 ^ (-theta * (↑m - ↑(stoppingGeneration nstar qfb R m ω) - ↑nstar))) (hFsum : ∀ᵐ (ω : Ω) ∂P, ∀ (k : ℕ), HasSum (fun (j : ℕ) => 3 ^ (theta / 2 * ↑j) * B (k + j) ω) (F k ω)) {N0 : ℕ} {Bconst : ℝ} (hstar : nstar ≤ N0) (hBconst : 1 ≤ Bconst) (hN0low : ↑qfb + ↑b + 1 + rowSplitOffset theta Cblk ≤ ↑N0 - ↑nstar) (hN0gain : Real.log 2 ≤ badTailExponent nstar theta mu cd Cblk qfb b N0 * (3 ^ (mu / 2) - 1)) (hN0abs : 2 * Real.log 4 ≤ badTailExponent nstar theta mu cd Cblk qfb b N0) (hBrel : 3 ^ (2 * mu * (↑nstar + badTailOffset theta Cblk qfb b - ↑N0)) ≤ cd / 2 * Bconst ^ (2 * mu)) (N : ℕ) (hN : N0 ≤ N) : P.real (Book.Ch05.Section57.badTailEvent (rowBadEvent delta F) N) ≤ Real.exp (-(3 ^ ↑(N - N0) / Bconst) ^ (2 * mu))

The bad-tail event of the weighted row series obeys the stretched-exponential bound in the shape consumed by the abstract normalized minimal scale.