Centroid of a Finite Set of Points in Affine Space

This file defines the centroid of a finite set of points in an affine space over a division ring.

Main definitions

• centroidWeights: A constant weight function assigning to each index in a Finset the same weight, equal to the reciprocal of the number of elements.

• centroid: the centroid of a Finset of points, defined as the affine combination using centroidWeights.

def Finset.centroidWeights (k : Type u_1) [DivisionRing k] {ι : Type u_4} (s : Finset ι) : ι → k

The weights for the centroid of some points.

Equations

• Finset.centroidWeights k s = Function.const ι (↑s.card)⁻¹

@[simp]

theorem Finset.centroidWeights_apply (k : Type u_1) [DivisionRing k] {ι : Type u_4} (s : Finset ι) (i : ι) : centroidWeights k s i = (↑s.card)⁻¹

centroidWeights at any point.

theorem Finset.centroidWeights_eq_const (k : Type u_1) [DivisionRing k] {ι : Type u_4} (s : Finset ι) : centroidWeights k s = Function.const ι (↑s.card)⁻¹

centroidWeights equals a constant function.

theorem Finset.sum_centroidWeights_eq_one_of_cast_card_ne_zero {k : Type u_1} [DivisionRing k] {ι : Type u_4} (s : Finset ι) (h : ↑s.card ≠ 0) : ∑ i ∈ s, centroidWeights k s i = 1

The weights in the centroid sum to 1, if the number of points, converted to k, is not zero.

theorem Finset.sum_centroidWeights_eq_one_of_card_ne_zero (k : Type u_1) [DivisionRing k] {ι : Type u_4} (s : Finset ι) [CharZero k] (h : s.card ≠ 0) : ∑ i ∈ s, centroidWeights k s i = 1

In the characteristic zero case, the weights in the centroid sum to 1 if the number of points is not zero.

theorem Finset.sum_centroidWeights_eq_one_of_nonempty (k : Type u_1) [DivisionRing k] {ι : Type u_4} (s : Finset ι) [CharZero k] (h : s.Nonempty) : ∑ i ∈ s, centroidWeights k s i = 1

In the characteristic zero case, the weights in the centroid sum to 1 if the set is nonempty.

theorem Finset.sum_centroidWeights_eq_one_of_card_eq_add_one (k : Type u_1) [DivisionRing k] {ι : Type u_4} (s : Finset ι) [CharZero k] {n : ℕ} (h : s.card = n + 1) : ∑ i ∈ s, centroidWeights k s i = 1

In the characteristic zero case, the weights in the centroid sum to 1 if the number of points is n + 1.

def Finset.centroid (k : Type u_1) {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} (s : Finset ι) (p : ι → P) : P

The centroid of some points. Although defined for any s, this is intended to be used in the case where the number of points, converted to k, is not zero.

Equations

• Finset.centroid k s p = (Finset.affineCombination k s p) (Finset.centroidWeights k s)

theorem Finset.centroid_def (k : Type u_1) {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} (s : Finset ι) (p : ι → P) : centroid k s p = (affineCombination k s p) (centroidWeights k s)

The definition of the centroid.

theorem Finset.centroid_univ (k : Type u_1) {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Finset P) : centroid k univ Subtype.val = centroid k s id

@[simp]

theorem Finset.centroid_singleton (k : Type u_1) {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} (p : ι → P) (i : ι) : centroid k {i} p = p i

The centroid of a single point.

theorem Finset.centroid_pair (k : Type u_1) {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} [DecidableEq ι] [Invertible 2] (p : ι → P) (i₁ i₂ : ι) : centroid k {i₁, i₂} p = 2⁻¹ • (p i₂ -ᵥ p i₁) +ᵥ p i₁

The centroid of two points, expressed directly as adding a vector to a point.

theorem Finset.centroid_pair_fin (k : Type u_1) {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Invertible 2] (p : Fin 2 → P) : centroid k univ p = 2⁻¹ • (p 1 -ᵥ p 0) +ᵥ p 0

The centroid of two points indexed by Fin 2, expressed directly as adding a vector to the first point.

