Theorems · Theorem · measure theory

MeasureTheory.exists_eLpNorm_indicator_le

∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E],
  p ≠ ⊤ →
    ∀ (c : E) {ε : ENNReal},
      ε ≠ 0 → ∃ η, 0 < η ∧ ∀ (s : Set α), μ s ≤ ↑η → MeasureTheory.eLpNorm (s.indicator fun x => c) p μ ≤ ε

The eLpNorm of the indicator of a set is uniformly small if the set itself has small measure, for any p < ∞. Given here as an existential ∀ ε > 0, ∃ η > 0, ... to avoid later management of ℝ≥0∞-arithmetic.

Defined in

Mathlib.MeasureTheory.Function.LpSpace.Indicator

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroup