Distances to the centroid of finitely many points

For a nonempty finite family of points p i, i ∈ s, in a pseudometric affine space over a real seminormed space, whose pairwise distances are at most d, the centroid s.centroid ℝ p lies within (1 - 1 / #s) * d of each point p j, j ∈ s. More precisely, the centroid of a nonempty subfamily t ⊆ s lies within (1 - #t / #s) * d of the whole family’s centroid. These are the estimates behind the shrinking of barycentric subdivision: the vertices of a simplex of the barycentric subdivision of a k-simplex of diameter d are centroids of nested faces, hence lie within k / (k + 1) * d of each other.

Main results

• Finset.dist_centroid_le_sum_dist: distance to the centroid is bounded by the average distance.
• Finset.dist_centroid_le: the centroid lies in every closed ball containing the points.
• Finset.dist_centroid_apply_le: the distance from the centroid to one of the points.
• Finset.dist_centroid_centroid_le_of_subset: the distance between the centroids of a family and of a nonempty subfamily.

References

• A. Hatcher, Algebraic Topology, Section 2.1, proof of Proposition 2.21, step (2).

theorem Finset.dist_centroid_le_sum_dist {ι : Type u_1} {s : Finset ι} {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] {p : ι → P} (hs : s.Nonempty) (q : P) : dist (centroid ℝ s p) q ≤ (↑s.card)⁻¹ * ∑ i ∈ s, dist (p i) q

Distance to the centroid is at most the average distance to the points.

theorem Finset.dist_centroid_le {ι : Type u_1} {s : Finset ι} {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] {p : ι → P} (hs : s.Nonempty) {q : P} {r : ℝ} (h : ∀ i ∈ s, dist (p i) q ≤ r) : dist (centroid ℝ s p) q ≤ r

The centroid of a nonempty family of points lies in every closed ball containing all of them.

theorem Finset.dist_centroid_centroid_le_of_subset {ι : Type u_1} {s t : Finset ι} {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] {p : ι → P} [DecidableEq ι] {d : ℝ} (hd : ∀ i ∈ s \ t, ∀ j ∈ t, dist (p i) (p j) ≤ d) (hts : t ⊆ s) (ht : t.Nonempty) : dist (centroid ℝ t p) (centroid ℝ s p) ≤ (1 - ↑t.card / ↑s.card) * d

If the distances from points outside a nonempty subfamily to points inside it are at most d, the centroids are at distance at most (1 - #t / #s) * d. In particular, the bound is zero when the two index sets agree.

theorem Finset.dist_centroid_apply_le {ι : Type u_1} {s : Finset ι} {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] {p : ι → P} [DecidableEq ι] {d : ℝ} {j : ι} (hd : ∀ i ∈ s.erase j, dist (p i) (p j) ≤ d) (hj : j ∈ s) : dist (centroid ℝ s p) (p j) ≤ (1 - (↑s.card)⁻¹) * d

If j ∈ s and the other points p i, i ∈ s.erase j, are at distance at most d from p j, then the centroid lies within (1 - 1 / #s) * d of p j.