The Lᵖ seminorm of a displacement is that of the distance

On a seminormed additive group E the extended distance is the extended norm of the difference, edist x y = ‖x - y‖ₑ. So under any measure π on E × E the displacement (x, y) ↦ x - y and the ground distance (x, y) ↦ edist x y have the same Lᵖ seminorm (MeasureTheory.eLpNorm_sub_eq_eLpNorm_edist). This turns an Lᵖ cost written with edist, as in optimal transport, into the Lᵖ seminorm of an E-valued function, to which the linear structure of E applies (for instance, scaling by a constant).

The measurability assumptions on E make both functions almost everywhere strongly measurable, which MeasureTheory.eLpNorm_congr_enorm_ae needs.

On a pseudometric space, MeasureTheory.memLp_dist_iff_memLp_edist likewise identifies membership in Lᵖ of the real distance to a basepoint with that of the extended distance.

The Minkowski estimate MeasureTheory.eLpNorm_edist_le_add bounds the Lᵖ seminorm of x ↦ edist (f' x) (g' x) by that of x ↦ edist (f x) (g x) plus the seminorms of the two displacements x ↦ edist (f x) (f' x) and x ↦ edist (g x) (g' x).

theorem MeasureTheory.eLpNorm_sub_eq_eLpNorm_edist {E : Type u_1} [SeminormedAddCommGroup E] [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopology E] (p : ENNReal) (π : Measure (E × E)) : eLpNorm (fun (z : E × E) => z.1 - z.2) p π = eLpNorm (fun (z : E × E) => edist z.1 z.2) p π

Under any law π on pairs of points of a seminormed group, the displacement x - y and the ground distance edist x y have the same Lᵖ seminorm.

theorem MeasureTheory.memLp_dist_iff_memLp_edist {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] {p : ENNReal} {x : X} {ν : Measure X} : MemLp (fun (y : X) => dist y x) p ν ↔ MemLp (fun (y : X) => edist x y) p ν

On a pseudometric space, the real-distance and extended-distance formulations of finite p-moment at a basepoint agree.

theorem MeasureTheory.eLpNorm_edist_le_add {α : Type u_1} {Y : Type u_2} {m : MeasurableSpace α} [PseudoEMetricSpace Y] {p : ENNReal} {μ : Measure α} {f g f' g' : α → Y} (hp1 : 1 ≤ p) (hmeas : AEStronglyMeasurable (fun (x : α) => edist (f' x) (g' x)) μ) : eLpNorm (fun (x : α) => edist (f' x) (g' x)) p μ ≤ eLpNorm (fun (x : α) => edist (f x) (g x)) p μ + (eLpNorm (fun (x : α) => edist (f x) (f' x)) p μ + eLpNorm (fun (x : α) => edist (g x) (g' x)) p μ)

Minkowski bound for distances. For maps f g f' g' : α → Y into a pseudo-emetric space and 1 ≤ p, the Lᵖ(μ) seminorm of x ↦ edist (f' x) (g' x) is at most that of x ↦ edist (f x) (g x) plus those of the two displacements x ↦ edist (f x) (f' x) and x ↦ edist (g x) (g' x).