Theorems · Theorem · measure theory

MeasureTheory.AEStronglyMeasurable.enorm

∀ {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [inst : TopologicalSpace β]
  [inst_1 : ContinuousENorm β] {f : α → β}, MeasureTheory.AEStronglyMeasurable f μ → AEMeasurable (fun x => ‖f x‖ₑ) μ

The enorm of a strongly a.e. measurable function is a.e. measurable. Note that unlike AEStronglyMeasurable.norm and AEStronglyMeasurable.nnnorm, this lemma proves a.e. measurability, not a.e. strong measurability. This is an intentional decision: for functions taking values in ℝ≥0∞, a.e. measurability is much more useful than a.e. strong measurability.

Defined in

Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Cited by

29 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceContinuousENorm