Theorems · Theorem · measure theory

MeasureTheory.uniformIntegrable_average

∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal} {E : Type u_4}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E],
  1 ≤ p →
    ∀ {f : ℕ → α → E},
      MeasureTheory.UniformIntegrable f p μ →
        MeasureTheory.UniformIntegrable (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, f i) p μ

The averaging of a uniformly integrable sequence is also uniformly integrable.

Defined in

Mathlib.MeasureTheory.Function.UniformIntegrable

Cited by

2 results in Mathlib

Foundations

Depth 218 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace