Theorems · Theorem · measure theory

MeasureTheory.AEStronglyMeasurable.edist

∀ {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [inst : PseudoMetricSpace β]
  {f g : α → β},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → AEMeasurable (fun a => edist (f a) (g a)) μ

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.

Defined in

Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Cited by

1 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpace