High-contrast homogenization: Provider.Quenched.RowDecayAESummability #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Almost-everywhere summability from stopping-generation decay #
The stopping-generation tail is uniform in the outer generation. Along the diagonal where the allowed stopping offset grows linearly, its probabilities are super-geometrically summable. Borel--Cantelli therefore makes the row decay strong enough to sum every weighted tail almost everywhere.
theorem
HCPolySupport.HighContrast.Quenched.ae_summable_weighted_row_of_stoppingGeneration
{Omega : Type u_1}
[MeasurableSpace Omega]
{P : MeasureTheory.Measure Omega}
[MeasureTheory.IsProbabilityMeasure P]
{nstar qfb b : ℕ}
{R B : ℕ → Omega → ℝ}
{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 {ω : Omega | 3 ^ (n + q + b) < R n ω} ≤ Real.exp (-(cd * 3 ^ (2 * mu * ↑q))))
(hBdecay :
∀ᵐ (ω : Omega) ∂P, ∀ (m : ℕ), nstar ≤ m → B m ω ≤ Cblk * delta * 3 ^ (-theta * (↑m - ↑(stoppingGeneration nstar qfb R m ω) - ↑nstar)))
(hBnonneg : ∀ (m : ℕ) (ω : Omega), 0 ≤ B m ω)
:
Almost-everywhere row decay against a stopping family supplies the almost-everywhere weighted summability required by the coupled engine.