Power bounds for extended distances

For nonnegative real exponents, the triangle inequality gives a split upper bound for a power of the extended distance in terms of powers of the distances from any fixed basepoint.

theorem TauCeti.edist_rpow_le_mul_edist_rpow_add_mul_edist_rpow {X : Type u_1} [TopologicalSpace X] [WeakPseudoEMetricSpace X] {r : ℝ} (hr : 0 ≤ r) (x₀ x y : X) : edist x y ^ r ≤ (ENNReal.ofReal r)⁻¹.LpAddConst * edist x₀ x ^ r + (ENNReal.ofReal r)⁻¹.LpAddConst * edist x₀ y ^ r

The split bound for a power of the distance. For a nonnegative exponent r, the cost edist x y ^ r is bounded by K * edist x₀ x ^ r + K * edist x₀ y ^ r about any basepoint x₀, with the finite constant K = ENNReal.LpAddConst (ENNReal.ofReal r)⁻¹.