RandomSeries.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Almost sure finiteness of a random Fourier energy

The Tonelli step used to turn summable expected squared Sobolev coefficients into almost sure finite Sobolev energy. This lemma does not identify the NLS flow or assert its existence.

theorem OAI.DefocusingNLS.ae_tsum_lt_top_of_summable_expectations line 22

Source documentation

Summable bounds on the expectations of nonnegative terms imply almost sure finiteness of their sum. Independence is not needed for this step.

theorem ae_tsum_lt_top_of_summable_expectations
    {ι Ω : Type*} [Countable ι] [MeasurableSpace Ω] {μ : Measure Ω}
    (F : ι → Ω → ℝ≥0∞) (hF : ∀ i, Measurable (F i))
    (w : ι → ℝ) (hw : Summable w)
    (hbound : ∀ i, ∫⁻ ω, F i ω ∂μ ≤ ENNReal.ofReal (w i)) :
    ∀ᵐ ω ∂μ, (∑' i, F i ω) < ∞ := by
…