Theorems · Theorem · measure theory

HasCompactSupport.memLp_of_bound

∀ {E : Type u_2} {p : ENNReal} [inst : NormedAddCommGroup E] {X : Type u_3} [inst_1 : TopologicalSpace X]
  [inst_2 : MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {f : X → E},
  HasCompactSupport f →
    MeasureTheory.AEStronglyMeasurable f μ → ∀ (C : ℝ), (∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C) → MeasureTheory.MemLp f p μ

A bounded measurable function with compact support is in L^p.

Defined in

Mathlib.MeasureTheory.Function.LpSpace.Indicator

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupTopologicalSpaceMeasurableSpaceMeasureTheory.IsFiniteMeasureOnCompacts