High-contrast homogenization: Provider.Quenched.RowTailSumConstruction #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
A measurable representative of the weighted row series #
The weighted tail series of e.random.adapted.sum need not
converge off the support of the law, so the endgame carries it as a measurable
function agreeing almost everywhere with the raw series. This file constructs
that representative from measurability of the rows and almost-everywhere
summability alone.
theorem
HCPolySupport.HighContrast.Quenched.exists_measurable_weighted_rowTailSum
{Ω : Type u_1}
[MeasurableSpace Ω]
{P : MeasureTheory.Measure Ω}
{B : ℕ → Ω → ℝ}
{kappa : ℝ}
(hB : ∀ (m : ℕ), Measurable (B m))
(hsummable : ∀ᵐ (ω : Ω) ∂P, ∀ (k : ℕ), Summable fun (j : ℕ) => 3 ^ (kappa * ↑j) * B (k + j) ω)
:
An almost-everywhere summable weighted row family has a measurable tail-sum representative at every generation.