Fact 2.1 — generalized triangle inequality for power- distances
ProvedRobustFracMP.fact_2_1approximation-algorithmsclusteringfacility-locationlmp-approximationmetric-spacesp2o-gran-per-chapterp2o-plan-paperp2o-v1
Let be a metric space and an integer. For all ,
This replaces the triangle inequality for power- distances, which are not metrics for ; it is used in every smoothness and density bound of Section 3.1.
Differences from the source: none.
Preamble
import Mathlib set_option autoImplicit false
Formal statement
namespace RobustFracMP
/-- **Fact 2.1 (Generalized Triangle Inequality).**
Czumaj–Jiang–Jin–Lou–Wang, *Fully Scalable MPC Algorithms for Euclidean Clustering*,
arXiv:2604.00954 (version of November 3, 2026; manuscript sha256 c65896fe…51d8), Fact 2.1, p.10 (PDF p.12): "Let (P, dist) be a metric space. For any p, q, t ∈ P, it holds that
dist^z(p, q) ≤ 2^{z−1} · (dist^z(p, t) + dist^z(t, q))."
**Formalization Note.** `z : ℕ` with `1 ≤ z` (the standing assumption of p.10), so `z − 1` is the
true difference. The metric space need not be finite. -/
theorem fact_2_1 {P : Type*} [MetricSpace P] (z : ℕ) (hz : 1 ≤ z) (p q t : P) :
dist p q ^ z ≤ 2 ^ (z - 1) * (dist p t ^ z + dist t q ^ z) := by sorry
end RobustFracMP
Source
Czumaj–Jiang–Jin–Lou–Wang, Fully Scalable MPC Algorithms for Euclidean Clustering, arXiv:2604.00954 (version of November 3, 2026; manuscript sha256 c65896fe…51d8), Fact 2.1, p.10 (PDF p.12)
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.