High-contrast homogenization: Provider.Quenched.CountableWeakOrliczAE #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Almost-everywhere countable weak-Orlicz summation #
This file gives the a.e.-safe counterpart of the pointwise countable summation
theorem. A pointwise limit outside one null set inherits a uniform weak-Orlicz
bound. For an a.e. summable series, AEMeasurable.mk then supplies a measurable
representative of the raw tsum without imposing summability on null outcomes.
theorem
HCPolySupport.IndependentSums.aemeasurable_tsum_of_ae_summable
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{X : ℕ → Ω → ℝ}
(hXm : ∀ (i : ℕ), Measurable (X i))
(hXSummable : ∀ᵐ (ω : Ω) ∂μ, Summable fun (i : ℕ) => X i ω)
:
AEMeasurable (fun (ω : Ω) => ∑' (i : ℕ), X i ω) μ
The tsum of measurable real summands is a.e.-measurable when the series is
summable almost everywhere.