The ℓ^p product distance as a measurable function

For a positive finite exponent p the extended distance on WithLp p (X × Y) is the ℓ^p combination (d₁ ^ p + d₂ ^ p) ^ (1 / p) of the two factor distances. This file records the two facts that make that distance usable as the ground distance of a measure-theoretic construction on the product: raising it to the power p makes it additive in the two factors, and it is jointly measurable for every exponent, including 0 and ∞, as soon as the two factor distances are.

The measurable structure of WithLp p (X × Y) is the one pulled back from X × Y, so measurability is a statement about the product measurable space and only the distance changes along the type synonym.

Main statements

• TauCeti.edist_toLp_rpow — the p-th power of the ℓ^p product distance is the sum of the p-th powers of the two factor distances;
• TauCeti.measurable_edist_toLp_prod — joint measurability of the ℓ^p product distance.

theorem TauCeti.edist_toLp_rpow {p : ENNReal} {X : Type u} {Y : Type v} [EDist X] [EDist Y] (hp : 0 < p.toReal) (z w : X × Y) : edist (WithLp.toLp p z) (WithLp.toLp p w) ^ p.toReal = edist z.1 w.1 ^ p.toReal + edist z.2 w.2 ^ p.toReal

Raising the ℓ^p product distance to the power p makes it additive in the two factors.

theorem TauCeti.measurable_edist_toLp_prod {p : ENNReal} {X : Type u} {Y : Type v} [EDist X] [EDist Y] [MeasurableSpace X] [MeasurableSpace Y] (hdX : Measurable fun (z : X × X) => edist z.1 z.2) (hdY : Measurable fun (z : Y × Y) => edist z.1 z.2) : Measurable fun (w : WithLp p (X × Y) × WithLp p (X × Y)) => edist w.1 w.2

The ℓ^p product distance is jointly measurable for every exponent, including 0 and ∞, as soon as the two factor distances are.