theorem Finset.centroid_map (k : Type u_1) {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {ι₂ : Type u_5} (s₂ : Finset ι₂) (e : ι₂ ↪ ι) (p : ι → P) : centroid k (map e s₂) p = centroid k s₂ (p ∘ ⇑e)

A centroid, over the image of an embedding, equals a centroid with the same points and weights over the original Finset.

def Finset.centroidWeightsIndicator (k : Type u_1) [DivisionRing k] {ι : Type u_4} (s : Finset ι) : ι → k

centroidWeights gives the weights for the centroid as a constant function, which is suitable when summing over the points whose centroid is being taken. This function gives the weights in a form suitable for summing over a larger set of points, as an indicator function that is zero outside the set whose centroid is being taken. In the case of a Fintype, the sum may be over univ.

Equations

• Finset.centroidWeightsIndicator k s = (↑s).indicator (Finset.centroidWeights k s)

theorem Finset.centroidWeightsIndicator_def (k : Type u_1) [DivisionRing k] {ι : Type u_4} (s : Finset ι) : centroidWeightsIndicator k s = (↑s).indicator (centroidWeights k s)

The definition of centroidWeightsIndicator.

theorem Finset.sum_centroidWeightsIndicator (k : Type u_1) [DivisionRing k] {ι : Type u_4} (s : Finset ι) [Fintype ι] : ∑ i : ι, centroidWeightsIndicator k s i = ∑ i ∈ s, centroidWeights k s i

The sum of the weights for the centroid indexed by a Fintype.

theorem Finset.sum_centroidWeightsIndicator_eq_one_of_card_ne_zero (k : Type u_1) [DivisionRing k] {ι : Type u_4} (s : Finset ι) [CharZero k] [Fintype ι] (h : s.card ≠ 0) : ∑ i : ι, centroidWeightsIndicator k s i = 1

In the characteristic zero case, the weights in the centroid indexed by a Fintype sum to 1 if the number of points is not zero.

theorem Finset.sum_centroidWeightsIndicator_eq_one_of_nonempty (k : Type u_1) [DivisionRing k] {ι : Type u_4} (s : Finset ι) [CharZero k] [Fintype ι] (h : s.Nonempty) : ∑ i : ι, centroidWeightsIndicator k s i = 1

In the characteristic zero case, the weights in the centroid indexed by a Fintype sum to 1 if the set is nonempty.

theorem Finset.sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one (k : Type u_1) [DivisionRing k] {ι : Type u_4} (s : Finset ι) [CharZero k] [Fintype ι] {n : ℕ} (h : s.card = n + 1) : ∑ i : ι, centroidWeightsIndicator k s i = 1

In the characteristic zero case, the weights in the centroid indexed by a Fintype sum to 1 if the number of points is n + 1.

theorem Finset.centroid_eq_affineCombination_fintype (k : Type u_1) {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} (s : Finset ι) [Fintype ι] (p : ι → P) : centroid k s p = (affineCombination k univ p) (centroidWeightsIndicator k s)

The centroid as an affine combination over a Fintype.

theorem Finset.centroid_eq_centroid_image_of_inj_on (k : Type u_1) {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} (s : Finset ι) {p : ι → P} (hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j) {ps : Set P} [Fintype ↑ps] (hps : ps = p '' ↑s) : centroid k s p = centroid k univ fun (x : ↑ps) => ↑x

An indexed family of points that is injective on the given Finset has the same centroid as the image of that Finset. This is stated in terms of a set equal to the image to provide control of definitional equality for the index type used for the centroid of the image.

theorem Finset.centroid_eq_of_inj_on_of_image_eq (k : Type u_1) {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} (s : Finset ι) {ι₂ : Type u_5} (s₂ : Finset ι₂) {p : ι → P} (hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j) {p₂ : ι₂ → P} (hi₂ : ∀ i ∈ s₂, ∀ j ∈ s₂, p₂ i = p₂ j → i = j) (he : p '' ↑s = p₂ '' ↑s₂) : centroid k s p = centroid k s₂ p₂

Two indexed families of points that are injective on the given Finsets and with the same points in the image of those Finsets have the same centroid.

theorem centroid_mem_affineSpan_of_cast_card_ne_zero {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {s : Finset ι} (p : ι → P) (h : ↑s.card ≠ 0) : Finset.centroid k s p ∈ affineSpan k (Set.range p)

The centroid lies in the affine span if the number of points, converted to k, is not zero.

theorem centroid_mem_affineSpan_of_card_ne_zero (k : Type u_1) {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} [CharZero k] {s : Finset ι} (p : ι → P) (h : s.card ≠ 0) : Finset.centroid k s p ∈ affineSpan k (Set.range p)

In the characteristic zero case, the centroid lies in the affine span if the number of points is not zero.

theorem centroid_mem_affineSpan_of_nonempty (k : Type u_1) {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} [CharZero k] {s : Finset ι} (p : ι → P) (h : s.Nonempty) : Finset.centroid k s p ∈ affineSpan k (Set.range p)

In the characteristic zero case, the centroid lies in the affine span if the set is nonempty.

theorem centroid_mem_affineSpan_of_card_eq_add_one (k : Type u_1) {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} [CharZero k] {s : Finset ι} (p : ι → P) {n : ℕ} (h : s.card = n + 1) : Finset.centroid k s p ∈ affineSpan k (Set.range p)

In the characteristic zero case, the centroid lies in the affine span if the number of points is n + 1.