edist — Mathlib

English

If f is AEStronglyMeasurable, then its ENorm ‖f‖ₑ is almost everywhere measurable.

Русский

Если f AEStronglyMeasurable, то ‖f‖ₑ почти всюду измеримо.

LaTeX

$$$AEStronglyMeasurable(f, \mu) \Rightarrow AEMeasurable(\|f\|_e, \mu)$$$

Lean4

/-- Given a.e. strongly measurable functions `f` and `g`, `edist f g` is measurable.

Note that 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, aesop safe 20 apply (rule_sets := [Measurable]), fun_prop]
protected theorem edist {β : Type*} [PseudoMetricSpace β] {f g : α → β} (hf : AEStronglyMeasurable f μ)
    (hg : AEStronglyMeasurable g μ) : AEMeasurable (fun a => edist (f a) (g a)) μ :=
  (continuous_edist.comp_aestronglyMeasurable (hf.prodMk hg)).aemeasurable

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