English
For a semifnormed group β, if f is AEStronglyMeasurable, then x ↦ ‖f(x)‖ is AEStronglyMeasurable.
Русский
Для полугруппы с нормой β, если f AEStronglyMeasurable, то x ↦ \|f(x)\| является AEStronglyMeasurable.
LaTeX
$$$AEStronglyMeasurable(f, \mu) \Rightarrow AEStronglyMeasurable(\lambda x. \|f(x)\|, \mu)$$$
Lean4
/-- 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. -/
@[fun_prop, measurability]
protected theorem enorm {β : Type*} [TopologicalSpace β] [ContinuousENorm β] {f : α → β}
(hf : AEStronglyMeasurable f μ) : AEMeasurable (‖f ·‖ₑ) μ :=
(continuous_enorm.comp_aestronglyMeasurable hf).aemeasurable
