Theorems · Theorem · measure theory

MeasureTheory.StronglyMeasurable.enorm

∀ {α : Type u_1} {x : MeasurableSpace α} {ε : Type u_5} [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε]
  {f : α → ε}, MeasureTheory.StronglyMeasurable f → Measurable fun x => ‖f x‖ₑ

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

Defined in

Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Cited by

19 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceContinuousENorm