# 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`.

source
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)⁻¹

Instances For

source
@[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.

source
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.

source
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.

source
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.

source
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.

source
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`.

source
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)

Instances For

source
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.

source
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
source
@[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.

source
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.

source
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.

source
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`.

source
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)

Instances For

source
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`.

source
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`.

source
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.

source
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.

source
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`.

source
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`.

source
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.

source
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 `Finset`s and with the same points in the image of those `Finset`s have the same centroid.

source
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.

source
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.

source
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.

source
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`.