Theorems · Theorem · measure theory

MeasureTheory.UniformIntegrable.spec

∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {p : ENNReal} {f : ι → α → β},
  p ≠ 0 →
    p ≠ ⊤ →
      MeasureTheory.UniformIntegrable f p μ →
        ∀ {ε : ℝ},
          0 < ε → ∃ C, ∀ (i : ι), MeasureTheory.eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Defined in

Mathlib.MeasureTheory.Function.UniformIntegrable

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroup