Truncating powers of distances by tails about a basepoint

In a pseudometric space a displacement larger than 2 R forces one of its two endpoints to lie at distance at least R from a basepoint x, and then the displacement is at most twice that distance. Consequently the q-th power of a displacement is at most its truncation at 2 R plus 2 ^ q times the parts, beyond distance R from x, of the q-th powers of the distances of the two endpoints from x. This is the pointwise estimate through which the tails of the moments of two laws control the transport cost of an unbounded power of the distance.

Main statements

• TauCeti.coe_nndist_rpow — the nonnegative and extended powers of a distance agree;
• TauCeti.continuous_nndist_rpow_const — a nonnegative power of distance from a fixed point is continuous;
• TauCeti.edist_rpow_le_min_add_indicator — the pointwise truncation estimate, for every real exponent.

theorem TauCeti.coe_nndist_rpow {X : Type u_1} [PseudoMetricSpace X] {q : ℝ} (hq : 0 ≤ q) (x y : X) : ↑(nndist x y ^ q) = edist x y ^ q

The q-th power of the nonnegative distance, coerced to ℝ≥0∞, is the q-th power of the extended distance.

theorem TauCeti.continuous_nndist_rpow_const {X : Type u_1} [PseudoMetricSpace X] {q : ℝ} (hq : 0 ≤ q) (x : X) : Continuous fun (y : X) => nndist x y ^ q

The nonnegative distance to a fixed point, raised to a nonnegative power, is continuous.

theorem TauCeti.edist_rpow_le_min_add_indicator {X : Type u_1} [PseudoMetricSpace X] {q : ℝ} (x : X) (R : NNReal) (y z : X) : edist y z ^ q ≤ min (edist y z) (2 * ↑R) ^ q + 2 ^ q * {w : X | R ≤ nndist x w}.indicator (fun (w : X) => edist x w ^ q) y + 2 ^ q * {w : X | R ≤ nndist x w}.indicator (fun (w : X) => edist x w ^ q) z

A displacement larger than 2 R is at most twice the distance from the basepoint x of an endpoint lying at distance at least R from it. Hence the q-th power of the displacement is at most its truncation at 2 R plus 2 ^ q times the tail parts, beyond R, of the q-th powers of the distances of the two endpoints from x. For a negative exponent the truncation alone already bounds the power.