nnnorm — Mathlib

English

If f is AEMeasurable, then a.e.-measurable version of its NN norm is AEMeasurable.

Русский

Если f а.е.-измерима, то a.e.-измеримая версия её NN-нормы также а.е.-измерима.

LaTeX

$$$AEMeasurable f \\mu \\Rightarrow AEMeasurable (\\lambda a. \\text{SeminormedAddGroup.toNNNorm}.nnnorm (f a)) \\mu$$$

Lean4

@[measurability, fun_prop]
protected theorem nnnorm {f : β → α} {μ : Measure β} (hf : AEMeasurable f μ) : AEMeasurable (fun a => ‖f a‖₊) μ :=
  measurable_nnnorm.comp_aemeasurable hf

Похожие утверждения