High-contrast homogenization: Provider.Quenched.QuenchedGenerationTail

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

One generation of the quenched bad-event estimate

The stopping radii of the endgame carry a Gaussian gauge at every shifted offset: the shifted tail of the quenched radius, read with the Gaussian concentration gauge supplied by unit range of dependence. This file passes that estimate to real thresholds, exactly as the stopping construction of ss.random.dirichlet does after the tail of its stopping index, and sums the resulting super-geometric family over the generations of the weighted row series. The outcome is a single stretched-exponential estimate for one bad event.

noncomputable def HCPolySupport.HighContrast.Quenched.badTailOffset (theta Cblk : ℝ) (qfb b : ℕ) : ℝ

The deterministic offset of the bad-event estimate: the split offset of the weighted row series together with the shift of the stopping-radius gauge.

Equations

• HCPolySupport.HighContrast.Quenched.badTailOffset theta Cblk qfb b = HCPolySupport.HighContrast.Quenched.rowSplitOffset theta Cblk + 1 + ↑qfb + ↑b

theorem HCPolySupport.HighContrast.Quenched.measureReal_stoppingGeneration_gt_real_le {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {nstar qfb b : ℕ} {R : ℕ → Ω → ℝ} {mu cd : ℝ} (hmu : 0 < mu) (hcd : 0 < cd) (hRtail : ∀ (n q : ℕ), nstar ≤ n → P.real {ω : Ω | 3 ^ (n + q + b) < R n ω} ≤ Real.exp (-(cd * 3 ^ (2 * mu * ↑q)))) (m : ℕ) {y : ℝ} (hy : ↑qfb + ↑b + 1 ≤ y) : P.real {ω : Ω | y < ↑(stoppingGeneration nstar qfb R m ω)} ≤ Real.exp (-(cd * 3 ^ (2 * mu * (y - 1 - ↑qfb - ↑b))))

The stopping estimate holds at every real threshold, not only at the triadic ones.

theorem HCPolySupport.HighContrast.Quenched.measureReal_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 ω)) {n : ℕ} (hn : nstar ≤ n) (hlow : ↑qfb + ↑b + 1 + rowSplitOffset theta Cblk ≤ ↑n - ↑nstar) (hgain : Real.log 2 ≤ cd * 3 ^ (2 * mu * (↑n - ↑nstar - badTailOffset theta Cblk qfb b)) * (3 ^ (mu / 2) - 1)) : P.real (rowBadEvent delta F n) ≤ 2 * Real.exp (-(cd * 3 ^ (2 * mu * (↑n - ↑nstar - badTailOffset theta Cblk qfb b))))

The bad event of one generation of the weighted row series carries a stretched-exponential estimate.