Affine combinations of points

This file defines affine combinations of points.

Main definitions

• weightedVSubOfPoint is a general weighted combination of subtractions with an explicit base point, yielding a vector.

• weightedVSub uses an arbitrary choice of base point and is intended to be used when the sum of weights is 0, in which case the result is independent of the choice of base point.

• affineCombination adds the weighted combination to the arbitrary base point, yielding a point rather than a vector, and is intended to be used when the sum of weights is 1, in which case the result is independent of the choice of base point.

These definitions are for sums over a Finset; versions for a Fintype may be obtained using Finset.univ, while versions for a Finsupp may be obtained using Finsupp.support.

References

• https://en.wikipedia.org/wiki/Affine_space

theorem Finset.univ_fin2 : Finset.univ = {0, 1}

def Finset.weightedVSubOfPoint {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (p : ι → P) (b : P) : (ι → k) →ₗ[k] V

A weighted sum of the results of subtracting a base point from the given points, as a linear map on the weights. The main cases of interest are where the sum of the weights is 0, in which case the sum is independent of the choice of base point, and where the sum of the weights is 1, in which case the sum added to the base point is independent of the choice of base point.

Equations

• Finset.weightedVSubOfPoint s p b = Finset.sum s fun (i : ι) => LinearMap.smulRight (LinearMap.proj i) (p i -ᵥ b)

@[simp]

theorem Finset.weightedVSubOfPoint_apply {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) (b : P) : (Finset.weightedVSubOfPoint s p b) w = Finset.sum s fun (i : ι) => w i • (p i -ᵥ b)

@[simp]

theorem Finset.weightedVSubOfPoint_apply_const {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : P) (b : P) : (Finset.weightedVSubOfPoint s (fun (x : ι) => p) b) w = (Finset.sum s fun (i : ι) => w i) • (p -ᵥ b)

The value of weightedVSubOfPoint, where the given points are equal.

theorem Finset.weightedVSubOfPoint_congr {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) {w₁ : ι → k} {w₂ : ι → k} (hw : ∀ i ∈ s, w₁ i = w₂ i) {p₁ : ι → P} {p₂ : ι → P} (hp : ∀ i ∈ s, p₁ i = p₂ i) (b : P) : (Finset.weightedVSubOfPoint s p₁ b) w₁ = (Finset.weightedVSubOfPoint s p₂ b) w₂

weightedVSubOfPoint gives equal results for two families of weights and two families of points that are equal on s.

theorem Finset.weightedVSubOfPoint_eq_of_weights_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (p : ι → P) (j : ι) (w₁ : ι → k) (w₂ : ι → k) (hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i) : (Finset.weightedVSubOfPoint s p (p j)) w₁ = (Finset.weightedVSubOfPoint s p (p j)) w₂

Given a family of points, if we use a member of the family as a base point, the weightedVSubOfPoint does not depend on the value of the weights at this point.

theorem Finset.weightedVSubOfPoint_eq_of_sum_eq_zero {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) (h : (Finset.sum s fun (i : ι) => w i) = 0) (b₁ : P) (b₂ : P) : (Finset.weightedVSubOfPoint s p b₁) w = (Finset.weightedVSubOfPoint s p b₂) w

The weighted sum is independent of the base point when the sum of the weights is 0.

theorem Finset.weightedVSubOfPoint_vadd_eq_of_sum_eq_one {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) (h : (Finset.sum s fun (i : ι) => w i) = 1) (b₁ : P) (b₂ : P) : (Finset.weightedVSubOfPoint s p b₁) w +ᵥ b₁ = (Finset.weightedVSubOfPoint s p b₂) w +ᵥ b₂

The weighted sum, added to the base point, is independent of the base point when the sum of the weights is 1.

@[simp]

theorem Finset.weightedVSubOfPoint_erase {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [DecidableEq ι] (w : ι → k) (p : ι → P) (i : ι) : (Finset.weightedVSubOfPoint (Finset.erase s i) p (p i)) w = (Finset.weightedVSubOfPoint s p (p i)) w

The weighted sum is unaffected by removing the base point, if present, from the set of points.

@[simp]

theorem Finset.weightedVSubOfPoint_insert {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [DecidableEq ι] (w : ι → k) (p : ι → P) (i : ι) : (Finset.weightedVSubOfPoint (insert i s) p (p i)) w = (Finset.weightedVSubOfPoint s p (p i)) w

The weighted sum is unaffected by adding the base point, whether or not present, to the set of points.

theorem Finset.weightedVSubOfPoint_indicator_subset {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (w : ι → k) (p : ι → P) (b : P) {s₁ : Finset ι} {s₂ : Finset ι} (h : s₁ ⊆ s₂) : (Finset.weightedVSubOfPoint s₁ p b) w = (Finset.weightedVSubOfPoint s₂ p b) (Set.indicator (↑s₁) w)

The weighted sum is unaffected by changing the weights to the corresponding indicator function and adding points to the set.

theorem Finset.weightedVSubOfPoint_map {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} {ι₂ : Type u_5} (s₂ : Finset ι₂) (e : ι₂ ↪ ι) (w : ι → k) (p : ι → P) (b : P) : (Finset.weightedVSubOfPoint (Finset.map e s₂) p b) w = (Finset.weightedVSubOfPoint s₂ (p ∘ ⇑e) b) (w ∘ ⇑e)

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

theorem Finset.sum_smul_vsub_eq_weightedVSubOfPoint_sub {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p₁ : ι → P) (p₂ : ι → P) (b : P) : (Finset.sum s fun (i : ι) => w i • (p₁ i -ᵥ p₂ i)) = (Finset.weightedVSubOfPoint s p₁ b) w - (Finset.weightedVSubOfPoint s p₂ b) w

A weighted sum of pairwise subtractions, expressed as a subtraction of two weightedVSubOfPoint expressions.

theorem Finset.sum_smul_vsub_const_eq_weightedVSubOfPoint_sub {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p₁ : ι → P) (p₂ : P) (b : P) : (Finset.sum s fun (i : ι) => w i • (p₁ i -ᵥ p₂)) = (Finset.weightedVSubOfPoint s p₁ b) w - (Finset.sum s fun (i : ι) => w i) • (p₂ -ᵥ b)

A weighted sum of pairwise subtractions, where the point on the right is constant, expressed as a subtraction involving a weightedVSubOfPoint expression.

theorem Finset.sum_smul_const_vsub_eq_sub_weightedVSubOfPoint {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p₂ : ι → P) (p₁ : P) (b : P) : (Finset.sum s fun (i : ι) => w i • (p₁ -ᵥ p₂ i)) = (Finset.sum s fun (i : ι) => w i) • (p₁ -ᵥ b) - (Finset.weightedVSubOfPoint s p₂ b) w

A weighted sum of pairwise subtractions, where the point on the left is constant, expressed as a subtraction involving a weightedVSubOfPoint expression.

theorem Finset.weightedVSubOfPoint_sdiff {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [DecidableEq ι] {s₂ : Finset ι} (h : s₂ ⊆ s) (w : ι → k) (p : ι → P) (b : P) : (Finset.weightedVSubOfPoint (s \ s₂) p b) w + (Finset.weightedVSubOfPoint s₂ p b) w = (Finset.weightedVSubOfPoint s p b) w

A weighted sum may be split into such sums over two subsets.

theorem Finset.weightedVSubOfPoint_sdiff_sub {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [DecidableEq ι] {s₂ : Finset ι} (h : s₂ ⊆ s) (w : ι → k) (p : ι → P) (b : P) : (Finset.weightedVSubOfPoint (s \ s₂) p b) w - (Finset.weightedVSubOfPoint s₂ p b) (-w) = (Finset.weightedVSubOfPoint s p b) w

A weighted sum may be split into a subtraction of such sums over two subsets.

theorem Finset.weightedVSubOfPoint_subtype_eq_filter {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) (b : P) (pred : ι → Prop) [DecidablePred pred] : ((Finset.weightedVSubOfPoint (Finset.subtype pred s) (fun (i : Subtype pred) => p ↑i) b) fun (i : Subtype pred) => w ↑i) = (Finset.weightedVSubOfPoint (Finset.filter pred s) p b) w

A weighted sum over s.subtype pred equals one over s.filter pred.

theorem Finset.weightedVSubOfPoint_filter_of_ne {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) (b : P) {pred : ι → Prop} [DecidablePred pred] (h : ∀ i ∈ s, w i ≠ 0 → pred i) : (Finset.weightedVSubOfPoint (Finset.filter pred s) p b) w = (Finset.weightedVSubOfPoint s p b) w

A weighted sum over s.filter pred equals one over s if all the weights at indices in s not satisfying pred are zero.

theorem Finset.weightedVSubOfPoint_const_smul {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) (b : P) (c : k) : (Finset.weightedVSubOfPoint s p b) (c • w) = c • (Finset.weightedVSubOfPoint s p b) w

A constant multiplier of the weights in weightedVSubOfPoint may be moved outside the sum.

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

A weighted sum of the results of subtracting a default base point from the given points, as a linear map on the weights. This is intended to be used when the sum of the weights is 0; that condition is specified as a hypothesis on those lemmas that require it.

Equations

• Finset.weightedVSub s p = Finset.weightedVSubOfPoint s p (Classical.choice (_ : Nonempty P))

theorem Finset.weightedVSub_apply {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) : (Finset.weightedVSub s p) w = Finset.sum s fun (i : ι) => w i • (p i -ᵥ Classical.choice (_ : Nonempty P))

Applying weightedVSub with given weights. This is for the case where a result involving a default base point is OK (for example, when that base point will cancel out later); a more typical use case for weightedVSub would involve selecting a preferred base point with weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero and then using weightedVSubOfPoint_apply.

theorem Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) (h : (Finset.sum s fun (i : ι) => w i) = 0) (b : P) : (Finset.weightedVSub s p) w = (Finset.weightedVSubOfPoint s p b) w

weightedVSub gives the sum of the results of subtracting any base point, when the sum of the weights is 0.

@[simp]

theorem Finset.weightedVSub_apply_const {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : P) (h : (Finset.sum s fun (i : ι) => w i) = 0) : (Finset.weightedVSub s fun (x : ι) => p) w = 0

The value of weightedVSub, where the given points are equal and the sum of the weights is 0.

@[simp]

theorem Finset.weightedVSub_empty {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (w : ι → k) (p : ι → P) : (Finset.weightedVSub ∅ p) w = 0

The weightedVSub for an empty set is 0.

theorem Finset.weightedVSub_congr {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) {w₁ : ι → k} {w₂ : ι → k} (hw : ∀ i ∈ s, w₁ i = w₂ i) {p₁ : ι → P} {p₂ : ι → P} (hp : ∀ i ∈ s, p₁ i = p₂ i) : (Finset.weightedVSub s p₁) w₁ = (Finset.weightedVSub s p₂) w₂

weightedVSub gives equal results for two families of weights and two families of points that are equal on s.

theorem Finset.weightedVSub_indicator_subset {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (w : ι → k) (p : ι → P) {s₁ : Finset ι} {s₂ : Finset ι} (h : s₁ ⊆ s₂) : (Finset.weightedVSub s₁ p) w = (Finset.weightedVSub s₂ p) (Set.indicator (↑s₁) w)

The weighted sum is unaffected by changing the weights to the corresponding indicator function and adding points to the set.

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

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

theorem Finset.sum_smul_vsub_eq_weightedVSub_sub {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p₁ : ι → P) (p₂ : ι → P) : (Finset.sum s fun (i : ι) => w i • (p₁ i -ᵥ p₂ i)) = (Finset.weightedVSub s p₁) w - (Finset.weightedVSub s p₂) w

A weighted sum of pairwise subtractions, expressed as a subtraction of two weightedVSub expressions.

theorem Finset.sum_smul_vsub_const_eq_weightedVSub {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p₁ : ι → P) (p₂ : P) (h : (Finset.sum s fun (i : ι) => w i) = 0) : (Finset.sum s fun (i : ι) => w i • (p₁ i -ᵥ p₂)) = (Finset.weightedVSub s p₁) w

A weighted sum of pairwise subtractions, where the point on the right is constant and the sum of the weights is 0.

theorem Finset.sum_smul_const_vsub_eq_neg_weightedVSub {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p₂ : ι → P) (p₁ : P) (h : (Finset.sum s fun (i : ι) => w i) = 0) : (Finset.sum s fun (i : ι) => w i • (p₁ -ᵥ p₂ i)) = -(Finset.weightedVSub s p₂) w

A weighted sum of pairwise subtractions, where the point on the left is constant and the sum of the weights is 0.

theorem Finset.weightedVSub_sdiff {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [DecidableEq ι] {s₂ : Finset ι} (h : s₂ ⊆ s) (w : ι → k) (p : ι → P) : (Finset.weightedVSub (s \ s₂) p) w + (Finset.weightedVSub s₂ p) w = (Finset.weightedVSub s p) w

A weighted sum may be split into such sums over two subsets.

theorem Finset.weightedVSub_sdiff_sub {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [DecidableEq ι] {s₂ : Finset ι} (h : s₂ ⊆ s) (w : ι → k) (p : ι → P) : (Finset.weightedVSub (s \ s₂) p) w - (Finset.weightedVSub s₂ p) (-w) = (Finset.weightedVSub s p) w

A weighted sum may be split into a subtraction of such sums over two subsets.

theorem Finset.weightedVSub_subtype_eq_filter {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) (pred : ι → Prop) [DecidablePred pred] : ((Finset.weightedVSub (Finset.subtype pred s) fun (i : Subtype pred) => p ↑i) fun (i : Subtype pred) => w ↑i) = (Finset.weightedVSub (Finset.filter pred s) p) w

A weighted sum over s.subtype pred equals one over s.filter pred.

theorem Finset.weightedVSub_filter_of_ne {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) {pred : ι → Prop} [DecidablePred pred] (h : ∀ i ∈ s, w i ≠ 0 → pred i) : (Finset.weightedVSub (Finset.filter pred s) p) w = (Finset.weightedVSub s p) w

A weighted sum over s.filter pred equals one over s if all the weights at indices in s not satisfying pred are zero.

theorem Finset.weightedVSub_const_smul {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) (c : k) : (Finset.weightedVSub s p) (c • w) = c • (Finset.weightedVSub s p) w

A constant multiplier of the weights in weightedVSub_of may be moved outside the sum.

instance Finset.instAddTorsorForAllAddGroupToAddGroupToAddGroupWithOne {k : Type u_1} [Ring k] {ι : Type u_4} : AddTorsor (ι → k) (ι → k)

Equations

• Finset.instAddTorsorForAllAddGroupToAddGroupToAddGroupWithOne = Pi.instAddTorsor

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

A weighted sum of the results of subtracting a default base point from the given points, added to that base point, as an affine map on the weights. This is intended to be used when the sum of the weights is 1, in which case it is an affine combination (barycenter) of the points with the given weights; that condition is specified as a hypothesis on those lemmas that require it.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Finset.affineCombination_linear (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (p : ι → P) : (Finset.affineCombination k s p).linear = Finset.weightedVSub s p

The linear map corresponding to affineCombination is weightedVSub.

theorem Finset.affineCombination_apply {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) : (Finset.affineCombination k s p) w = (Finset.weightedVSubOfPoint s p (Classical.choice (_ : Nonempty P))) w +ᵥ Classical.choice (_ : Nonempty P)

Applying affineCombination with given weights. This is for the case where a result involving a default base point is OK (for example, when that base point will cancel out later); a more typical use case for affineCombination would involve selecting a preferred base point with affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one and then using weightedVSubOfPoint_apply.

@[simp]

theorem Finset.affineCombination_apply_const {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : P) (h : (Finset.sum s fun (i : ι) => w i) = 1) : (Finset.affineCombination k s fun (x : ι) => p) w = p

The value of affineCombination, where the given points are equal.

theorem Finset.affineCombination_congr {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) {w₁ : ι → k} {w₂ : ι → k} (hw : ∀ i ∈ s, w₁ i = w₂ i) {p₁ : ι → P} {p₂ : ι → P} (hp : ∀ i ∈ s, p₁ i = p₂ i) : (Finset.affineCombination k s p₁) w₁ = (Finset.affineCombination k s p₂) w₂

affineCombination gives equal results for two families of weights and two families of points that are equal on s.

theorem Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) (h : (Finset.sum s fun (i : ι) => w i) = 1) (b : P) : (Finset.affineCombination k s p) w = (Finset.weightedVSubOfPoint s p b) w +ᵥ b

affineCombination gives the sum with any base point, when the sum of the weights is 1.

theorem Finset.weightedVSub_vadd_affineCombination {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w₁ : ι → k) (w₂ : ι → k) (p : ι → P) : (Finset.weightedVSub s p) w₁ +ᵥ (Finset.affineCombination k s p) w₂ = (Finset.affineCombination k s p) (w₁ + w₂)

Adding a weightedVSub to an affineCombination.

theorem Finset.affineCombination_vsub {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w₁ : ι → k) (w₂ : ι → k) (p : ι → P) : (Finset.affineCombination k s p) w₁ -ᵥ (Finset.affineCombination k s p) w₂ = (Finset.weightedVSub s p) (w₁ - w₂)

Subtracting two affineCombinations.

theorem Finset.attach_affineCombination_of_injective {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] [DecidableEq P] (s : Finset P) (w : P → k) (f : { x : P // x ∈ s } → P) (hf : Function.Injective f) : (Finset.affineCombination k (Finset.attach s) f) (w ∘ f) = (Finset.affineCombination k (Finset.image f Finset.univ) id) w

theorem Finset.attach_affineCombination_coe {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (s : Finset P) (w : P → k) : (Finset.affineCombination k (Finset.attach s) Subtype.val) (w ∘ Subtype.val) = (Finset.affineCombination k s id) w

@[simp]

theorem Finset.weightedVSub_eq_linear_combination {k : Type u_1} {V : Type u_2} [Ring k] [AddCommGroup V] [Module k V] {ι : Type u_6} (s : Finset ι) {w : ι → k} {p : ι → V} (hw : Finset.sum s w = 0) : (Finset.weightedVSub s p) w = Finset.sum s fun (i : ι) => w i • p i

Viewing a module as an affine space modelled on itself, a weightedVSub is just a linear combination.

@[simp]

theorem Finset.affineCombination_eq_linear_combination {k : Type u_1} {V : Type u_2} [Ring k] [AddCommGroup V] [Module k V] {ι : Type u_4} (s : Finset ι) (p : ι → V) (w : ι → k) (hw : (Finset.sum s fun (i : ι) => w i) = 1) : (Finset.affineCombination k s p) w = Finset.sum s fun (i : ι) => w i • p i

Viewing a module as an affine space modelled on itself, affine combinations are just linear combinations.

@[simp]

theorem Finset.affineCombination_of_eq_one_of_eq_zero {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) {i : ι} (his : i ∈ s) (hwi : w i = 1) (hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0) : (Finset.affineCombination k s p) w = p i

An affineCombination equals a point if that point is in the set and has weight 1 and the other points in the set have weight 0.

theorem Finset.affineCombination_indicator_subset {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (w : ι → k) (p : ι → P) {s₁ : Finset ι} {s₂ : Finset ι} (h : s₁ ⊆ s₂) : (Finset.affineCombination k s₁ p) w = (Finset.affineCombination k s₂ p) (Set.indicator (↑s₁) w)

An affine combination is unaffected by changing the weights to the corresponding indicator function and adding points to the set.

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

An affine combination, over the image of an embedding, equals an affine combination with the same points and weights over the original Finset.

theorem Finset.sum_smul_vsub_eq_affineCombination_vsub {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p₁ : ι → P) (p₂ : ι → P) : (Finset.sum s fun (i : ι) => w i • (p₁ i -ᵥ p₂ i)) = (Finset.affineCombination k s p₁) w -ᵥ (Finset.affineCombination k s p₂) w

A weighted sum of pairwise subtractions, expressed as a subtraction of two affineCombination expressions.

theorem Finset.sum_smul_vsub_const_eq_affineCombination_vsub {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p₁ : ι → P) (p₂ : P) (h : (Finset.sum s fun (i : ι) => w i) = 1) : (Finset.sum s fun (i : ι) => w i • (p₁ i -ᵥ p₂)) = (Finset.affineCombination k s p₁) w -ᵥ p₂

A weighted sum of pairwise subtractions, where the point on the right is constant and the sum of the weights is 1.

theorem Finset.sum_smul_const_vsub_eq_vsub_affineCombination {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p₂ : ι → P) (p₁ : P) (h : (Finset.sum s fun (i : ι) => w i) = 1) : (Finset.sum s fun (i : ι) => w i • (p₁ -ᵥ p₂ i)) = p₁ -ᵥ (Finset.affineCombination k s p₂) w

A weighted sum of pairwise subtractions, where the point on the left is constant and the sum of the weights is 1.

theorem Finset.affineCombination_sdiff_sub {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [DecidableEq ι] {s₂ : Finset ι} (h : s₂ ⊆ s) (w : ι → k) (p : ι → P) : (Finset.affineCombination k (s \ s₂) p) w -ᵥ (Finset.affineCombination k s₂ p) (-w) = (Finset.weightedVSub s p) w

A weighted sum may be split into a subtraction of affine combinations over two subsets.

theorem Finset.affineCombination_eq_of_weightedVSub_eq_zero_of_eq_neg_one {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) {w : ι → k} {p : ι → P} (hw : (Finset.weightedVSub s p) w = 0) {i : ι} [DecidablePred fun (x : ι) => x ≠ i] (his : i ∈ s) (hwi : w i = -1) : (Finset.affineCombination k (Finset.filter (fun (x : ι) => x ≠ i) s) p) w = p i

If a weighted sum is zero and one of the weights is -1, the corresponding point is the affine combination of the other points with the given weights.

theorem Finset.affineCombination_subtype_eq_filter {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) (pred : ι → Prop) [DecidablePred pred] : ((Finset.affineCombination k (Finset.subtype pred s) fun (i : Subtype pred) => p ↑i) fun (i : Subtype pred) => w ↑i) = (Finset.affineCombination k (Finset.filter pred s) p) w

An affine combination over s.subtype pred equals one over s.filter pred.

theorem Finset.affineCombination_filter_of_ne {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) {pred : ι → Prop} [DecidablePred pred] (h : ∀ i ∈ s, w i ≠ 0 → pred i) : (Finset.affineCombination k (Finset.filter pred s) p) w = (Finset.affineCombination k s p) w

An affine combination over s.filter pred equals one over s if all the weights at indices in s not satisfying pred are zero.

theorem Finset.eq_weightedVSubOfPoint_subset_iff_eq_weightedVSubOfPoint_subtype {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} {v : V} {x : k} {s : Set ι} {p : ι → P} {b : P} : (∃ (fs : Finset ι), ↑fs ⊆ s ∧ ∃ (w : ι → k), (Finset.sum fs fun (i : ι) => w i) = x ∧ v = (Finset.weightedVSubOfPoint fs p b) w) ↔ ∃ (fs : Finset ↑s) (w : ↑s → k), (Finset.sum fs fun (i : ↑s) => w i) = x ∧ v = (Finset.weightedVSubOfPoint fs (fun (i : ↑s) => p ↑i) b) w

Suppose an indexed family of points is given, along with a subset of the index type. A vector can be expressed as weightedVSubOfPoint using a Finset lying within that subset and with a given sum of weights if and only if it can be expressed as weightedVSubOfPoint with that sum of weights for the corresponding indexed family whose index type is the subtype corresponding to that subset.

theorem Finset.eq_weightedVSub_subset_iff_eq_weightedVSub_subtype (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} {v : V} {s : Set ι} {p : ι → P} : (∃ (fs : Finset ι), ↑fs ⊆ s ∧ ∃ (w : ι → k), (Finset.sum fs fun (i : ι) => w i) = 0 ∧ v = (Finset.weightedVSub fs p) w) ↔ ∃ (fs : Finset ↑s) (w : ↑s → k), (Finset.sum fs fun (i : ↑s) => w i) = 0 ∧ v = (Finset.weightedVSub fs fun (i : ↑s) => p ↑i) w

Suppose an indexed family of points is given, along with a subset of the index type. A vector can be expressed as weightedVSub using a Finset lying within that subset and with sum of weights 0 if and only if it can be expressed as weightedVSub with sum of weights 0 for the corresponding indexed family whose index type is the subtype corresponding to that subset.

theorem Finset.eq_affineCombination_subset_iff_eq_affineCombination_subtype (k : Type u_1) (V : Type u_2) {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} {p0 : P} {s : Set ι} {p : ι → P} : (∃ (fs : Finset ι), ↑fs ⊆ s ∧ ∃ (w : ι → k), (Finset.sum fs fun (i : ι) => w i) = 1 ∧ p0 = (Finset.affineCombination k fs p) w) ↔ ∃ (fs : Finset ↑s) (w : ↑s → k), (Finset.sum fs fun (i : ↑s) => w i) = 1 ∧ p0 = (Finset.affineCombination k fs fun (i : ↑s) => p ↑i) w

Suppose an indexed family of points is given, along with a subset of the index type. A point can be expressed as an affineCombination using a Finset lying within that subset and with sum of weights 1 if and only if it can be expressed an affineCombination with sum of weights 1 for the corresponding indexed family whose index type is the subtype corresponding to that subset.

theorem Finset.map_affineCombination {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) {V₂ : Type u_6} {P₂ : Type u_7} [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (p : ι → P) (w : ι → k) (hw : Finset.sum s w = 1) (f : P →ᵃ[k] P₂) : f ((Finset.affineCombination k s p) w) = (Finset.affineCombination k s (⇑f ∘ p)) w

Affine maps commute with affine combinations.

def Finset.affineCombinationSingleWeights (k : Type u_1) [Ring k] {ι : Type u_4} [DecidableEq ι] (i : ι) : ι → k

Weights for expressing a single point as an affine combination.

Equations

• Finset.affineCombinationSingleWeights k i = Function.update (Function.const ι 0) i 1

@[simp]

theorem Finset.affineCombinationSingleWeights_apply_self (k : Type u_1) [Ring k] {ι : Type u_4} [DecidableEq ι] (i : ι) : Finset.affineCombinationSingleWeights k i i = 1

@[simp]

theorem Finset.affineCombinationSingleWeights_apply_of_ne (k : Type u_1) [Ring k] {ι : Type u_4} [DecidableEq ι] {i : ι} {j : ι} (h : j ≠ i) : Finset.affineCombinationSingleWeights k i j = 0

@[simp]

theorem Finset.sum_affineCombinationSingleWeights (k : Type u_1) [Ring k] {ι : Type u_4} (s : Finset ι) [DecidableEq ι] {i : ι} (h : i ∈ s) : (Finset.sum s fun (j : ι) => Finset.affineCombinationSingleWeights k i j) = 1

def Finset.weightedVSubVSubWeights (k : Type u_1) [Ring k] {ι : Type u_4} [DecidableEq ι] (i : ι) (j : ι) : ι → k

Weights for expressing the subtraction of two points as a weightedVSub.

Equations

• Finset.weightedVSubVSubWeights k i j = Finset.affineCombinationSingleWeights k i - Finset.affineCombinationSingleWeights k j

@[simp]

theorem Finset.weightedVSubVSubWeights_self (k : Type u_1) [Ring k] {ι : Type u_4} [DecidableEq ι] (i : ι) : Finset.weightedVSubVSubWeights k i i = 0

@[simp]

theorem Finset.weightedVSubVSubWeights_apply_left (k : Type u_1) [Ring k] {ι : Type u_4} [DecidableEq ι] {i : ι} {j : ι} (h : i ≠ j) : Finset.weightedVSubVSubWeights k i j i = 1

@[simp]

theorem Finset.weightedVSubVSubWeights_apply_right (k : Type u_1) [Ring k] {ι : Type u_4} [DecidableEq ι] {i : ι} {j : ι} (h : i ≠ j) : Finset.weightedVSubVSubWeights k i j j = -1

@[simp]

theorem Finset.weightedVSubVSubWeights_apply_of_ne (k : Type u_1) [Ring k] {ι : Type u_4} [DecidableEq ι] {i : ι} {j : ι} {t : ι} (hi : t ≠ i) (hj : t ≠ j) : Finset.weightedVSubVSubWeights k i j t = 0

@[simp]

theorem Finset.sum_weightedVSubVSubWeights (k : Type u_1) [Ring k] {ι : Type u_4} (s : Finset ι) [DecidableEq ι] {i : ι} {j : ι} (hi : i ∈ s) (hj : j ∈ s) : (Finset.sum s fun (t : ι) => Finset.weightedVSubVSubWeights k i j t) = 0

def Finset.affineCombinationLineMapWeights {k : Type u_1} [Ring k] {ι : Type u_4} [DecidableEq ι] (i : ι) (j : ι) (c : k) : ι → k

Weights for expressing lineMap as an affine combination.

Equations

• Finset.affineCombinationLineMapWeights i j c = c • Finset.weightedVSubVSubWeights k j i + Finset.affineCombinationSingleWeights k i

@[simp]

theorem Finset.affineCombinationLineMapWeights_self {k : Type u_1} [Ring k] {ι : Type u_4} [DecidableEq ι] (i : ι) (c : k) : Finset.affineCombinationLineMapWeights i i c = Finset.affineCombinationSingleWeights k i

@[simp]

theorem Finset.affineCombinationLineMapWeights_apply_left {k : Type u_1} [Ring k] {ι : Type u_4} [DecidableEq ι] {i : ι} {j : ι} (h : i ≠ j) (c : k) : Finset.affineCombinationLineMapWeights i j c i = 1 - c

@[simp]

theorem Finset.affineCombinationLineMapWeights_apply_right {k : Type u_1} [Ring k] {ι : Type u_4} [DecidableEq ι] {i : ι} {j : ι} (h : i ≠ j) (c : k) : Finset.affineCombinationLineMapWeights i j c j = c

@[simp]

theorem Finset.affineCombinationLineMapWeights_apply_of_ne {k : Type u_1} [Ring k] {ι : Type u_4} [DecidableEq ι] {i : ι} {j : ι} {t : ι} (hi : t ≠ i) (hj : t ≠ j) (c : k) : Finset.affineCombinationLineMapWeights i j c t = 0

@[simp]

theorem Finset.sum_affineCombinationLineMapWeights {k : Type u_1} [Ring k] {ι : Type u_4} (s : Finset ι) [DecidableEq ι] {i : ι} {j : ι} (hi : i ∈ s) (hj : j ∈ s) (c : k) : (Finset.sum s fun (t : ι) => Finset.affineCombinationLineMapWeights i j c t) = 1

@[simp]

theorem Finset.affineCombination_affineCombinationSingleWeights (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [DecidableEq ι] (p : ι → P) {i : ι} (hi : i ∈ s) : (Finset.affineCombination k s p) (Finset.affineCombinationSingleWeights k i) = p i

An affine combination with affineCombinationSingleWeights gives the specified point.

@[simp]

theorem Finset.weightedVSub_weightedVSubVSubWeights (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [DecidableEq ι] (p : ι → P) {i : ι} {j : ι} (hi : i ∈ s) (hj : j ∈ s) : (Finset.weightedVSub s p) (Finset.weightedVSubVSubWeights k i j) = p i -ᵥ p j

A weighted subtraction with weightedVSubVSubWeights gives the result of subtracting the specified points.

@[simp]

theorem Finset.affineCombination_affineCombinationLineMapWeights {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [DecidableEq ι] (p : ι → P) {i : ι} {j : ι} (hi : i ∈ s) (hj : j ∈ s) (c : k) : (Finset.affineCombination k s p) (Finset.affineCombinationLineMapWeights i j c) = (AffineMap.lineMap (p i) (p j)) c

An affine combination with affineCombinationLineMapWeights gives the result of line_map.

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 : ι) : Finset.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 ι) : 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) : (Finset.sum s fun (i : ι) => Finset.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) : (Finset.sum s fun (i : ι) => Finset.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) : (Finset.sum s fun (i : ι) => Finset.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) : (Finset.sum s fun (i : ι) => Finset.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) : Finset.centroid k s p = (Finset.affineCombination k s p) (Finset.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) : Finset.centroid k Finset.univ Subtype.val = Finset.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 : ι) : Finset.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₂ : ι) : Finset.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) : Finset.centroid k Finset.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) : Finset.centroid k (Finset.map e s₂) p = Finset.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 = Set.indicator (↑s) (Finset.centroidWeights k s)

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

The definition of centroidWeightsIndicator.

theorem Finset.sum_centroidWeightsIndicator (k : Type u_1) [DivisionRing k] {ι : Type u_4} (s : Finset ι) [Fintype ι] : (Finset.sum Finset.univ fun (i : ι) => Finset.centroidWeightsIndicator k s i) = Finset.sum s fun (i : ι) => Finset.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) : (Finset.sum Finset.univ fun (i : ι) => Finset.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) : (Finset.sum Finset.univ fun (i : ι) => Finset.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) : (Finset.sum Finset.univ fun (i : ι) => Finset.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) : Finset.centroid k s p = (Finset.affineCombination k Finset.univ p) (Finset.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) : Finset.centroid k s p = Finset.centroid k Finset.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₂) : Finset.centroid k s p = Finset.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 weightedVSub_mem_vectorSpan {ι : Type u_1} {k : Type u_2} {V : Type u_3} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Finset ι} {w : ι → k} (h : (Finset.sum s fun (i : ι) => w i) = 0) (p : ι → P) : (Finset.weightedVSub s p) w ∈ vectorSpan k (Set.range p)

A weightedVSub with sum of weights 0 is in the vectorSpan of an indexed family.

theorem affineCombination_mem_affineSpan {ι : Type u_1} {k : Type u_2} {V : Type u_3} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Nontrivial k] {s : Finset ι} {w : ι → k} (h : (Finset.sum s fun (i : ι) => w i) = 1) (p : ι → P) : (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)

An affineCombination with sum of weights 1 is in the affineSpan of an indexed family, if the underlying ring is nontrivial.

theorem mem_vectorSpan_iff_eq_weightedVSub {ι : Type u_1} (k : Type u_2) {V : Type u_3} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {v : V} {p : ι → P} : v ∈ vectorSpan k (Set.range p) ↔ ∃ (s : Finset ι) (w : ι → k), (Finset.sum s fun (i : ι) => w i) = 0 ∧ v = (Finset.weightedVSub s p) w

A vector is in the vectorSpan of an indexed family if and only if it is a weightedVSub with sum of weights 0.

theorem eq_affineCombination_of_mem_affineSpan {ι : Type u_1} {k : Type u_2} {V : Type u_3} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p1 : P} {p : ι → P} (h : p1 ∈ affineSpan k (Set.range p)) : ∃ (s : Finset ι) (w : ι → k), (Finset.sum s fun (i : ι) => w i) = 1 ∧ p1 = (Finset.affineCombination k s p) w

A point in the affineSpan of an indexed family is an affineCombination with sum of weights 1. See also eq_affineCombination_of_mem_affineSpan_of_fintype.

theorem eq_affineCombination_of_mem_affineSpan_of_fintype {ι : Type u_1} {k : Type u_2} {V : Type u_3} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Fintype ι] {p1 : P} {p : ι → P} (h : p1 ∈ affineSpan k (Set.range p)) : ∃ (w : ι → k), (Finset.sum Finset.univ fun (i : ι) => w i) = 1 ∧ p1 = (Finset.affineCombination k Finset.univ p) w

theorem mem_affineSpan_iff_eq_affineCombination {ι : Type u_1} (k : Type u_2) (V : Type u_3) {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Nontrivial k] {p1 : P} {p : ι → P} : p1 ∈ affineSpan k (Set.range p) ↔ ∃ (s : Finset ι) (w : ι → k), (Finset.sum s fun (i : ι) => w i) = 1 ∧ p1 = (Finset.affineCombination k s p) w

A point is in the affineSpan of an indexed family if and only if it is an affineCombination with sum of weights 1, provided the underlying ring is nontrivial.

theorem mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd {ι : Type u_1} (k : Type u_2) (V : Type u_3) {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Nontrivial k] (p : ι → P) (j : ι) (q : P) : q ∈ affineSpan k (Set.range p) ↔ ∃ (s : Finset ι) (w : ι → k), q = (Finset.weightedVSubOfPoint s p (p j)) w +ᵥ p j

Given a family of points together with a chosen base point in that family, membership of the affine span of this family corresponds to an identity in terms of weightedVSubOfPoint, with weights that are not required to sum to 1.

theorem affineSpan_eq_affineSpan_lineMap_units {k : Type u_2} {V : Type u_3} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Nontrivial k] {s : Set P} {p : P} (hp : p ∈ s) (w : ↑s → kˣ) : affineSpan k (Set.range fun (q : ↑s) => (AffineMap.lineMap p ↑q) ↑(w q)) = affineSpan k s

Given a set of points, together with a chosen base point in this set, if we affinely transport all other members of the set along the line joining them to this base point, the affine span is unchanged.

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.

def AffineMap.weightedVSubOfPoint {k : Type u_1} {V : Type u_2} (P : Type u_3) [CommRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) : (ι → P) × P →ᵃ[k] V

A weighted sum, as an affine map on the points involved.

Equations

• One or more equations did not get rendered due to their size.