Mathlib.LinearAlgebra.AffineSpace.Combination

Finset.univ_fin2 theorem

: (univ : Finset (Fin 2)) = {0, 1}

Full source

theorem univ_fin2 : (univ : Finset (Fin 2)) = {0, 1} := by
  ext x
  fin_cases x <;> simp

Universal Finite Set of $\mathrm{Fin}(2)$ is $\{0,1\}$

Informal description

The universal finite set of the type $\mathrm{Fin}(2)$ (the finite ordinals less than 2) is equal to the set $\{0, 1\}$.

Finset.weightedVSubOfPoint definition

(p : ι → P) (b : P) : (ι → k) →ₗ[k] V

Full source

/-- 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. -/
def weightedVSubOfPoint (p : ι → P) (b : P) : (ι → k) →ₗ[k] V :=
  ∑ i ∈ s, (LinearMap.proj i : (ι → k) →ₗ[k] k).smulRight (p i -ᵥ b)

Weighted vector subtraction from a base point

Informal description

For a finite set $s$ of indices $\iota$, a family of points $p : \iota \to P$ in an affine space, and a base point $b \in P$, the function $\text{weightedVSubOfPoint}$ is a linear map from the space of weight functions $\iota \to k$ to the vector space $V$ associated with the affine space. It computes the weighted sum $\sum_{i \in s} w_i \cdot (p_i - b)$, where $p_i - b$ denotes the vector from $b$ to $p_i$. This construction is particularly useful when the sum of weights is 0, making the result independent of the choice of base point, or when the sum of weights is 1, making the result (when added to the base point) independent of the choice of base point.

Finset.weightedVSubOfPoint_apply theorem

(w : ι → k) (p : ι → P) (b : P) : s.weightedVSubOfPoint p b w = ∑ i ∈ s, w i • (p i -ᵥ b)

Full source

@[simp]
theorem weightedVSubOfPoint_apply (w : ι → k) (p : ι → P) (b : P) :
    s.weightedVSubOfPoint p b w = ∑ i ∈ s, w i • (p i -ᵥ b) := by
  simp [weightedVSubOfPoint, LinearMap.sum_apply]

Weighted Vector Subtraction Formula from Base Point

Informal description

For a finite set $s$ of indices $\iota$, a family of points $p : \iota \to P$ in an affine space with associated vector space $V$ over a field $k$, a base point $b \in P$, and weights $w : \iota \to k$, the weighted vector subtraction from $b$ is given by: \[ \text{weightedVSubOfPoint}_s(p, b, w) = \sum_{i \in s} w_i \cdot (p_i - b) \] where $p_i - b$ denotes the vector from $b$ to $p_i$ and $\cdot$ denotes the scalar multiplication in $V$.

Finset.weightedVSubOfPoint_apply_const theorem

(w : ι → k) (p : P) (b : P) : s.weightedVSubOfPoint (fun _ => p) b w = (∑ i ∈ s, w i) • (p -ᵥ b)

Full source

/-- The value of `weightedVSubOfPoint`, where the given points are equal. -/
@[simp (high)]
theorem weightedVSubOfPoint_apply_const (w : ι → k) (p : P) (b : P) :
    s.weightedVSubOfPoint (fun _ => p) b w = (∑ i ∈ s, w i) • (p -ᵥ b) := by
  rw [weightedVSubOfPoint_apply, sum_smul]

Weighted Vector Subtraction Formula for Constant Points

Informal description

For a finite set $s$ of indices $\iota$, a constant point $p$ in an affine space, a base point $b$, and weights $w : \iota \to k$, the weighted vector subtraction from $b$ is given by: \[ \text{weightedVSubOfPoint}_s(\lambda \_, p, b, w) = \left(\sum_{i \in s} w_i\right) \cdot (p - b) \] where $p - b$ denotes the vector from $b$ to $p$ and $\cdot$ denotes scalar multiplication in the associated vector space $V$.

Finset.weightedVSubOfPoint_vadd theorem

 (s : Finset ι) (w : ι → k) (p : ι → P) (b : P) (v : V) :
  s.weightedVSubOfPoint (v +ᵥ p) b w = s.weightedVSubOfPoint p (-v +ᵥ b) w

Full source

lemma weightedVSubOfPoint_vadd (s : Finset ι) (w : ι → k) (p : ι → P) (b : P) (v : V) :
    s.weightedVSubOfPoint (v +ᵥ p) b w = s.weightedVSubOfPoint p (-v +ᵥ b) w := by
  simp [vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, add_comm]

Invariance of Weighted Vector Subtraction under Translation

Informal description

For a finite set $s$ of indices $\iota$, weights $w : \iota \to k$, a family of points $p : \iota \to P$ in an affine space with associated vector space $V$, a base point $b \in P$, and a vector $v \in V$, the weighted vector subtraction from $b$ satisfies: \[ \text{weightedVSubOfPoint}_s(v + p, b, w) = \text{weightedVSubOfPoint}_s(p, -v + b, w) \] where $v + p$ denotes the translation of each point $p_i$ by $v$, and $-v + b$ denotes the translation of $b$ by $-v$.

Finset.weightedVSubOfPoint_smul theorem

 {G : Type*} [Group G] [DistribMulAction G V] [SMulCommClass G k V] (s : Finset ι) (w : ι → k) (p : ι → V) (b : V)
  (a : G) : s.weightedVSubOfPoint (a • p) b w = a • s.weightedVSubOfPoint p (a⁻¹ • b) w

Full source

lemma weightedVSubOfPoint_smul {G : Type*} [Group G] [DistribMulAction G V] [SMulCommClass G k V]
    (s : Finset ι) (w : ι → k) (p : ι → V) (b : V) (a : G) :
    s.weightedVSubOfPoint (a • p) b w = a • s.weightedVSubOfPoint p (a⁻¹ • b) w := by
  simp [smul_sum, smul_sub, smul_comm a (w _)]

Equivariance of Weighted Vector Subtraction under Group Action

Informal description

Let $G$ be a group acting distributively on a vector space $V$ over a field $k$, with the actions of $G$ and $k$ on $V$ commuting. For any finite set $s$ of indices $\iota$, any weights $w : \iota \to k$, any points $p : \iota \to V$, any base point $b \in V$, and any element $a \in G$, we have: \[ \text{weightedVSubOfPoint}_s(a \cdot p, b, w) = a \cdot \text{weightedVSubOfPoint}_s(p, a^{-1} \cdot b, w) \] where $\cdot$ denotes the action of $G$ on $V$ and $\text{weightedVSubOfPoint}_s$ is the weighted vector subtraction from the base point.

Finset.weightedVSubOfPoint_congr theorem

 {w₁ w₂ : ι → k} (hw : ∀ i ∈ s, w₁ i = w₂ i) {p₁ p₂ : ι → P} (hp : ∀ i ∈ s, p₁ i = p₂ i) (b : P) :
  s.weightedVSubOfPoint p₁ b w₁ = s.weightedVSubOfPoint p₂ b w₂

Full source

/-- `weightedVSubOfPoint` gives equal results for two families of weights and two families of
points that are equal on `s`. -/
theorem weightedVSubOfPoint_congr {w₁ w₂ : ι → k} (hw : ∀ i ∈ s, w₁ i = w₂ i) {p₁ p₂ : ι → P}
    (hp : ∀ i ∈ s, p₁ i = p₂ i) (b : P) :
    s.weightedVSubOfPoint p₁ b w₁ = s.weightedVSubOfPoint p₂ b w₂ := by
  simp_rw [weightedVSubOfPoint_apply]
  refine sum_congr rfl fun i hi => ?_
  rw [hw i hi, hp i hi]

Weighted Vector Subtraction is Uniquely Determined by Weights and Points on a Finite Set

Informal description

For a finite set $s$ of indices $\iota$, two families of weights $w_1, w_2 : \iota \to k$ that agree on $s$ (i.e., $w_1(i) = w_2(i)$ for all $i \in s$), and two families of points $p_1, p_2 : \iota \to P$ in an affine space that agree on $s$ (i.e., $p_1(i) = p_2(i)$ for all $i \in s$), the weighted vector subtraction from any base point $b \in P$ yields the same result: \[ \text{weightedVSubOfPoint}_s(p_1, b, w_1) = \text{weightedVSubOfPoint}_s(p_2, b, w_2). \]

Finset.weightedVSubOfPoint_eq_of_weights_eq theorem

 (p : ι → P) (j : ι) (w₁ w₂ : ι → k) (hw : ∀ i, i ≠ j → w₁ i = w₂ i) :
  s.weightedVSubOfPoint p (p j) w₁ = s.weightedVSubOfPoint p (p j) w₂

Full source

/-- 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 weightedVSubOfPoint_eq_of_weights_eq (p : ι → P) (j : ι) (w₁ w₂ : ι → k)
    (hw : ∀ i, i ≠ j → w₁ i = w₂ i) :
    s.weightedVSubOfPoint p (p j) w₁ = s.weightedVSubOfPoint p (p j) w₂ := by
  simp only [Finset.weightedVSubOfPoint_apply]
  congr
  ext i
  rcases eq_or_ne i j with h | h
  · simp [h]
  · simp [hw i h]

Weighted Vector Subtraction is Independent of Weight at Base Point

Informal description

Let $s$ be a finite set of indices, $p : \iota \to P$ a family of points in an affine space, and $j \in \iota$. For any two weight functions $w_1, w_2 : \iota \to k$ that agree on all indices except possibly at $j$, the weighted vector subtraction from the base point $p_j$ satisfies: \[ \sum_{i \in s} w_1(i) \cdot (p_i - p_j) = \sum_{i \in s} w_2(i) \cdot (p_i - p_j) \] where $\cdot$ denotes scalar multiplication and $-$ denotes vector subtraction in the associated vector space of the affine space.

Finset.weightedVSubOfPoint_eq_of_sum_eq_zero theorem

 (w : ι → k) (p : ι → P) (h : ∑ i ∈ s, w i = 0) (b₁ b₂ : P) :
  s.weightedVSubOfPoint p b₁ w = s.weightedVSubOfPoint p b₂ w

Full source

/-- The weighted sum is independent of the base point when the sum of
the weights is 0. -/
theorem weightedVSubOfPoint_eq_of_sum_eq_zero (w : ι → k) (p : ι → P) (h : ∑ i ∈ s, w i = 0)
    (b₁ b₂ : P) : s.weightedVSubOfPoint p b₁ w = s.weightedVSubOfPoint p b₂ w := by
  apply eq_of_sub_eq_zero
  rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, ← sum_sub_distrib]
  conv_lhs =>
    congr
    · skip
    · ext
      rw [← smul_sub, vsub_sub_vsub_cancel_left]
  rw [← sum_smul, h, zero_smul]

Invariance of Weighted Vector Subtraction under Base Point Change when Weights Sum to Zero

Informal description

For a finite set $s$ of indices $\iota$, a family of points $p : \iota \to P$ in an affine space with associated vector space $V$ over a field $k$, and weights $w : \iota \to k$ such that $\sum_{i \in s} w_i = 0$, the weighted vector subtraction $\sum_{i \in s} w_i \cdot (p_i - b)$ is independent of the choice of base point $b \in P$. That is, for any two base points $b_1, b_2 \in P$, we have: \[ \sum_{i \in s} w_i \cdot (p_i - b_1) = \sum_{i \in s} w_i \cdot (p_i - b_2) \]

Finset.weightedVSubOfPoint_vadd_eq_of_sum_eq_one theorem

 (w : ι → k) (p : ι → P) (h : ∑ i ∈ s, w i = 1) (b₁ b₂ : P) :
  s.weightedVSubOfPoint p b₁ w +ᵥ b₁ = s.weightedVSubOfPoint p b₂ w +ᵥ b₂

Full source

/-- The weighted sum, added to the base point, is independent of the
base point when the sum of the weights is 1. -/
theorem weightedVSubOfPoint_vadd_eq_of_sum_eq_one (w : ι → k) (p : ι → P) (h : ∑ i ∈ s, w i = 1)
    (b₁ b₂ : P) : s.weightedVSubOfPoint p b₁ w +ᵥ b₁ = s.weightedVSubOfPoint p b₂ w +ᵥ b₂ := by
  rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, ← @vsub_eq_zero_iff_eq V,
    vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, ← add_sub_assoc, add_comm, add_sub_assoc, ←
    sum_sub_distrib]
  conv_lhs =>
    congr
    · skip
    · congr
      · skip
      · ext
        rw [← smul_sub, vsub_sub_vsub_cancel_left]
  rw [← sum_smul, h, one_smul, vsub_add_vsub_cancel, vsub_self]

Base Point Independence of Affine Combination with Unit Weight Sum

Informal description

For a finite set $s$ of indices $\iota$, a family of points $p : \iota \to P$ in an affine space with associated vector space $V$ over a field $k$, and weights $w : \iota \to k$ such that $\sum_{i \in s} w_i = 1$, the affine combination of points is independent of the base point. That is, for any two base points $b_1, b_2 \in P$, we have: \[ \sum_{i \in s} w_i (p_i - b_1) + b_1 = \sum_{i \in s} w_i (p_i - b_2) + b_2 \]

Finset.weightedVSubOfPoint_erase theorem

 [DecidableEq ι] (w : ι → k) (p : ι → P) (i : ι) :
  (s.erase i).weightedVSubOfPoint p (p i) w = s.weightedVSubOfPoint p (p i) w

Full source

/-- The weighted sum is unaffected by removing the base point, if
present, from the set of points. -/
@[simp (high)]
theorem weightedVSubOfPoint_erase [DecidableEq ι] (w : ι → k) (p : ι → P) (i : ι) :
    (s.erase i).weightedVSubOfPoint p (p i) w = s.weightedVSubOfPoint p (p i) w := by
  rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply]
  apply sum_erase
  rw [vsub_self, smul_zero]

Weighted Vector Subtraction Unaffected by Removing Base Point

Informal description

Let $s$ be a finite set of indices $\iota$, $w : \iota \to k$ a weight function, $p : \iota \to P$ a family of points in an affine space, and $i \in \iota$. Then the weighted vector subtraction from the base point $p_i$ over the set $s \setminus \{i\}$ is equal to the weighted vector subtraction from $p_i$ over the entire set $s$. That is, \[ \sum_{j \in s \setminus \{i\}} w_j \cdot (p_j - p_i) = \sum_{j \in s} w_j \cdot (p_j - p_i). \]

Finset.weightedVSubOfPoint_insert theorem

 [DecidableEq ι] (w : ι → k) (p : ι → P) (i : ι) :
  (insert i s).weightedVSubOfPoint p (p i) w = s.weightedVSubOfPoint p (p i) w

Full source

/-- The weighted sum is unaffected by adding the base point, whether
or not present, to the set of points. -/
@[simp (high)]
theorem weightedVSubOfPoint_insert [DecidableEq ι] (w : ι → k) (p : ι → P) (i : ι) :
    (insert i s).weightedVSubOfPoint p (p i) w = s.weightedVSubOfPoint p (p i) w := by
  rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply]
  apply sum_insert_zero
  rw [vsub_self, smul_zero]

Weighted Vector Subtraction Unaffected by Inserting Base Point

Informal description

Let $s$ be a finite set of indices $\iota$, $p : \iota \to P$ a family of points in an affine space with associated vector space $V$ over a field $k$, $w : \iota \to k$ a weight function, and $i \in \iota$ an index. Then the weighted vector subtraction from the base point $p_i$ satisfies: \[ (\text{insert } i \text{ } s).\text{weightedVSubOfPoint } p \text{ } (p_i) \text{ } w = s.\text{weightedVSubOfPoint } p \text{ } (p_i) \text{ } w \] where $\text{weightedVSubOfPoint}$ computes the weighted sum $\sum_{j \in s} w_j \cdot (p_j - p_i)$.

Finset.weightedVSubOfPoint_indicator_subset theorem

 (w : ι → k) (p : ι → P) (b : P) {s₁ s₂ : Finset ι} (h : s₁ ⊆ s₂) :
  s₁.weightedVSubOfPoint p b w = s₂.weightedVSubOfPoint p b (Set.indicator (↑s₁) w)

Full source

/-- The weighted sum is unaffected by changing the weights to the
corresponding indicator function and adding points to the set. -/
theorem weightedVSubOfPoint_indicator_subset (w : ι → k) (p : ι → P) (b : P) {s₁ s₂ : Finset ι}
    (h : s₁ ⊆ s₂) :
    s₁.weightedVSubOfPoint p b w = s₂.weightedVSubOfPoint p b (Set.indicator (↑s₁) w) := by
  rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply]
  exact Eq.symm <|
    sum_indicator_subset_of_eq_zero w (fun i wi => wi • (p i -ᵥ b : V)) h fun i => zero_smul k _

Weighted Vector Subtraction Unaffected by Indicator Weights and Superset

Informal description

For a finite set of indices $\iota$, a family of points $p \colon \iota \to P$ in an affine space with associated vector space $V$ over a field $k$, a base point $b \in P$, and weights $w \colon \iota \to k$, if $s_1 \subseteq s_2$ are two finite subsets of $\iota$, then the weighted vector subtraction from $b$ over $s_1$ is equal to the weighted vector subtraction from $b$ over $s_2$ using the indicator function of $s_1$ as weights. That is, \[ \sum_{i \in s_1} w_i \cdot (p_i - b) = \sum_{i \in s_2} (\mathbf{1}_{s_1}(i) \cdot w_i) \cdot (p_i - b), \] where $\mathbf{1}_{s_1}$ is the indicator function of $s_1$.

Finset.weightedVSubOfPoint_map theorem

 (e : ι₂ ↪ ι) (w : ι → k) (p : ι → P) (b : P) :
  (s₂.map e).weightedVSubOfPoint p b w = s₂.weightedVSubOfPoint (p ∘ e) b (w ∘ e)

Full source

/-- A weighted sum, over the image of an embedding, equals a weighted
sum with the same points and weights over the original
`Finset`. -/
theorem weightedVSubOfPoint_map (e : ι₂ ↪ ι) (w : ι → k) (p : ι → P) (b : P) :
    (s₂.map e).weightedVSubOfPoint p b w = s₂.weightedVSubOfPoint (p ∘ e) b (w ∘ e) := by
  simp_rw [weightedVSubOfPoint_apply]
  exact Finset.sum_map _ _ _

Weighted Vector Subtraction under Injective Mapping

Informal description

Let $e : \iota_2 \hookrightarrow \iota$ be an injective function, $w : \iota \to k$ a weight function, $p : \iota \to P$ a family of points in an affine space with associated vector space $V$ over a field $k$, and $b \in P$ a base point. For any finite set $s_2 \subseteq \iota_2$, the weighted vector subtraction from $b$ over the image of $s_2$ under $e$ is equal to the weighted vector subtraction from $b$ over $s_2$ with points and weights composed with $e$. That is, \[ \sum_{i \in e(s_2)} w_i \cdot (p_i - b) = \sum_{j \in s_2} w_{e(j)} \cdot (p_{e(j)} - b) \] where $\cdot$ denotes scalar multiplication in $V$ and $-$ denotes vector subtraction in the affine space.

Finset.sum_smul_vsub_eq_weightedVSubOfPoint_sub theorem

 (w : ι → k) (p₁ p₂ : ι → P) (b : P) :
  (∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i)) = s.weightedVSubOfPoint p₁ b w - s.weightedVSubOfPoint p₂ b w

Full source

/-- A weighted sum of pairwise subtractions, expressed as a subtraction of two
`weightedVSubOfPoint` expressions. -/
theorem sum_smul_vsub_eq_weightedVSubOfPoint_sub (w : ι → k) (p₁ p₂ : ι → P) (b : P) :
    (∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i)) =
      s.weightedVSubOfPoint p₁ b w - s.weightedVSubOfPoint p₂ b w := by
  simp_rw [weightedVSubOfPoint_apply, ← sum_sub_distrib, ← smul_sub, vsub_sub_vsub_cancel_right]

Weighted Sum of Vector Subtractions as Difference of Weighted VSubs

Informal description

For a finite set $s$ of indices $\iota$, weights $w : \iota \to k$, and two families of points $p_1, p_2 : \iota \to P$ in an affine space with associated vector space $V$ over a field $k$, the weighted sum of vector subtractions can be expressed as the difference of two weighted vector subtractions from a base point $b \in P$: \[ \sum_{i \in s} w_i \cdot (p_1 i - p_2 i) = \text{weightedVSubOfPoint}_s(p_1, b, w) - \text{weightedVSubOfPoint}_s(p_2, b, w), \] where $p - q$ denotes the vector from $q$ to $p$ and $\cdot$ denotes scalar multiplication in $V$.

Finset.sum_smul_vsub_const_eq_weightedVSubOfPoint_sub theorem

 (w : ι → k) (p₁ : ι → P) (p₂ b : P) :
  (∑ i ∈ s, w i • (p₁ i -ᵥ p₂)) = s.weightedVSubOfPoint p₁ b w - (∑ i ∈ s, w i) • (p₂ -ᵥ b)

Full source

/-- A weighted sum of pairwise subtractions, where the point on the right is constant,
expressed as a subtraction involving a `weightedVSubOfPoint` expression. -/
theorem sum_smul_vsub_const_eq_weightedVSubOfPoint_sub (w : ι → k) (p₁ : ι → P) (p₂ b : P) :
    (∑ i ∈ s, w i • (p₁ i -ᵥ p₂)) = s.weightedVSubOfPoint p₁ b w - (∑ i ∈ s, w i) • (p₂ -ᵥ b) := by
  rw [sum_smul_vsub_eq_weightedVSubOfPoint_sub, weightedVSubOfPoint_apply_const]

Weighted Sum of Vector Subtractions from Constant Point as Difference of Weighted VSubs

Informal description

For a finite set $s$ of indices $\iota$, weights $w : \iota \to k$, a family of points $p_1 : \iota \to P$ in an affine space with associated vector space $V$ over a field $k$, and two points $p_2, b \in P$, the weighted sum of vector subtractions from $p_2$ can be expressed as: \[ \sum_{i \in s} w_i \cdot (p_1 i - p_2) = \text{weightedVSubOfPoint}_s(p_1, b, w) - \left(\sum_{i \in s} w_i\right) \cdot (p_2 - b), \] where $p - q$ denotes the vector from $q$ to $p$ and $\cdot$ denotes scalar multiplication in $V$.

Finset.sum_smul_const_vsub_eq_sub_weightedVSubOfPoint theorem

 (w : ι → k) (p₂ : ι → P) (p₁ b : P) :
  (∑ i ∈ s, w i • (p₁ -ᵥ p₂ i)) = (∑ i ∈ s, w i) • (p₁ -ᵥ b) - s.weightedVSubOfPoint p₂ b w

Full source

/-- A weighted sum of pairwise subtractions, where the point on the left is constant,
expressed as a subtraction involving a `weightedVSubOfPoint` expression. -/
theorem sum_smul_const_vsub_eq_sub_weightedVSubOfPoint (w : ι → k) (p₂ : ι → P) (p₁ b : P) :
    (∑ i ∈ s, w i • (p₁ -ᵥ p₂ i)) = (∑ i ∈ s, w i) • (p₁ -ᵥ b) - s.weightedVSubOfPoint p₂ b w := by
  rw [sum_smul_vsub_eq_weightedVSubOfPoint_sub, weightedVSubOfPoint_apply_const]

Weighted Sum of Constant-Point Vector Subtractions as Linear Combination

Informal description

For a finite set $s$ of indices $\iota$, weights $w : \iota \to k$, a family of points $p_2 : \iota \to P$ in an affine space with associated vector space $V$ over a field $k$, and two points $p_1, b \in P$, the weighted sum of vector subtractions from $p_1$ to each $p_2 i$ can be expressed as: \[ \sum_{i \in s} w_i \cdot (p_1 - p_2 i) = \left(\sum_{i \in s} w_i\right) \cdot (p_1 - b) - \text{weightedVSubOfPoint}_s(p_2, b, w), \] where $p - q$ denotes the vector from $q$ to $p$ and $\cdot$ denotes scalar multiplication in $V$.

Finset.weightedVSubOfPoint_sdiff theorem

 [DecidableEq ι] {s₂ : Finset ι} (h : s₂ ⊆ s) (w : ι → k) (p : ι → P) (b : P) :
  (s \ s₂).weightedVSubOfPoint p b w + s₂.weightedVSubOfPoint p b w = s.weightedVSubOfPoint p b w

Full source

/-- A weighted sum may be split into such sums over two subsets. -/
theorem weightedVSubOfPoint_sdiff [DecidableEq ι] {s₂ : Finset ι} (h : s₂ ⊆ s) (w : ι → k)
    (p : ι → P) (b : P) :
    (s \ s₂).weightedVSubOfPoint p b w + s₂.weightedVSubOfPoint p b w =
      s.weightedVSubOfPoint p b w := by
  simp_rw [weightedVSubOfPoint_apply, sum_sdiff h]

Splitting Property of Weighted Vector Subtraction in Affine Space

Informal description

Let $s$ be a finite set of indices $\iota$ with a decidable equality, and let $s_2 \subseteq s$ be a subset. For any family of points $p : \iota \to P$ in an affine space with associated vector space $V$ over a field $k$, a base point $b \in P$, and weights $w : \iota \to k$, the weighted vector subtraction from $b$ satisfies: \[ \text{weightedVSubOfPoint}_{s \setminus s_2}(p, b, w) + \text{weightedVSubOfPoint}_{s_2}(p, b, w) = \text{weightedVSubOfPoint}_s(p, b, w) \] where $\text{weightedVSubOfPoint}_s(p, b, w) = \sum_{i \in s} w_i \cdot (p_i - b)$ denotes the weighted sum of vector subtractions from the base point $b$.

Finset.weightedVSubOfPoint_sdiff_sub theorem

 [DecidableEq ι] {s₂ : Finset ι} (h : s₂ ⊆ s) (w : ι → k) (p : ι → P) (b : P) :
  (s \ s₂).weightedVSubOfPoint p b w - s₂.weightedVSubOfPoint p b (-w) = s.weightedVSubOfPoint p b w

Full source

/-- A weighted sum may be split into a subtraction of such sums over two subsets. -/
theorem weightedVSubOfPoint_sdiff_sub [DecidableEq ι] {s₂ : Finset ι} (h : s₂ ⊆ s) (w : ι → k)
    (p : ι → P) (b : P) :
    (s \ s₂).weightedVSubOfPoint p b w - s₂.weightedVSubOfPoint p b (-w) =
      s.weightedVSubOfPoint p b w := by
  rw [map_neg, sub_neg_eq_add, s.weightedVSubOfPoint_sdiff h]

Subtractive Splitting Property of Weighted Vector Subtraction in Affine Space

Informal description

Let $s$ be a finite set of indices $\iota$ with decidable equality, and let $s_2 \subseteq s$ be a subset. For any family of points $p : \iota \to P$ in an affine space with associated vector space $V$ over a field $k$, a base point $b \in P$, and weights $w : \iota \to k$, the following equality holds: \[ \sum_{i \in s \setminus s_2} w_i \cdot (p_i - b) - \sum_{i \in s_2} (-w_i) \cdot (p_i - b) = \sum_{i \in s} w_i \cdot (p_i - b), \] where $p_i - b$ denotes the vector from $b$ to $p_i$ and $\cdot$ denotes scalar multiplication in $V$.

Finset.weightedVSubOfPoint_subtype_eq_filter theorem

 (w : ι → k) (p : ι → P) (b : P) (pred : ι → Prop) [DecidablePred pred] :
  ((s.subtype pred).weightedVSubOfPoint (fun i => p i) b fun i => w i) = {x ∈ s | pred x}.weightedVSubOfPoint p b w

Full source

/-- A weighted sum over `s.subtype pred` equals one over `{x ∈ s | pred x}`. -/
theorem weightedVSubOfPoint_subtype_eq_filter (w : ι → k) (p : ι → P) (b : P) (pred : ι → Prop)
    [DecidablePred pred] :
    ((s.subtype pred).weightedVSubOfPoint (fun i => p i) b fun i => w i) =
      {x ∈ s | pred x}.weightedVSubOfPoint p b w := by
  rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, ← sum_subtype_eq_sum_filter]

Equality of Weighted Vector Subtraction over Subtype and Filtered Set

Informal description

For a finite set $s$ of indices $\iota$, a family of points $p : \iota \to P$ in an affine space with associated vector space $V$ over a field $k$, a base point $b \in P$, weights $w : \iota \to k$, and a predicate $\text{pred} : \iota \to \text{Prop}$, the weighted vector subtraction from $b$ over the subtype of $s$ satisfying $\text{pred}$ is equal to the weighted vector subtraction from $b$ over the filtered set $\{x \in s \mid \text{pred }x\}$. That is, \[ \sum_{i \in s, \text{pred }i} w_i \cdot (p_i - b) = \sum_{i \in \{x \in s \mid \text{pred }x\}} w_i \cdot (p_i - b), \] where $p_i - b$ denotes the vector from $b$ to $p_i$ and $\cdot$ denotes scalar multiplication in $V$.

Finset.weightedVSubOfPoint_filter_of_ne theorem

 (w : ι → k) (p : ι → P) (b : P) {pred : ι → Prop} [DecidablePred pred] (h : ∀ i ∈ s, w i ≠ 0 → pred i) :
  {x ∈ s | pred x}.weightedVSubOfPoint p b w = s.weightedVSubOfPoint p b w

Full source

/-- A weighted sum over `{x ∈ s | pred x}` equals one over `s` if all the weights at indices in `s`
not satisfying `pred` are zero. -/
theorem weightedVSubOfPoint_filter_of_ne (w : ι → k) (p : ι → P) (b : P) {pred : ι → Prop}
    [DecidablePred pred] (h : ∀ i ∈ s, w i ≠ 0 → pred i) :
    {x ∈ s | pred x}.weightedVSubOfPoint p b w = s.weightedVSubOfPoint p b w := by
  rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, sum_filter_of_ne]
  intro i hi hne
  refine h i hi ?_
  intro hw
  simp [hw] at hne

Weighted Vector Subtraction Equality Under Nonzero Weight Filtering

Informal description

Let $s$ be a finite set of indices, $w : \iota \to k$ a weight function, $p : \iota \to P$ a family of points in an affine space with associated vector space $V$ over field $k$, and $b \in P$ a base point. For any predicate $\text{pred} : \iota \to \text{Prop}$, if for all $i \in s$ with $w_i \neq 0$ we have $\text{pred}(i)$, then the weighted vector subtraction from $b$ over the filtered set $\{x \in s \mid \text{pred}(x)\}$ equals the weighted vector subtraction over the entire set $s$: \[ \sum_{i \in \{x \in s \mid \text{pred}(x)\}} w_i \cdot (p_i - b) = \sum_{i \in s} w_i \cdot (p_i - b). \]

Finset.weightedVSubOfPoint_const_smul theorem

(w : ι → k) (p : ι → P) (b : P) (c : k) : s.weightedVSubOfPoint p b (c • w) = c • s.weightedVSubOfPoint p b w

Full source

/-- A constant multiplier of the weights in `weightedVSubOfPoint` may be moved outside the
sum. -/
theorem weightedVSubOfPoint_const_smul (w : ι → k) (p : ι → P) (b : P) (c : k) :
    s.weightedVSubOfPoint p b (c • w) = c • s.weightedVSubOfPoint p b w := by
  simp_rw [weightedVSubOfPoint_apply, smul_sum, Pi.smul_apply, smul_smul, smul_eq_mul]

Scalar Multiplication Commutes with Weighted Vector Subtraction

Informal description

For a finite set $s$ of indices $\iota$, a family of points $p : \iota \to P$ in an affine space with associated vector space $V$ over a field $k$, a base point $b \in P$, weights $w : \iota \to k$, and a scalar $c \in k$, the weighted vector subtraction satisfies: \[ \text{weightedVSubOfPoint}_s(p, b, c \cdot w) = c \cdot \text{weightedVSubOfPoint}_s(p, b, w) \] where $c \cdot w$ denotes the pointwise scalar multiplication of the weight function $w$ by $c$, and $c \cdot \text{weightedVSubOfPoint}_s(p, b, w)$ denotes the scalar multiplication of the resulting vector by $c$.

Finset.weightedVSub definition

(p : ι → P) : (ι → k) →ₗ[k] V

Full source

/-- 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. -/
def weightedVSub (p : ι → P) : (ι → k) →ₗ[k] V :=
  s.weightedVSubOfPoint p (Classical.choice S.nonempty)

Weighted vector subtraction in affine space

Informal description

For a finite set $s$ of indices $\iota$ and a family of points $p : \iota \to P$ in an affine space, the function $\text{weightedVSub}$ is a linear map from the space of weight functions $\iota \to k$ to the vector space $V$ associated with the affine space. It computes the weighted sum $\sum_{i \in s} w_i \cdot (p_i - b)$, where $b$ is an arbitrary base point in $P$ (chosen using the axiom of choice) and $p_i - b$ denotes the vector from $b$ to $p_i$. This construction is particularly useful when the sum of weights is 0, making the result independent of the choice of base point.

Finset.weightedVSub_apply theorem

(w : ι → k) (p : ι → P) : s.weightedVSub p w = ∑ i ∈ s, w i • (p i -ᵥ Classical.choice S.nonempty)

Full source

/-- 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 weightedVSub_apply (w : ι → k) (p : ι → P) :
    s.weightedVSub p w = ∑ i ∈ s, w i • (p i -ᵥ Classical.choice S.nonempty) := by
  simp [weightedVSub, LinearMap.sum_apply]

Weighted Vector Subtraction Formula in Affine Space

Informal description

For a finite set $s$ of indices $\iota$, a family of points $p : \iota \to P$ in an affine space with associated vector space $V$ over a field $k$, and weights $w : \iota \to k$, the weighted vector subtraction is given by: \[ \text{weightedVSub}_s(p, w) = \sum_{i \in s} w_i \cdot (p_i - b) \] where $b$ is an arbitrarily chosen base point in $P$ (via the axiom of choice) and $p_i - b$ denotes the vector from $b$ to $p_i$.

Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero theorem

(w : ι → k) (p : ι → P) (h : ∑ i ∈ s, w i = 0) (b : P) : s.weightedVSub p w = s.weightedVSubOfPoint p b w

Full source

/-- `weightedVSub` gives the sum of the results of subtracting any
base point, when the sum of the weights is 0. -/
theorem weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero (w : ι → k) (p : ι → P)
    (h : ∑ i ∈ s, w i = 0) (b : P) : s.weightedVSub p w = s.weightedVSubOfPoint p b w :=
  s.weightedVSubOfPoint_eq_of_sum_eq_zero w p h _ _

Equality of Weighted Vector Subtraction and Base-Point-Weighted Subtraction when Weights Sum to Zero

Informal description

For a finite set $s$ of indices $\iota$, a family of points $p : \iota \to P$ in an affine space with associated vector space $V$ over a field $k$, and weights $w : \iota \to k$ such that $\sum_{i \in s} w_i = 0$, the weighted vector subtraction $\text{weightedVSub}_s(p, w)$ is equal to $\text{weightedVSubOfPoint}_s(p, b, w)$ for any base point $b \in P$. That is, \[ \sum_{i \in s} w_i \cdot (p_i - b') = \sum_{i \in s} w_i \cdot (p_i - b) \] where $b'$ is the implicitly chosen base point in $\text{weightedVSub}$ and $b$ is any explicitly given base point.

Finset.weightedVSub_apply_const theorem

(w : ι → k) (p : P) (h : ∑ i ∈ s, w i = 0) : s.weightedVSub (fun _ => p) w = 0

Full source

/-- The value of `weightedVSub`, where the given points are equal and the sum of the weights
is 0. -/
@[simp]
theorem weightedVSub_apply_const (w : ι → k) (p : P) (h : ∑ i ∈ s, w i = 0) :
    s.weightedVSub (fun _ => p) w = 0 := by
  rw [weightedVSub, weightedVSubOfPoint_apply_const, h, zero_smul]

Weighted Vector Subtraction of Constant Points with Zero Sum of Weights Yields Zero

Informal description

For any finite set $s$ of indices $\iota$, any point $p$ in an affine space, and any weights $w : \iota \to k$ such that $\sum_{i \in s} w_i = 0$, the weighted vector subtraction of the constant family of points (all equal to $p$) with weights $w$ is the zero vector, i.e., \[ \text{weightedVSub}_s (\lambda \_, p) w = 0. \]

Finset.weightedVSub_empty theorem

(w : ι → k) (p : ι → P) : (∅ : Finset ι).weightedVSub p w = (0 : V)

Full source

/-- The `weightedVSub` for an empty set is 0. -/
@[simp]
theorem weightedVSub_empty (w : ι → k) (p : ι → P) : (∅ : Finset ι).weightedVSub p w = (0 : V) := by
  simp [weightedVSub_apply]

Weighted Vector Subtraction over Empty Set is Zero

Informal description

For any weight function $w \colon \iota \to k$ and any family of points $p \colon \iota \to P$ in an affine space, the weighted vector subtraction over the empty set is the zero vector, i.e., \[ \text{weightedVSub}_{\emptyset}(p, w) = 0. \]

Finset.weightedVSub_vadd theorem

 {s : Finset ι} {w : ι → k} (h : ∑ i ∈ s, w i = 0) (p : ι → P) (v : V) : s.weightedVSub (v +ᵥ p) w = s.weightedVSub p w

Full source

lemma weightedVSub_vadd {s : Finset ι} {w : ι → k} (h : ∑ i ∈ s, w i = 0) (p : ι → P) (v : V) :
    s.weightedVSub (v +ᵥ p) w = s.weightedVSub p w := by
  rw [weightedVSub, weightedVSubOfPoint_vadd,
    weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ _ _ h]

Invariance of Weighted Vector Subtraction under Translation when Weights Sum to Zero

Informal description

For any finite set $s$ of indices $\iota$, weights $w \colon \iota \to k$ such that $\sum_{i \in s} w_i = 0$, family of points $p \colon \iota \to P$ in an affine space with associated vector space $V$, and vector $v \in V$, the weighted vector subtraction satisfies: \[ \text{weightedVSub}_s(v + p, w) = \text{weightedVSub}_s(p, w) \] where $v + p$ denotes the translation of each point $p_i$ by $v$.

Finset.weightedVSub_smul theorem

 {G : Type*} [Group G] [DistribMulAction G V] [SMulCommClass G k V] {s : Finset ι} {w : ι → k} (h : ∑ i ∈ s, w i = 0)
  (p : ι → V) (a : G) : s.weightedVSub (a • p) w = a • s.weightedVSub p w

Full source

lemma weightedVSub_smul {G : Type*} [Group G] [DistribMulAction G V] [SMulCommClass G k V]
    {s : Finset ι} {w : ι → k} (h : ∑ i ∈ s, w i = 0) (p : ι → V) (a : G) :
    s.weightedVSub (a • p) w = a • s.weightedVSub p w := by
  rw [weightedVSub, weightedVSubOfPoint_smul,
    weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ _ _ h]

Equivariance of Weighted Vector Subtraction under Group Action with Zero Weight Sum

Informal description

Let $G$ be a group acting distributively on a vector space $V$ over a field $k$, with the actions of $G$ and $k$ on $V$ commuting. For any finite set $s$ of indices $\iota$, any weights $w \colon \iota \to k$ such that $\sum_{i \in s} w_i = 0$, any points $p \colon \iota \to V$, and any element $a \in G$, we have: \[ \sum_{i \in s} w_i \cdot (a \cdot p_i - b) = a \cdot \sum_{i \in s} w_i \cdot (p_i - a^{-1} \cdot b), \] where $b$ is an arbitrary base point (the result is independent of the choice of $b$ due to the zero sum condition on weights).

Finset.weightedVSub_congr theorem

 {w₁ w₂ : ι → k} (hw : ∀ i ∈ s, w₁ i = w₂ i) {p₁ p₂ : ι → P} (hp : ∀ i ∈ s, p₁ i = p₂ i) :
  s.weightedVSub p₁ w₁ = s.weightedVSub p₂ w₂

Full source

/-- `weightedVSub` gives equal results for two families of weights and two families of points
that are equal on `s`. -/
theorem weightedVSub_congr {w₁ w₂ : ι → k} (hw : ∀ i ∈ s, w₁ i = w₂ i) {p₁ p₂ : ι → P}
    (hp : ∀ i ∈ s, p₁ i = p₂ i) : s.weightedVSub p₁ w₁ = s.weightedVSub p₂ w₂ :=
  s.weightedVSubOfPoint_congr hw hp _

Equality of Weighted Vector Subtraction for Equal Weights and Points on a Finite Set

Informal description

For any finite set $s$ of indices $\iota$, if two families of weights $w_1, w_2 : \iota \to k$ satisfy $w_1(i) = w_2(i)$ for all $i \in s$, and two families of points $p_1, p_2 : \iota \to P$ in an affine space satisfy $p_1(i) = p_2(i)$ for all $i \in s$, then the weighted vector subtractions are equal: \[ \sum_{i \in s} w_1(i) \cdot (p_1(i) - b) = \sum_{i \in s} w_2(i) \cdot (p_2(i) - b), \] where $b$ is an arbitrary base point (the result is independent of the choice of $b$ when the sum of weights is zero).

Finset.weightedVSub_indicator_subset theorem

 (w : ι → k) (p : ι → P) {s₁ s₂ : Finset ι} (h : s₁ ⊆ s₂) :
  s₁.weightedVSub p w = s₂.weightedVSub p (Set.indicator (↑s₁) w)

Full source

/-- The weighted sum is unaffected by changing the weights to the
corresponding indicator function and adding points to the set. -/
theorem weightedVSub_indicator_subset (w : ι → k) (p : ι → P) {s₁ s₂ : Finset ι} (h : s₁ ⊆ s₂) :
    s₁.weightedVSub p w = s₂.weightedVSub p (Set.indicator (↑s₁) w) :=
  weightedVSubOfPoint_indicator_subset _ _ _ h

Weighted Vector Subtraction Unaffected by Indicator Weights and Superset

Informal description

For a finite set of indices $\iota$, a family of points $p \colon \iota \to P$ in an affine space with associated vector space $V$ over a field $k$, and weights $w \colon \iota \to k$, if $s_1 \subseteq s_2$ are two finite subsets of $\iota$, then the weighted vector subtraction over $s_1$ is equal to the weighted vector subtraction over $s_2$ using the indicator function of $s_1$ as weights. That is, \[ \sum_{i \in s_1} w_i \cdot (p_i - b) = \sum_{i \in s_2} \mathbf{1}_{s_1}(i) \cdot w_i \cdot (p_i - b), \] where $\mathbf{1}_{s_1}$ is the indicator function of $s_1$ and $b$ is an arbitrary base point (the result is independent of $b$ when the sum of weights is zero).

Finset.weightedVSub_map theorem

 (e : ι₂ ↪ ι) (w : ι → k) (p : ι → P) : (s₂.map e).weightedVSub p w = s₂.weightedVSub (p ∘ e) (w ∘ e)

Full source

/-- A weighted subtraction, over the image of an embedding, equals a
weighted subtraction with the same points and weights over the
original `Finset`. -/
theorem weightedVSub_map (e : ι₂ ↪ ι) (w : ι → k) (p : ι → P) :
    (s₂.map e).weightedVSub p w = s₂.weightedVSub (p ∘ e) (w ∘ e) :=
  s₂.weightedVSubOfPoint_map _ _ _ _

Weighted Vector Subtraction under Injective Mapping

Informal description

Let $e : \iota_2 \hookrightarrow \iota$ be an injective function, $w : \iota \to k$ a weight function, and $p : \iota \to P$ a family of points in an affine space with associated vector space $V$ over a field $k$. For any finite subset $s_2 \subseteq \iota_2$, the weighted vector subtraction over the image $e(s_2)$ is equal to the weighted vector subtraction over $s_2$ with points and weights composed with $e$. That is, \[ \sum_{i \in e(s_2)} w_i \cdot (p_i - b) = \sum_{j \in s_2} w_{e(j)} \cdot (p_{e(j)} - b) \] where $b$ is an arbitrary base point (chosen via the axiom of choice), $\cdot$ denotes scalar multiplication, and $-$ denotes vector subtraction in the affine space.

Finset.sum_smul_vsub_eq_weightedVSub_sub theorem

 (w : ι → k) (p₁ p₂ : ι → P) : (∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i)) = s.weightedVSub p₁ w - s.weightedVSub p₂ w

Full source

/-- A weighted sum of pairwise subtractions, expressed as a subtraction of two `weightedVSub`
expressions. -/
theorem sum_smul_vsub_eq_weightedVSub_sub (w : ι → k) (p₁ p₂ : ι → P) :
    (∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i)) = s.weightedVSub p₁ w - s.weightedVSub p₂ w :=
  s.sum_smul_vsub_eq_weightedVSubOfPoint_sub _ _ _ _

Weighted Sum of Vector Subtractions as Difference of Weighted VSubs

Informal description

For a finite set $s$ of indices $\iota$, weights $w : \iota \to k$, and two families of points $p_1, p_2 : \iota \to P$ in an affine space with associated vector space $V$ over a field $k$, the weighted sum of vector subtractions equals the difference of the weighted vector subtractions: \[ \sum_{i \in s} w_i \cdot (p_1 i - p_2 i) = \text{weightedVSub}_s(p_1, w) - \text{weightedVSub}_s(p_2, w), \] where $p - q$ denotes the vector from $q$ to $p$ and $\cdot$ denotes scalar multiplication in $V$.

Finset.sum_smul_vsub_const_eq_weightedVSub theorem

 (w : ι → k) (p₁ : ι → P) (p₂ : P) (h : ∑ i ∈ s, w i = 0) : (∑ i ∈ s, w i • (p₁ i -ᵥ p₂)) = s.weightedVSub p₁ w

Full source

/-- A weighted sum of pairwise subtractions, where the point on the right is constant and the
sum of the weights is 0. -/
theorem sum_smul_vsub_const_eq_weightedVSub (w : ι → k) (p₁ : ι → P) (p₂ : P)
    (h : ∑ i ∈ s, w i = 0) : (∑ i ∈ s, w i • (p₁ i -ᵥ p₂)) = s.weightedVSub p₁ w := by
  rw [sum_smul_vsub_eq_weightedVSub_sub, s.weightedVSub_apply_const _ _ h, sub_zero]

Weighted Sum of Vector Subtractions from Fixed Point Equals Weighted VSub When Weights Sum to Zero

Informal description

For a finite set $s$ of indices $\iota$, weights $w : \iota \to k$ with $\sum_{i \in s} w_i = 0$, a family of points $p_1 : \iota \to P$ in an affine space, and a fixed point $p_2 \in P$, the weighted sum of vector subtractions equals the weighted vector subtraction of $p_1$: \[ \sum_{i \in s} w_i \cdot (p_1 i - p_2) = \text{weightedVSub}_s(p_1, w), \] where $\cdot$ denotes scalar multiplication and $-$ denotes vector subtraction in the affine space.

Finset.sum_smul_const_vsub_eq_neg_weightedVSub theorem

 (w : ι → k) (p₂ : ι → P) (p₁ : P) (h : ∑ i ∈ s, w i = 0) : (∑ i ∈ s, w i • (p₁ -ᵥ p₂ i)) = -s.weightedVSub p₂ w

Full source

/-- A weighted sum of pairwise subtractions, where the point on the left is constant and the
sum of the weights is 0. -/
theorem sum_smul_const_vsub_eq_neg_weightedVSub (w : ι → k) (p₂ : ι → P) (p₁ : P)
    (h : ∑ i ∈ s, w i = 0) : (∑ i ∈ s, w i • (p₁ -ᵥ p₂ i)) = -s.weightedVSub p₂ w := by
  rw [sum_smul_vsub_eq_weightedVSub_sub, s.weightedVSub_apply_const _ _ h, zero_sub]

Weighted Sum of Constant-Vector Subtractions Equals Negative Weighted VSub

Informal description

For a finite set $s$ of indices $\iota$, weights $w : \iota \to k$ such that $\sum_{i \in s} w_i = 0$, a point $p_1 \in P$, and a family of points $p_2 : \iota \to P$ in an affine space with associated vector space $V$ over a field $k$, the weighted sum of vector subtractions satisfies: \[ \sum_{i \in s} w_i \cdot (p_1 - p_2 i) = -\text{weightedVSub}_s(p_2, w), \] where $p_1 - p_2 i$ denotes the vector from $p_2 i$ to $p_1$ and $\cdot$ denotes scalar multiplication in $V$.

Finset.weightedVSub_sdiff theorem

 [DecidableEq ι] {s₂ : Finset ι} (h : s₂ ⊆ s) (w : ι → k) (p : ι → P) :
  (s \ s₂).weightedVSub p w + s₂.weightedVSub p w = s.weightedVSub p w

Full source

/-- A weighted sum may be split into such sums over two subsets. -/
theorem weightedVSub_sdiff [DecidableEq ι] {s₂ : Finset ι} (h : s₂ ⊆ s) (w : ι → k) (p : ι → P) :
    (s \ s₂).weightedVSub p w + s₂.weightedVSub p w = s.weightedVSub p w :=
  s.weightedVSubOfPoint_sdiff h _ _ _

Splitting Property of Weighted Vector Subtraction in Affine Space

Informal description

Let $s$ be a finite set of indices $\iota$ with decidable equality, and let $s_2 \subseteq s$ be a subset. For any family of points $p : \iota \to P$ in an affine space with associated vector space $V$ over a field $k$, and weights $w : \iota \to k$, the weighted vector subtraction satisfies: \[ (s \setminus s_2).\text{weightedVSub}(p, w) + s_2.\text{weightedVSub}(p, w) = s.\text{weightedVSub}(p, w), \] where $\text{weightedVSub}_s(p, w) = \sum_{i \in s} w_i \cdot (p_i - b)$ for an arbitrary base point $b \in P$ (with the result independent of $b$ when $\sum_{i \in s} w_i = 0$).

Finset.weightedVSub_sdiff_sub theorem

 [DecidableEq ι] {s₂ : Finset ι} (h : s₂ ⊆ s) (w : ι → k) (p : ι → P) :
  (s \ s₂).weightedVSub p w - s₂.weightedVSub p (-w) = s.weightedVSub p w

Full source

/-- A weighted sum may be split into a subtraction of such sums over two subsets. -/
theorem weightedVSub_sdiff_sub [DecidableEq ι] {s₂ : Finset ι} (h : s₂ ⊆ s) (w : ι → k)
    (p : ι → P) : (s \ s₂).weightedVSub p w - s₂.weightedVSub p (-w) = s.weightedVSub p w :=
  s.weightedVSubOfPoint_sdiff_sub h _ _ _

Subtractive Splitting Property of Weighted Vector Subtraction in Affine Space

Informal description

Let $s$ be a finite set of indices $\iota$ with decidable equality, and let $s_2 \subseteq s$ be a subset. For any family of points $p : \iota \to P$ in an affine space with associated vector space $V$ over a field $k$, and weights $w : \iota \to k$, the following equality holds: \[ \sum_{i \in s \setminus s_2} w_i \cdot (p_i - b) - \sum_{i \in s_2} (-w_i) \cdot (p_i - b) = \sum_{i \in s} w_i \cdot (p_i - b), \] where $b$ is an arbitrary base point in $P$ and $p_i - b$ denotes the vector from $b$ to $p_i$.

Finset.weightedVSub_subtype_eq_filter theorem

 (w : ι → k) (p : ι → P) (pred : ι → Prop) [DecidablePred pred] :
  ((s.subtype pred).weightedVSub (fun i => p i) fun i => w i) = {x ∈ s | pred x}.weightedVSub p w

Full source

/-- A weighted sum over `s.subtype pred` equals one over `{x ∈ s | pred x}`. -/
theorem weightedVSub_subtype_eq_filter (w : ι → k) (p : ι → P) (pred : ι → Prop)
    [DecidablePred pred] :
    ((s.subtype pred).weightedVSub (fun i => p i) fun i => w i) =
      {x ∈ s | pred x}.weightedVSub p w :=
  s.weightedVSubOfPoint_subtype_eq_filter _ _ _ _

Equality of Weighted Vector Subtraction over Subtype and Filtered Set

Informal description

For a finite set $s$ of indices $\iota$, a family of points $p : \iota \to P$ in an affine space with associated vector space $V$ over a field $k$, weights $w : \iota \to k$, and a predicate $\text{pred} : \iota \to \text{Prop}$, the weighted vector subtraction over the subtype of $s$ satisfying $\text{pred}$ is equal to the weighted vector subtraction over the filtered set $\{x \in s \mid \text{pred }x\}$. That is, \[ \sum_{i \in s, \text{pred }i} w_i \cdot (p_i - b) = \sum_{i \in \{x \in s \mid \text{pred }x\}} w_i \cdot (p_i - b), \] where $b$ is an arbitrary base point (implicitly chosen) and $p_i - b$ denotes the vector from $b$ to $p_i$.

Finset.weightedVSub_filter_of_ne theorem

 (w : ι → k) (p : ι → P) {pred : ι → Prop} [DecidablePred pred] (h : ∀ i ∈ s, w i ≠ 0 → pred i) :
  {x ∈ s | pred x}.weightedVSub p w = s.weightedVSub p w

Full source

/-- A weighted sum over `{x ∈ s | pred x}` equals one over `s` if all the weights at indices in `s`
not satisfying `pred` are zero. -/
theorem weightedVSub_filter_of_ne (w : ι → k) (p : ι → P) {pred : ι → Prop} [DecidablePred pred]
    (h : ∀ i ∈ s, w i ≠ 0 → pred i) : {x ∈ s | pred x}.weightedVSub p w = s.weightedVSub p w :=
  s.weightedVSubOfPoint_filter_of_ne _ _ _ h

Equality of Weighted Vector Subtraction Under Nonzero Weight Filtering

Informal description

Let $s$ be a finite set of indices, $w : \iota \to k$ a weight function, and $p : \iota \to P$ a family of points in an affine space with associated vector space $V$ over field $k$. For any predicate $\text{pred} : \iota \to \text{Prop}$, if for all $i \in s$ with $w_i \neq 0$ we have $\text{pred}(i)$, then the weighted vector subtraction over the filtered set $\{x \in s \mid \text{pred}(x)\}$ equals the weighted vector subtraction over the entire set $s$: \[ \sum_{i \in \{x \in s \mid \text{pred}(x)\}} w_i \cdot (p_i - b) = \sum_{i \in s} w_i \cdot (p_i - b), \] where $b$ is an arbitrary base point (implicitly chosen via the axiom of choice) and $p_i - b$ denotes the vector from $b$ to $p_i$.

Finset.weightedVSub_const_smul theorem

(w : ι → k) (p : ι → P) (c : k) : s.weightedVSub p (c • w) = c • s.weightedVSub p w

Full source

/-- A constant multiplier of the weights in `weightedVSub_of` may be moved outside the sum. -/
theorem weightedVSub_const_smul (w : ι → k) (p : ι → P) (c : k) :
    s.weightedVSub p (c • w) = c • s.weightedVSub p w :=
  s.weightedVSubOfPoint_const_smul _ _ _ _

Scalar Multiplication Commutes with Weighted Vector Subtraction in Affine Space

Informal description

For a finite set $s$ of indices $\iota$, a family of points $p : \iota \to P$ in an affine space with associated vector space $V$ over a field $k$, weights $w : \iota \to k$, and a scalar $c \in k$, the weighted vector subtraction satisfies: \[ \sum_{i \in s} (c \cdot w_i) \cdot (p_i - b) = c \cdot \left(\sum_{i \in s} w_i \cdot (p_i - b)\right), \] where $b$ is an arbitrary base point (implicitly chosen) and $p_i - b$ denotes the vector from $b$ to $p_i$.

Finset.instAddTorsorForall instance

: AffineSpace (ι → k) (ι → k)

Full source

instance : AffineSpace (ι → k) (ι → k) := Pi.instAddTorsor

Function Space as an Affine Space Over Itself

Informal description

For any index type $\iota$ and field $k$, the function space $\iota \to k$ forms an affine space over itself, where the underlying vector space is also $\iota \to k$.

Finset.affineCombination definition

(p : ι → P) : (ι → k) →ᵃ[k] P

Full source

/-- 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. -/
def affineCombination (p : ι → P) : (ι → k) →ᵃ[k] P where
  toFun w := s.weightedVSubOfPoint p (Classical.choice S.nonempty) w +ᵥ Classical.choice S.nonempty
  linear := s.weightedVSub p
  map_vadd' w₁ w₂ := by simp_rw [vadd_vadd, weightedVSub, vadd_eq_add, LinearMap.map_add]

Affine combination of points in an affine space

Informal description

Given a finite set of indices $s$ and a family of points $p : \iota \to P$ in an affine space over a field $k$, the affine combination is an affine map from the space of weight functions $\iota \to k$ to $P$. For a given weight function $w$, it computes the weighted sum $\sum_{i \in s} w_i \cdot (p_i - b) + b$, where $b$ is an arbitrary base point in $P$ (chosen using the axiom of choice). This construction is particularly useful when the sum of weights is 1, making the result independent of the choice of base point.

Finset.affineCombination_linear theorem

(p : ι → P) : (s.affineCombination k p).linear = s.weightedVSub p

Full source

/-- The linear map corresponding to `affineCombination` is
`weightedVSub`. -/
@[simp]
theorem affineCombination_linear (p : ι → P) :
    (s.affineCombination k p).linear = s.weightedVSub p :=
  rfl

Linear Part of Affine Combination Equals Weighted Vector Subtraction

Informal description

For a finite set of indices $s$ and a family of points $p : \iota \to P$ in an affine space over a field $k$, the linear part of the affine combination map $\text{affineCombination}_k p$ is equal to the weighted vector subtraction map $\text{weightedVSub}_k p$. In other words, the linear transformation associated with the affine combination is precisely the weighted vector subtraction operation.

Finset.affineCombination_apply theorem

 (w : ι → k) (p : ι → P) :
  (s.affineCombination k p) w = s.weightedVSubOfPoint p (Classical.choice S.nonempty) w +ᵥ Classical.choice S.nonempty

Full source

/-- 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`. -/
theorem affineCombination_apply (w : ι → k) (p : ι → P) :
    (s.affineCombination k p) w =
      s.weightedVSubOfPoint p (Classical.choice S.nonempty) w +ᵥ Classical.choice S.nonempty :=
  rfl

Evaluation of Affine Combination as Weighted Vector Sum Plus Base Point

Informal description

For a finite set $s$ of indices $\iota$, a weight function $w \colon \iota \to k$, and a family of points $p \colon \iota \to P$ in an affine space over a field $k$, the affine combination evaluated at $w$ is given by \[ (s.\text{affineCombination}_k\, p)\, w = s.\text{weightedVSubOfPoint}\, p\, b\, w + b, \] where $b$ is an arbitrary base point in $P$ (chosen using the axiom of choice).

Finset.affineCombination_apply_const theorem

(w : ι → k) (p : P) (h : ∑ i ∈ s, w i = 1) : s.affineCombination k (fun _ => p) w = p

Full source

/-- The value of `affineCombination`, where the given points are equal. -/
@[simp]
theorem affineCombination_apply_const (w : ι → k) (p : P) (h : ∑ i ∈ s, w i = 1) :
    s.affineCombination k (fun _ => p) w = p := by
  rw [affineCombination_apply, s.weightedVSubOfPoint_apply_const, h, one_smul, vsub_vadd]

Affine Combination of Constant Points with Sum of Weights One

Informal description

For a finite set $s$ of indices, a point $p$ in an affine space over a field $k$, and weights $w : \iota \to k$ such that $\sum_{i \in s} w_i = 1$, the affine combination of the constant family of points (all equal to $p$) with weights $w$ equals $p$. That is: \[ \sum_{i \in s} w_i p = p \]

Finset.affineCombination_congr theorem

 {w₁ w₂ : ι → k} (hw : ∀ i ∈ s, w₁ i = w₂ i) {p₁ p₂ : ι → P} (hp : ∀ i ∈ s, p₁ i = p₂ i) :
  s.affineCombination k p₁ w₁ = s.affineCombination k p₂ w₂

Full source

/-- `affineCombination` gives equal results for two families of weights and two families of
points that are equal on `s`. -/
theorem affineCombination_congr {w₁ w₂ : ι → k} (hw : ∀ i ∈ s, w₁ i = w₂ i) {p₁ p₂ : ι → P}
    (hp : ∀ i ∈ s, p₁ i = p₂ i) : s.affineCombination k p₁ w₁ = s.affineCombination k p₂ w₂ := by
  simp_rw [affineCombination_apply, s.weightedVSubOfPoint_congr hw hp]

Affine Combination is Uniquely Determined by Weights and Points on a Finite Set

Informal description

Let $s$ be a finite set of indices, and let $w_1, w_2 \colon \iota \to k$ be two weight functions that agree on $s$ (i.e., $w_1(i) = w_2(i)$ for all $i \in s$). Let $p_1, p_2 \colon \iota \to P$ be two families of points in an affine space over a field $k$ that agree on $s$ (i.e., $p_1(i) = p_2(i)$ for all $i \in s$). Then the affine combinations of these points with the respective weights are equal: \[ \text{affineCombination}_s(p_1, w_1) = \text{affineCombination}_s(p_2, w_2). \]

Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one theorem

 (w : ι → k) (p : ι → P) (h : ∑ i ∈ s, w i = 1) (b : P) : s.affineCombination k p w = s.weightedVSubOfPoint p b w +ᵥ b

Full source

/-- `affineCombination` gives the sum with any base point, when the
sum of the weights is 1. -/
theorem affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one (w : ι → k) (p : ι → P)
    (h : ∑ i ∈ s, w i = 1) (b : P) :
    s.affineCombination k p w = s.weightedVSubOfPoint p b w +ᵥ b :=
  s.weightedVSubOfPoint_vadd_eq_of_sum_eq_one w p h _ _

Affine Combination as Weighted Vector Subtraction Plus Base Point

Informal description

For a finite set $s$ of indices, a family of points $p : \iota \to P$ in an affine space over a field $k$, and weights $w : \iota \to k$ such that $\sum_{i \in s} w_i = 1$, the affine combination of points equals the weighted vector subtraction from any base point $b \in P$ followed by translation by $b$. That is: \[ \sum_{i \in s} w_i p_i = \sum_{i \in s} w_i (p_i - b) + b \]

Finset.weightedVSub_vadd_affineCombination theorem

 (w₁ w₂ : ι → k) (p : ι → P) : s.weightedVSub p w₁ +ᵥ s.affineCombination k p w₂ = s.affineCombination k p (w₁ + w₂)

Full source

/-- Adding a `weightedVSub` to an `affineCombination`. -/
theorem weightedVSub_vadd_affineCombination (w₁ w₂ : ι → k) (p : ι → P) :
    s.weightedVSub p w₁ +ᵥ s.affineCombination k p w₂ = s.affineCombination k p (w₁ + w₂) := by
  rw [← vadd_eq_add, AffineMap.map_vadd, affineCombination_linear]

Sum of Weighted Vector Subtraction and Affine Combination Equals Combined Affine Combination

Informal description

For a finite set $s$ of indices, a family of points $p : \iota \to P$ in an affine space over a field $k$, and weight functions $w_1, w_2 : \iota \to k$, the sum of the weighted vector subtraction of $p$ with weights $w_1$ and the affine combination of $p$ with weights $w_2$ equals the affine combination of $p$ with weights $w_1 + w_2$. That is: \[ \sum_{i \in s} w_1(i)(p_i - b) + \sum_{i \in s} w_2(i)p_i = \sum_{i \in s} (w_1(i) + w_2(i))p_i \] where $b$ is an arbitrary base point (the result is independent of the choice of $b$).

Finset.affineCombination_vsub theorem

 (w₁ w₂ : ι → k) (p : ι → P) : s.affineCombination k p w₁ -ᵥ s.affineCombination k p w₂ = s.weightedVSub p (w₁ - w₂)

Full source

/-- Subtracting two `affineCombination`s. -/
theorem affineCombination_vsub (w₁ w₂ : ι → k) (p : ι → P) :
    s.affineCombination k p w₁ -ᵥ s.affineCombination k p w₂ = s.weightedVSub p (w₁ - w₂) := by
  rw [← AffineMap.linearMap_vsub, affineCombination_linear, vsub_eq_sub]

Vector Difference of Affine Combinations Equals Weighted Vector Subtraction of Weight Differences

Informal description

For a finite set $s$ of indices, a family of points $p : \iota \to P$ in an affine space over a field $k$, and weight functions $w_1, w_2 : \iota \to k$, the vector difference between the affine combinations of $p$ with weights $w_1$ and $w_2$ equals the weighted vector subtraction of $p$ with weights $w_1 - w_2$. That is: \[ \sum_{i \in s} w_1(i) p_i - \sum_{i \in s} w_2(i) p_i = \sum_{i \in s} (w_1(i) - w_2(i)) (p_i - b) \] where $b$ is an arbitrary base point (the result is independent of the choice of $b$).

Finset.attach_affineCombination_of_injective theorem

 [DecidableEq P] (s : Finset P) (w : P → k) (f : s → P) (hf : Function.Injective f) :
  s.attach.affineCombination k f (w ∘ f) = (image f univ).affineCombination k id w

Full source

theorem attach_affineCombination_of_injective [DecidableEq P] (s : Finset P) (w : P → k) (f : s → P)
    (hf : Function.Injective f) :
    s.attach.affineCombination k f (w ∘ f) = (image f univ).affineCombination k id w := by
  simp only [affineCombination, weightedVSubOfPoint_apply, id, vadd_right_cancel_iff,
    Function.comp_apply, AffineMap.coe_mk]
  let g₁ : s → V := fun i => w (f i) • (f i -ᵥ Classical.choice S.nonempty)
  let g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice S.nonempty)
  change univ.sum g₁ = (image f univ).sum g₂
  have hgf : g₁ = g₂ ∘ f := by
    ext
    simp [g₁, g₂]
  rw [hgf, sum_image]
  · simp only [g₁, g₂,Function.comp_apply]
  · exact fun _ _ _ _ hxy => hf hxy

Equality of Affine Combinations under Injective Mapping

Informal description

Let $P$ be an affine space over a field $k$, and let $s$ be a finite set of points in $P$. Given a weight function $w : P \to k$ and an injective function $f : s \to P$, the affine combination of the points in $s$ with weights $w \circ f$ is equal to the affine combination of the image of $f$ with weights $w$. More precisely, we have: \[ \sum_{p \in s} w(f(p)) \cdot f(p) = \sum_{q \in f(s)} w(q) \cdot q \] where the sums are taken as affine combinations in $P$.

Finset.attach_affineCombination_coe theorem

 (s : Finset P) (w : P → k) : s.attach.affineCombination k ((↑) : s → P) (w ∘ (↑)) = s.affineCombination k id w

Full source

theorem attach_affineCombination_coe (s : Finset P) (w : P → k) :
    s.attach.affineCombination k ((↑) : s → P) (w ∘ (↑)) = s.affineCombination k id w := by
  classical rw [attach_affineCombination_of_injective s w ((↑) : s → P) Subtype.coe_injective,
      univ_eq_attach, attach_image_val]

Equality of Affine Combinations under Canonical Embedding

Informal description

Let $P$ be an affine space over a field $k$, and let $s$ be a finite set of points in $P$. Given a weight function $w : P \to k$, the affine combination of the points in $s$ with weights $w$ is equal to the affine combination of the canonical embedding of $s$ into $P$ with weights $w$ composed with this embedding. More precisely, we have: \[ \sum_{p \in s} w(p) \cdot p = \sum_{p \in s} w(p) \cdot p \] where the sums are taken as affine combinations in $P$.

Finset.weightedVSub_eq_linear_combination theorem

{ι} (s : Finset ι) {w : ι → k} {p : ι → V} (hw : s.sum w = 0) : s.weightedVSub p w = ∑ i ∈ s, w i • p i

Full source

/-- Viewing a module as an affine space modelled on itself, a `weightedVSub` is just a linear
combination. -/
@[simp]
theorem weightedVSub_eq_linear_combination {ι} (s : Finset ι) {w : ι → k} {p : ι → V}
    (hw : s.sum w = 0) : s.weightedVSub p w = ∑ i ∈ s, w i • p i := by
  simp [s.weightedVSub_apply, vsub_eq_sub, smul_sub, ← Finset.sum_smul, hw]

Weighted Vector Subtraction as Linear Combination under Zero Sum Condition

Informal description

Let $s$ be a finite set of indices $\iota$, $w : \iota \to k$ be a weight function, and $p : \iota \to V$ be a family of vectors in a vector space $V$ over a field $k$. If the sum of the weights $\sum_{i \in s} w_i = 0$, then the weighted vector subtraction of $p$ with weights $w$ equals the linear combination $\sum_{i \in s} w_i \cdot p_i$, i.e., \[ \text{weightedVSub}_s(p, w) = \sum_{i \in s} w_i p_i. \]

Finset.affineCombination_eq_linear_combination theorem

 (s : Finset ι) (p : ι → V) (w : ι → k) (hw : ∑ i ∈ s, w i = 1) : s.affineCombination k p w = ∑ i ∈ s, w i • p i

Full source

/-- Viewing a module as an affine space modelled on itself, affine combinations are just linear
combinations. -/
@[simp]
theorem affineCombination_eq_linear_combination (s : Finset ι) (p : ι → V) (w : ι → k)
    (hw : ∑ i ∈ s, w i = 1) : s.affineCombination k p w = ∑ i ∈ s, w i • p i := by
  simp [s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p hw 0]

Affine Combination Equals Linear Combination for Unit Sum Weights

Informal description

For a finite set $s$ of indices $\iota$, a family of vectors $p : \iota \to V$ in a vector space $V$ over a field $k$, and weights $w : \iota \to k$ such that $\sum_{i \in s} w_i = 1$, the affine combination of the vectors equals their linear combination: \[ \sum_{i \in s} w_i p_i = \sum_{i \in s} w_i \cdot p_i. \]

Finset.affineCombination_of_eq_one_of_eq_zero theorem

 (w : ι → k) (p : ι → P) {i : ι} (his : i ∈ s) (hwi : w i = 1) (hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0) :
  s.affineCombination k p w = p i

Full source

/-- 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. -/
@[simp]
theorem affineCombination_of_eq_one_of_eq_zero (w : ι → k) (p : ι → P) {i : ι} (his : i ∈ s)
    (hwi : w i = 1) (hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0) : s.affineCombination k p w = p i := by
  have h1 : ∑ i ∈ s, w i = 1 := hwi ▸ sum_eq_single i hw0 fun h => False.elim (h his)
  rw [s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p h1 (p i),
    weightedVSubOfPoint_apply]
  convert zero_vadd V (p i)
  refine sum_eq_zero ?_
  intro i2 hi2
  by_cases h : i2 = i
  · simp [h]
  · simp [hw0 i2 hi2 h]

Affine Combination with Single Nonzero Weight Yields Corresponding Point

Informal description

Let $s$ be a finite set of indices, $w : \iota \to k$ a weight function, and $p : \iota \to P$ a family of points in an affine space over a field $k$. If there exists an index $i \in s$ such that $w_i = 1$ and $w_j = 0$ for all other indices $j \in s$ with $j \neq i$, then the affine combination of the points $p$ with weights $w$ equals $p_i$, i.e., \[ \sum_{j \in s} w_j p_j = p_i. \]

Finset.affineCombination_indicator_subset theorem

 (w : ι → k) (p : ι → P) {s₁ s₂ : Finset ι} (h : s₁ ⊆ s₂) :
  s₁.affineCombination k p w = s₂.affineCombination k p (Set.indicator (↑s₁) w)

Full source

/-- An affine combination is unaffected by changing the weights to the
corresponding indicator function and adding points to the set. -/
theorem affineCombination_indicator_subset (w : ι → k) (p : ι → P) {s₁ s₂ : Finset ι}
    (h : s₁ ⊆ s₂) :
    s₁.affineCombination k p w = s₂.affineCombination k p (Set.indicator (↑s₁) w) := by
  rw [affineCombination_apply, affineCombination_apply,
    weightedVSubOfPoint_indicator_subset _ _ _ h]

Affine Combination Unaffected by Indicator Weights and Superset

Informal description

Let $k$ be a ring, $V$ a module over $k$, and $P$ an affine space over $V$. Given two finite subsets $s_1 \subseteq s_2$ of an index set $\iota$, a family of points $p : \iota \to P$, and weights $w : \iota \to k$, the affine combination of $p$ with weights $w$ over $s_1$ equals the affine combination of $p$ with weights $\mathbf{1}_{s_1} \cdot w$ over $s_2$, where $\mathbf{1}_{s_1}$ is the indicator function of $s_1$. That is, \[ \sum_{i \in s_1} w_i p_i = \sum_{j \in s_2} (\mathbf{1}_{s_1}(j) \cdot w_j) p_j, \] where both sums are affine combinations (assuming the weights sum to 1).

Finset.affineCombination_map theorem

 (e : ι₂ ↪ ι) (w : ι → k) (p : ι → P) : (s₂.map e).affineCombination k p w = s₂.affineCombination k (p ∘ e) (w ∘ e)

Full source

/-- An affine combination, over the image of an embedding, equals an
affine combination with the same points and weights over the original
`Finset`. -/
theorem affineCombination_map (e : ι₂ ↪ ι) (w : ι → k) (p : ι → P) :
    (s₂.map e).affineCombination k p w = s₂.affineCombination k (p ∘ e) (w ∘ e) := by
  simp_rw [affineCombination_apply, weightedVSubOfPoint_map]

Affine Combination under Injective Mapping

Informal description

Let $e : \iota_2 \hookrightarrow \iota$ be an injective function, $w : \iota \to k$ a weight function, and $p : \iota \to P$ a family of points in an affine space over a field $k$. For any finite subset $s_2 \subseteq \iota_2$, the affine combination of the points $p$ with weights $w$ over the image $e(s_2)$ is equal to the affine combination of the points $p \circ e$ with weights $w \circ e$ over $s_2$. That is, \[ \sum_{i \in e(s_2)} w_i p_i = \sum_{j \in s_2} w_{e(j)} p_{e(j)} \] where the sums are affine combinations (assuming the weights sum to 1).

Finset.sum_smul_vsub_eq_affineCombination_vsub theorem

 (w : ι → k) (p₁ p₂ : ι → P) :
  (∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i)) = s.affineCombination k p₁ w -ᵥ s.affineCombination k p₂ w

Full source

/-- A weighted sum of pairwise subtractions, expressed as a subtraction of two `affineCombination`
expressions. -/
theorem sum_smul_vsub_eq_affineCombination_vsub (w : ι → k) (p₁ p₂ : ι → P) :
    (∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i)) =
      s.affineCombination k p₁ w -ᵥ s.affineCombination k p₂ w := by
  simp_rw [affineCombination_apply, vadd_vsub_vadd_cancel_right]
  exact s.sum_smul_vsub_eq_weightedVSubOfPoint_sub _ _ _ _

Weighted Sum of Vector Subtractions Equals Difference of Affine Combinations

Informal description

For a finite set $s$ of indices $\iota$, weights $w : \iota \to k$, and two families of points $p_1, p_2 : \iota \to P$ in an affine space over a field $k$, the weighted sum of vector subtractions equals the vector subtraction of the corresponding affine combinations: \[ \sum_{i \in s} w_i \cdot (p_1 i - p_2 i) = \text{affineCombination}_s(p_1, w) - \text{affineCombination}_s(p_2, w), \] where $p_1 i - p_2 i$ denotes the vector from $p_2 i$ to $p_1 i$, $\cdot$ denotes scalar multiplication, and $\text{affineCombination}_s(p, w)$ is the affine combination of points $p$ with weights $w$ over the set $s$.

Finset.sum_smul_vsub_const_eq_affineCombination_vsub theorem

 (w : ι → k) (p₁ : ι → P) (p₂ : P) (h : ∑ i ∈ s, w i = 1) :
  (∑ i ∈ s, w i • (p₁ i -ᵥ p₂)) = s.affineCombination k p₁ w -ᵥ p₂

Full source

/-- A weighted sum of pairwise subtractions, where the point on the right is constant and the
sum of the weights is 1. -/
theorem sum_smul_vsub_const_eq_affineCombination_vsub (w : ι → k) (p₁ : ι → P) (p₂ : P)
    (h : ∑ i ∈ s, w i = 1) : (∑ i ∈ s, w i • (p₁ i -ᵥ p₂)) = s.affineCombination k p₁ w -ᵥ p₂ := by
  rw [sum_smul_vsub_eq_affineCombination_vsub, affineCombination_apply_const _ _ _ h]

Weighted Sum of Vector Differences Equals Affine Combination Minus Fixed Point

Informal description

For a finite set $s$ of indices $\iota$, weights $w : \iota \to k$ such that $\sum_{i \in s} w_i = 1$, a family of points $p_1 : \iota \to P$ in an affine space over a field $k$, and a fixed point $p_2 \in P$, the weighted sum of vector subtractions equals the vector subtraction of the affine combination and the fixed point: \[ \sum_{i \in s} w_i \cdot (p_1 i - p_2) = \text{affineCombination}_s(p_1, w) - p_2, \] where $p_1 i - p_2$ denotes the vector from $p_2$ to $p_1 i$, $\cdot$ denotes scalar multiplication, and $\text{affineCombination}_s(p_1, w)$ is the affine combination of points $p_1$ with weights $w$ over the set $s$.

Finset.sum_smul_const_vsub_eq_vsub_affineCombination theorem

 (w : ι → k) (p₂ : ι → P) (p₁ : P) (h : ∑ i ∈ s, w i = 1) :
  (∑ i ∈ s, w i • (p₁ -ᵥ p₂ i)) = p₁ -ᵥ s.affineCombination k p₂ w

Full source

/-- A weighted sum of pairwise subtractions, where the point on the left is constant and the
sum of the weights is 1. -/
theorem sum_smul_const_vsub_eq_vsub_affineCombination (w : ι → k) (p₂ : ι → P) (p₁ : P)
    (h : ∑ i ∈ s, w i = 1) : (∑ i ∈ s, w i • (p₁ -ᵥ p₂ i)) = p₁ -ᵥ s.affineCombination k p₂ w := by
  rw [sum_smul_vsub_eq_affineCombination_vsub, affineCombination_apply_const _ _ _ h]

Weighted Sum of Vectors from Points Equals Vector from Affine Combination

Informal description

For a finite set $s$ of indices, weights $w : \iota \to k$ with $\sum_{i \in s} w_i = 1$, a point $p_1$ in an affine space over a field $k$, and a family of points $p_2 : \iota \to P$, the weighted sum of the vectors from each $p_2 i$ to $p_1$ equals the vector from the affine combination of $p_2$ with weights $w$ to $p_1$: \[ \sum_{i \in s} w_i \cdot (p_1 - p_2 i) = p_1 - \text{affineCombination}_s(p_2, w), \] where $\text{affineCombination}_s(p_2, w)$ denotes the affine combination of the points $p_2$ with weights $w$ over the set $s$.

Finset.affineCombination_sdiff_sub theorem

 [DecidableEq ι] {s₂ : Finset ι} (h : s₂ ⊆ s) (w : ι → k) (p : ι → P) :
  (s \ s₂).affineCombination k p w -ᵥ s₂.affineCombination k p (-w) = s.weightedVSub p w

Full source

/-- A weighted sum may be split into a subtraction of affine combinations over two subsets. -/
theorem affineCombination_sdiff_sub [DecidableEq ι] {s₂ : Finset ι} (h : s₂ ⊆ s) (w : ι → k)
    (p : ι → P) :
    (s \ s₂).affineCombination k p w -ᵥ s₂.affineCombination k p (-w) = s.weightedVSub p w := by
  simp_rw [affineCombination_apply, vadd_vsub_vadd_cancel_right]
  exact s.weightedVSub_sdiff_sub h _ _

Difference of Affine Combinations Equals Weighted Vector Subtraction

Informal description

Let $s$ be a finite set of indices $\iota$ with decidable equality, and let $s_2 \subseteq s$ be a subset. For any family of points $p : \iota \to P$ in an affine space over a field $k$ and weights $w : \iota \to k$, the difference of the affine combinations over $s \setminus s_2$ with weights $w$ and over $s_2$ with weights $-w$ equals the weighted vector subtraction over $s$ with weights $w$. That is, \[ \sum_{i \in s \setminus s_2} w_i p_i - \sum_{i \in s_2} (-w_i) p_i = \sum_{i \in s} w_i (p_i - b), \] where $b$ is an arbitrary base point in $P$ (the result is independent of the choice of $b$).

Finset.affineCombination_eq_of_weightedVSub_eq_zero_of_eq_neg_one theorem

 {w : ι → k} {p : ι → P} (hw : s.weightedVSub p w = (0 : V)) {i : ι} [DecidablePred (· ≠ i)] (his : i ∈ s)
  (hwi : w i = -1) : {x ∈ s | x ≠ i}.affineCombination k p w = p i

Full source

/-- 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 affineCombination_eq_of_weightedVSub_eq_zero_of_eq_neg_one {w : ι → k} {p : ι → P}
    (hw : s.weightedVSub p w = (0 : V)) {i : ι} [DecidablePred (· ≠ i)] (his : i ∈ s)
    (hwi : w i = -1) : {x ∈ s | x ≠ i}.affineCombination k p w = p i := by
  classical
    rw [← @vsub_eq_zero_iff_eq V, ← hw,
      ← s.affineCombination_sdiff_sub (singleton_subset_iff.2 his), sdiff_singleton_eq_erase,
      ← filter_ne']
    congr
    refine (affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_singleton_self _) ?_ ?_).symm
    · simp [hwi]
    · simp

Affine Combination Equality from Weighted Vector Subtraction Zero Condition with Negative One Weight

Informal description

Let $s$ be a finite set of indices, $w \colon \iota \to k$ a weight function, and $p \colon \iota \to P$ a family of points in an affine space over a field $k$. Suppose the weighted vector subtraction $\sum_{j \in s} w_j (p_j - b) = 0$ for some base point $b \in P$. If there exists an index $i \in s$ such that $w_i = -1$, then the affine combination of the remaining points $\{x \in s \mid x \neq i\}$ with weights $w$ equals $p_i$, i.e., \[ \sum_{\substack{j \in s \\ j \neq i}} w_j p_j = p_i. \]

Finset.affineCombination_subtype_eq_filter theorem

 (w : ι → k) (p : ι → P) (pred : ι → Prop) [DecidablePred pred] :
  ((s.subtype pred).affineCombination k (fun i => p i) fun i => w i) = {x ∈ s | pred x}.affineCombination k p w

Full source

/-- An affine combination over `s.subtype pred` equals one over `{x ∈ s | pred x}`. -/
theorem affineCombination_subtype_eq_filter (w : ι → k) (p : ι → P) (pred : ι → Prop)
    [DecidablePred pred] :
    ((s.subtype pred).affineCombination k (fun i => p i) fun i => w i) =
      {x ∈ s | pred x}.affineCombination k p w := by
  rw [affineCombination_apply, affineCombination_apply, weightedVSubOfPoint_subtype_eq_filter]

Equality of Affine Combinations over Subtype and Filtered Set

Informal description

Let $s$ be a finite set of indices $\iota$, $w \colon \iota \to k$ a weight function, $p \colon \iota \to P$ a family of points in an affine space over a field $k$, and $\text{pred} \colon \iota \to \text{Prop}$ a decidable predicate. Then the affine combination over the subtype of $s$ satisfying $\text{pred}$ is equal to the affine combination over the filtered set $\{x \in s \mid \text{pred }x\}$. That is, \[ \sum_{i \in s, \text{pred }i} w_i \cdot p_i = \sum_{i \in \{x \in s \mid \text{pred }x\}} w_i \cdot p_i, \] where the sums are affine combinations (with weights summing to 1).

Finset.affineCombination_filter_of_ne theorem

 (w : ι → k) (p : ι → P) {pred : ι → Prop} [DecidablePred pred] (h : ∀ i ∈ s, w i ≠ 0 → pred i) :
  {x ∈ s | pred x}.affineCombination k p w = s.affineCombination k p w

Full source

/-- An affine combination over `{x ∈ s | pred x}` equals one over `s` if all the weights at indices
in `s` not satisfying `pred` are zero. -/
theorem affineCombination_filter_of_ne (w : ι → k) (p : ι → P) {pred : ι → Prop}
    [DecidablePred pred] (h : ∀ i ∈ s, w i ≠ 0 → pred i) :
    {x ∈ s | pred x}.affineCombination k p w = s.affineCombination k p w := by
  rw [affineCombination_apply, affineCombination_apply,
    s.weightedVSubOfPoint_filter_of_ne _ _ _ h]

Affine Combination Equality Under Nonzero Weight Filtering

Informal description

Let $s$ be a finite set of indices, $w \colon \iota \to k$ a weight function, and $p \colon \iota \to P$ a family of points in an affine space over a field $k$. For any predicate $\mathrm{pred} \colon \iota \to \mathrm{Prop}$, if for all $i \in s$ with $w_i \neq 0$ we have $\mathrm{pred}(i)$, then the affine combination over the filtered set $\{x \in s \mid \mathrm{pred}(x)\}$ equals the affine combination over the entire set $s$: \[ \sum_{i \in \{x \in s \mid \mathrm{pred}(x)\}} w_i p_i = \sum_{i \in s} w_i p_i. \]

Finset.map_affineCombination theorem

 {V₂ P₂ : Type*} [AddCommGroup V₂] [Module k V₂] [AffineSpace V₂ P₂] (p : ι → P) (w : ι → k) (hw : s.sum w = 1)
  (f : P →ᵃ[k] P₂) : f (s.affineCombination k p w) = s.affineCombination k (f ∘ p) w

Full source

/-- Affine maps commute with affine combinations. -/
theorem map_affineCombination {V₂ P₂ : Type*} [AddCommGroup V₂] [Module k V₂] [AffineSpace V₂ P₂]
    (p : ι → P) (w : ι → k) (hw : s.sum w = 1) (f : P →ᵃ[k] P₂) :
    f (s.affineCombination k p w) = s.affineCombination k (f ∘ p) w := by
  have b := Classical.choice (inferInstance : AffineSpace V P).nonempty
  have b₂ := Classical.choice (inferInstance : AffineSpace V₂ P₂).nonempty
  rw [s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p hw b,
    s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w (f ∘ p) hw b₂, ←
    s.weightedVSubOfPoint_vadd_eq_of_sum_eq_one w (f ∘ p) hw (f b) b₂]
  simp only [weightedVSubOfPoint_apply, RingHom.id_apply, AffineMap.map_vadd,
    LinearMap.map_smulₛₗ, AffineMap.linearMap_vsub, map_sum, Function.comp_apply]

Affine Maps Preserve Affine Combinations

Informal description

Let $k$ be a ring, $V$ and $P$ be the vector space and affine space over $k$ respectively, and $V_2$, $P_2$ be another pair of vector space and affine space over $k$. Given a finite set of indices $s$, a family of points $p : \iota \to P$, weights $w : \iota \to k$ with $\sum_{i \in s} w_i = 1$, and an affine map $f : P \to P_2$, the image of the affine combination of points under $f$ equals the affine combination of the images of the points under $f$ with the same weights. That is: \[ f\left(\sum_{i \in s} w_i p_i\right) = \sum_{i \in s} w_i f(p_i) \]

Finset.affineCombination_apply_eq_lineMap_sum theorem

 [DecidableEq ι] (w : ι → k) (p : ι → P) (p₁ p₂ : P) (s' : Finset ι) (h : ∑ i ∈ s, w i = 1)
  (hp₂ : ∀ i ∈ s ∩ s', p i = p₂) (hp₁ : ∀ i ∈ s \ s', p i = p₁) :
  s.affineCombination k p w = AffineMap.lineMap p₁ p₂ (∑ i ∈ s ∩ s', w i)

Full source

/-- The value of `affineCombination`, where the given points take only two values. -/
lemma affineCombination_apply_eq_lineMap_sum [DecidableEq ι] (w : ι → k) (p : ι → P)
    (p₁ p₂ : P) (s' : Finset ι) (h : ∑ i ∈ s, w i = 1) (hp₂ : ∀ i ∈ s ∩ s', p i = p₂)
    (hp₁ : ∀ i ∈ s \ s', p i = p₁) :
    s.affineCombination k p w = AffineMap.lineMap p₁ p₂ (∑ i ∈ s ∩ s', w i) := by
  rw [s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p h p₁,
    weightedVSubOfPoint_apply, ← s.sum_inter_add_sum_diff s', AffineMap.lineMap_apply,
    vadd_right_cancel_iff, sum_smul]
  convert add_zero _ with i hi
  · convert Finset.sum_const_zero with i hi
    simp [hp₁ i hi]
  · exact (hp₂ i hi).symm

Affine Combination of Two-Valued Points as Line Map

Informal description

Let $k$ be a ring, $V$ a vector space over $k$, and $P$ an affine space over $V$. Given a finite set of indices $s$, weights $w : \iota \to k$ with $\sum_{i \in s} w_i = 1$, and points $p : \iota \to P$ such that: - For all $i \in s \cap s'$, $p_i = p₂$ - For all $i \in s \setminus s'$, $p_i = p₁$ then the affine combination of the points equals the affine line map between $p₁$ and $p₂$ evaluated at the sum of weights in $s \cap s'$: \[ \sum_{i \in s} w_i p_i = \text{lineMap}_{p₁,p₂}\left(\sum_{i \in s \cap s'} w_i\right) \]

Finset.affineCombinationSingleWeights definition

[DecidableEq ι] (i : ι) : ι → k

Full source

/-- Weights for expressing a single point as an affine combination. -/
def affineCombinationSingleWeights [DecidableEq ι] (i : ι) : ι → k :=
  Pi.single i 1

Single-point affine combination weights

Informal description

For a given index `i` in a type `ι`, the function `affineCombinationSingleWeights` assigns weight 1 to `i` and weight 0 to all other indices. This is used to express a single point as an affine combination where the sum of weights equals 1.

Finset.affineCombinationSingleWeights_apply_self theorem

[DecidableEq ι] (i : ι) : affineCombinationSingleWeights k i i = 1

Full source

@[simp]
theorem affineCombinationSingleWeights_apply_self [DecidableEq ι] (i : ι) :
    affineCombinationSingleWeights k i i = 1 := Pi.single_eq_same _ _

Self-Weight in Single-Point Affine Combination is One

Informal description

For any index $i$ in a type $\iota$, the weight assigned to $i$ in the single-point affine combination is $1$, i.e., $\text{affineCombinationSingleWeights}_k(i, i) = 1$.

Finset.affineCombinationSingleWeights_apply_of_ne theorem

[DecidableEq ι] {i j : ι} (h : j ≠ i) : affineCombinationSingleWeights k i j = 0

Full source

@[simp]
theorem affineCombinationSingleWeights_apply_of_ne [DecidableEq ι] {i j : ι} (h : j ≠ i) :
    affineCombinationSingleWeights k i j = 0 := Pi.single_eq_of_ne h _

Vanishing of Off-Diagonal Weights in Single-Point Affine Combination

Informal description

For any distinct indices $i$ and $j$ in a type $\iota$, the weight assigned to $j$ in the single-point affine combination with base index $i$ is zero, i.e., $\text{affineCombinationSingleWeights}_k(i, j) = 0$.

Finset.sum_affineCombinationSingleWeights theorem

[DecidableEq ι] {i : ι} (h : i ∈ s) : ∑ j ∈ s, affineCombinationSingleWeights k i j = 1

Full source

@[simp]
theorem sum_affineCombinationSingleWeights [DecidableEq ι] {i : ι} (h : i ∈ s) :
    ∑ j ∈ s, affineCombinationSingleWeights k i j = 1 := by
  rw [← affineCombinationSingleWeights_apply_self k i]
  exact sum_eq_single_of_mem i h fun j _ hj => affineCombinationSingleWeights_apply_of_ne k hj

Sum of Single-Point Affine Combination Weights is One

Informal description

For any index $i$ in a finite set $s$ of type $\iota$, the sum of the weights assigned by the single-point affine combination function $\text{affineCombinationSingleWeights}_k(i, \cdot)$ over all elements in $s$ equals $1$. That is, \[ \sum_{j \in s} \text{affineCombinationSingleWeights}_k(i, j) = 1. \]

Finset.weightedVSubVSubWeights definition

[DecidableEq ι] (i j : ι) : ι → k

Full source

/-- Weights for expressing the subtraction of two points as a `weightedVSub`. -/
def weightedVSubVSubWeights [DecidableEq ι] (i j : ι) : ι → k :=
  affineCombinationSingleWeights k i - affineCombinationSingleWeights k j

Weights for vector subtraction of two single-point affine combinations

Informal description

For indices $ i $ and $ j $ in a type $ \iota $, the function `weightedVSubVSubWeights` assigns weights to express the difference between the single-point affine combinations centered at $ i $ and $ j $. Specifically, it is defined as the difference between the weights assigned by `affineCombinationSingleWeights` for $ i $ and $ j $.

Finset.weightedVSubVSubWeights_self theorem

[DecidableEq ι] (i : ι) : weightedVSubVSubWeights k i i = 0

Full source

@[simp]
theorem weightedVSubVSubWeights_self [DecidableEq ι] (i : ι) :
    weightedVSubVSubWeights k i i = 0 := by simp [weightedVSubVSubWeights]

Vanishing Weights for Self-Subtraction in Affine Combinations

Informal description

For any index $i$ in a type $\iota$, the weights assigned by the function $\text{weightedVSubVSubWeights}_k(i, i)$ are identically zero, i.e., $\text{weightedVSubVSubWeights}_k(i, i) = 0$.

Finset.weightedVSubVSubWeights_apply_left theorem

[DecidableEq ι] {i j : ι} (h : i ≠ j) : weightedVSubVSubWeights k i j i = 1

Full source

@[simp]
theorem weightedVSubVSubWeights_apply_left [DecidableEq ι] {i j : ι} (h : i ≠ j) :
    weightedVSubVSubWeights k i j i = 1 := by simp [weightedVSubVSubWeights, h]

Left Weight in Vector Subtraction of Single-Point Affine Combinations is One

Informal description

For any distinct indices $i$ and $j$ in a type $\iota$, the weight assigned to $i$ in the vector subtraction of the single-point affine combinations centered at $i$ and $j$ is $1$, i.e., $\text{weightedVSubVSubWeights}_k(i, j, i) = 1$.

Finset.weightedVSubVSubWeights_apply_right theorem

[DecidableEq ι] {i j : ι} (h : i ≠ j) : weightedVSubVSubWeights k i j j = -1

Full source

@[simp]
theorem weightedVSubVSubWeights_apply_right [DecidableEq ι] {i j : ι} (h : i ≠ j) :
    weightedVSubVSubWeights k i j j = -1 := by simp [weightedVSubVSubWeights, h.symm]

Right Weight in Vector Subtraction of Single-Point Affine Combinations is Negative One

Informal description

For any distinct indices $i$ and $j$ in a type $\iota$, the weight assigned to $j$ in the vector subtraction of the single-point affine combinations centered at $i$ and $j$ is $-1$, i.e., $\text{weightedVSubVSubWeights}_k(i, j, j) = -1$.

Finset.weightedVSubVSubWeights_apply_of_ne theorem

[DecidableEq ι] {i j t : ι} (hi : t ≠ i) (hj : t ≠ j) : weightedVSubVSubWeights k i j t = 0

Full source

@[simp]
theorem weightedVSubVSubWeights_apply_of_ne [DecidableEq ι] {i j t : ι} (hi : t ≠ i) (hj : t ≠ j) :
    weightedVSubVSubWeights k i j t = 0 := by simp [weightedVSubVSubWeights, hi, hj]

Vanishing of Off-Diagonal Weights in Vector Subtraction of Single-Point Affine Combinations

Informal description

For any distinct indices $i$, $j$, and $t$ in a type $\iota$, if $t$ is different from both $i$ and $j$, then the weight assigned to $t$ in the vector subtraction of the single-point affine combinations centered at $i$ and $j$ is zero, i.e., $\text{weightedVSubVSubWeights}_k(i, j, t) = 0$.

Finset.sum_weightedVSubVSubWeights theorem

[DecidableEq ι] {i j : ι} (hi : i ∈ s) (hj : j ∈ s) : ∑ t ∈ s, weightedVSubVSubWeights k i j t = 0

Full source

@[simp]
theorem sum_weightedVSubVSubWeights [DecidableEq ι] {i j : ι} (hi : i ∈ s) (hj : j ∈ s) :
    ∑ t ∈ s, weightedVSubVSubWeights k i j t = 0 := by
  simp_rw [weightedVSubVSubWeights, Pi.sub_apply, sum_sub_distrib]
  simp [hi, hj]

Sum of Vector Subtraction Weights is Zero

Informal description

For any distinct indices $i$ and $j$ in a finite set $s$ of type $\iota$, the sum of the weights assigned by the function $\text{weightedVSubVSubWeights}_k(i, j, \cdot)$ over all elements in $s$ equals $0$. That is, \[ \sum_{t \in s} \text{weightedVSubVSubWeights}_k(i, j, t) = 0. \]

Finset.affineCombinationLineMapWeights definition

[DecidableEq ι] (i j : ι) (c : k) : ι → k

Full source

/-- Weights for expressing `lineMap` as an affine combination. -/
def affineCombinationLineMapWeights [DecidableEq ι] (i j : ι) (c : k) : ι → k :=
  c • weightedVSubVSubWeights k j i + affineCombinationSingleWeights k i

Weights for linear interpolation affine combination

Informal description

For indices $ i $ and $ j $ in a type $ \iota $ and a scalar $ c $ in a field $ k $, the function `affineCombinationLineMapWeights` assigns weights to express the affine combination corresponding to the linear interpolation between points $ i $ and $ j $ with parameter $ c $. Specifically, it is defined as the sum of $ c $ times the weights for the vector subtraction between $ j $ and $ i $, and the weights for the single-point affine combination centered at $ i $.

Finset.affineCombinationLineMapWeights_self theorem

[DecidableEq ι] (i : ι) (c : k) : affineCombinationLineMapWeights i i c = affineCombinationSingleWeights k i

Full source

@[simp]
theorem affineCombinationLineMapWeights_self [DecidableEq ι] (i : ι) (c : k) :
    affineCombinationLineMapWeights i i c = affineCombinationSingleWeights k i := by
  simp [affineCombinationLineMapWeights]

Self-interpolation affine combination weights reduce to single-point weights

Informal description

For any index $i$ in a type $\iota$ and any scalar $c$ in a field $k$, the weights assigned by the affine combination for linear interpolation between $i$ and itself are equal to the weights for the single-point affine combination centered at $i$. That is, \[ \text{affineCombinationLineMapWeights}(i, i, c) = \text{affineCombinationSingleWeights}_k(i). \]

Finset.affineCombinationLineMapWeights_apply_left theorem

[DecidableEq ι] {i j : ι} (h : i ≠ j) (c : k) : affineCombinationLineMapWeights i j c i = 1 - c

Full source

@[simp]
theorem affineCombinationLineMapWeights_apply_left [DecidableEq ι] {i j : ι} (h : i ≠ j) (c : k) :
    affineCombinationLineMapWeights i j c i = 1 - c := by
  simp [affineCombinationLineMapWeights, h.symm, sub_eq_neg_add]

Left weight in linear interpolation affine combination equals $1 - c$

Informal description

For any distinct indices $i$ and $j$ in a type $\iota$ and any scalar $c$ in a field $k$, the weight assigned to $i$ in the affine combination for linear interpolation between $i$ and $j$ is equal to $1 - c$, i.e., $\text{affineCombinationLineMapWeights}(i, j, c)(i) = 1 - c$.

Finset.affineCombinationLineMapWeights_apply_right theorem

[DecidableEq ι] {i j : ι} (h : i ≠ j) (c : k) : affineCombinationLineMapWeights i j c j = c

Full source

@[simp]
theorem affineCombinationLineMapWeights_apply_right [DecidableEq ι] {i j : ι} (h : i ≠ j) (c : k) :
    affineCombinationLineMapWeights i j c j = c := by
  simp [affineCombinationLineMapWeights, h.symm]

Right weight in linear interpolation affine combination equals parameter $c$

Informal description

For any distinct indices $i$ and $j$ in a type $\iota$ and any scalar $c$ in a field $k$, the weight assigned to $j$ in the affine combination for linear interpolation between $i$ and $j$ is equal to $c$, i.e., $\text{affineCombinationLineMapWeights}(i, j, c)(j) = c$.

Finset.affineCombinationLineMapWeights_apply_of_ne theorem

[DecidableEq ι] {i j t : ι} (hi : t ≠ i) (hj : t ≠ j) (c : k) : affineCombinationLineMapWeights i j c t = 0

Full source

@[simp]
theorem affineCombinationLineMapWeights_apply_of_ne [DecidableEq ι] {i j t : ι} (hi : t ≠ i)
    (hj : t ≠ j) (c : k) : affineCombinationLineMapWeights i j c t = 0 := by
  simp [affineCombinationLineMapWeights, hi, hj]

Vanishing of Off-Diagonal Weights in Linear Interpolation Affine Combination

Informal description

For any distinct indices $i$, $j$, and $t$ in a type $\iota$, and any scalar $c$ in a field $k$, if $t$ is different from both $i$ and $j$, then the weight assigned to $t$ in the affine combination for linear interpolation between $i$ and $j$ is zero, i.e., $\text{affineCombinationLineMapWeights}(i, j, c)(t) = 0$.

Finset.sum_affineCombinationLineMapWeights theorem

 [DecidableEq ι] {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (c : k) : ∑ t ∈ s, affineCombinationLineMapWeights i j c t = 1

Full source

@[simp]
theorem sum_affineCombinationLineMapWeights [DecidableEq ι] {i j : ι} (hi : i ∈ s) (hj : j ∈ s)
    (c : k) : ∑ t ∈ s, affineCombinationLineMapWeights i j c t = 1 := by
  simp_rw [affineCombinationLineMapWeights, Pi.add_apply, sum_add_distrib]
  simp [hi, hj, ← mul_sum]

Sum of Linear Interpolation Weights is One

Informal description

For any distinct indices $i$ and $j$ in a finite set $s$ of type $\iota$ and any scalar $c$ in a field $k$, the sum of the weights assigned by the affine combination for linear interpolation between $i$ and $j$ over all elements in $s$ equals $1$. That is, \[ \sum_{t \in s} \text{affineCombinationLineMapWeights}(i, j, c)(t) = 1. \]

Finset.affineCombination_affineCombinationSingleWeights theorem

 [DecidableEq ι] (p : ι → P) {i : ι} (hi : i ∈ s) : s.affineCombination k p (affineCombinationSingleWeights k i) = p i

Full source

/-- An affine combination with `affineCombinationSingleWeights` gives the specified point. -/
@[simp]
theorem affineCombination_affineCombinationSingleWeights [DecidableEq ι] (p : ι → P) {i : ι}
    (hi : i ∈ s) : s.affineCombination k p (affineCombinationSingleWeights k i) = p i := by
  refine s.affineCombination_of_eq_one_of_eq_zero _ _ hi (by simp) ?_
  rintro j - hj
  simp [hj]

Single-Point Affine Combination Yields Corresponding Point

Informal description

Let $s$ be a finite set of indices, $k$ a field, and $p : \iota \to P$ a family of points in an affine space over $k$. For any index $i \in s$, the affine combination of the points $p$ with weights given by the single-point affine combination weights (which assigns weight 1 to $i$ and 0 to all other indices) equals $p_i$, i.e., \[ \sum_{j \in s} (\text{affineCombinationSingleWeights}_k(i))(j) \cdot p_j = p_i. \]

Finset.weightedVSub_weightedVSubVSubWeights theorem

 [DecidableEq ι] (p : ι → P) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) :
  s.weightedVSub p (weightedVSubVSubWeights k i j) = p i -ᵥ p j

Full source

/-- A weighted subtraction with `weightedVSubVSubWeights` gives the result of subtracting the
specified points. -/
@[simp]
theorem weightedVSub_weightedVSubVSubWeights [DecidableEq ι] (p : ι → P) {i j : ι} (hi : i ∈ s)
    (hj : j ∈ s) : s.weightedVSub p (weightedVSubVSubWeights k i j) = p i -ᵥ p j := by
  rw [weightedVSubVSubWeights, ← affineCombination_vsub,
    s.affineCombination_affineCombinationSingleWeights k p hi,
    s.affineCombination_affineCombinationSingleWeights k p hj]

Weighted Vector Subtraction Yields Point Difference in Affine Space

Informal description

For any finite set $s$ of indices and any family of points $p : \iota \to P$ in an affine space over a field $k$, if $i$ and $j$ are distinct indices in $s$, then the weighted vector subtraction of $p$ with weights given by $\text{weightedVSubVSubWeights}(i,j)$ equals the vector difference $p_i - p_j$. That is, \[ \sum_{t \in s} \text{weightedVSubVSubWeights}(i,j)(t) \cdot (p_t - b) = p_i - p_j, \] where $b$ is an arbitrary base point (the result is independent of the choice of $b$).

Finset.affineCombination_affineCombinationLineMapWeights theorem

 [DecidableEq ι] (p : ι → P) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (c : k) :
  s.affineCombination k p (affineCombinationLineMapWeights i j c) = AffineMap.lineMap (p i) (p j) c

Full source

/-- An affine combination with `affineCombinationLineMapWeights` gives the result of
`line_map`. -/
@[simp]
theorem affineCombination_affineCombinationLineMapWeights [DecidableEq ι] (p : ι → P) {i j : ι}
    (hi : i ∈ s) (hj : j ∈ s) (c : k) :
    s.affineCombination k p (affineCombinationLineMapWeights i j c) =
      AffineMap.lineMap (p i) (p j) c := by
  rw [affineCombinationLineMapWeights, ← weightedVSub_vadd_affineCombination,
    weightedVSub_const_smul, s.affineCombination_affineCombinationSingleWeights k p hi,
    s.weightedVSub_weightedVSubVSubWeights k p hj hi, AffineMap.lineMap_apply]

Affine Combination with Line Map Weights Yields Linear Interpolation

Informal description

Let $s$ be a finite set of indices, $k$ a field, and $p : \iota \to P$ a family of points in an affine space over $k$. For any distinct indices $i, j \in s$ and scalar $c \in k$, the affine combination of the points $p$ with weights given by $\text{affineCombinationLineMapWeights}(i,j,c)$ equals the affine line map between $p_i$ and $p_j$ evaluated at $c$, i.e., \[ \sum_{t \in s} w_t \cdot p_t = (1-c) \cdot p_i + c \cdot p_j, \] where $w_t = \text{affineCombinationLineMapWeights}(i,j,c)(t)$.

Finset.centroidWeights definition

: ι → k

Full source

/-- The weights for the centroid of some points. -/
def centroidWeights : ι → k :=
  Function.const ι (#s : k)⁻¹

Centroid weights for a finite set

Informal description

The function assigns to each index $i$ in a finite set $s$ the weight $(|s|)^{-1}$, where $|s|$ denotes the cardinality of $s$ and the inverse is taken in the field $k$. These weights are used to compute the centroid of a family of points.

Finset.centroidWeights_apply theorem

(i : ι) : s.centroidWeights k i = (#s : k)⁻¹

Full source

/-- `centroidWeights` at any point. -/
@[simp]
theorem centroidWeights_apply (i : ι) : s.centroidWeights k i = (#s : k)⁻¹ :=
  rfl

Centroid Weight Formula: $w_i = (|s|)^{-1}$

Informal description

For any index $i$ in a finite set $s$, the centroid weight function evaluated at $i$ is equal to the inverse of the cardinality of $s$ in the field $k$, i.e., $w_i = (|s|)^{-1}$ where $w_i$ is the centroid weight at $i$ and $|s|$ is the cardinality of $s$.

Finset.centroidWeights_eq_const theorem

: s.centroidWeights k = Function.const ι (#s : k)⁻¹

Full source

/-- `centroidWeights` equals a constant function. -/
theorem centroidWeights_eq_const : s.centroidWeights k = Function.const ι (#s : k)⁻¹ :=
  rfl

Centroid Weights as Constant Function

Informal description

The centroid weights function for a finite set $s$ over a field $k$ is equal to the constant function that assigns to each element of $s$ the value $(|s|)^{-1}$, where $|s|$ denotes the cardinality of $s$ and the inverse is taken in $k$.

Finset.sum_centroidWeights_eq_one_of_cast_card_ne_zero theorem

(h : (#s : k) ≠ 0) : ∑ i ∈ s, s.centroidWeights k i = 1

Full source

/-- The weights in the centroid sum to 1, if the number of points,
converted to `k`, is not zero. -/
theorem sum_centroidWeights_eq_one_of_cast_card_ne_zero (h : (#s : k) ≠ 0) :
    ∑ i ∈ s, s.centroidWeights k i = 1 := by simp [h]

Sum of Centroid Weights Equals One When Cardinality is Nonzero in Field

Informal description

Let $s$ be a finite set with cardinality $|s|$, and let $k$ be a field. If the image of $|s|$ in $k$ is nonzero, then the sum of the centroid weights over $s$ equals 1, i.e., \[ \sum_{i \in s} w_i = 1, \] where $w_i = (|s|)^{-1}$ is the centroid weight assigned to each $i \in s$.

Finset.sum_centroidWeights_eq_one_of_card_ne_zero theorem

[CharZero k] (h : #s ≠ 0) : ∑ i ∈ s, s.centroidWeights k i = 1

Full source

/-- In the characteristic zero case, the weights in the centroid sum
to 1 if the number of points is not zero. -/
theorem sum_centroidWeights_eq_one_of_card_ne_zero [CharZero k] (h : #s#s ≠ 0) :
    ∑ i ∈ s, s.centroidWeights k i = 1 := by
  simp_all

Sum of Centroid Weights Equals One for Nonempty Finite Sets in Characteristic Zero

Informal description

Let $k$ be a field of characteristic zero and $s$ be a finite set with cardinality $|s| \neq 0$. Then the sum of the centroid weights over $s$ equals $1$, i.e., \[ \sum_{i \in s} w_i = 1, \] where $w_i = |s|^{-1}$ for each $i \in s$.

Finset.sum_centroidWeights_eq_one_of_nonempty theorem

[CharZero k] (h : s.Nonempty) : ∑ i ∈ s, s.centroidWeights k i = 1

Full source

/-- In the characteristic zero case, the weights in the centroid sum
to 1 if the set is nonempty. -/
theorem sum_centroidWeights_eq_one_of_nonempty [CharZero k] (h : s.Nonempty) :
    ∑ i ∈ s, s.centroidWeights k i = 1 :=
  s.sum_centroidWeights_eq_one_of_card_ne_zero k (ne_of_gt (card_pos.2 h))

Sum of Centroid Weights Equals One for Nonempty Finite Sets in Characteristic Zero

Informal description

Let $k$ be a field of characteristic zero and $s$ be a nonempty finite set. Then the sum of the centroid weights over $s$ equals $1$, i.e., \[ \sum_{i \in s} w_i = 1, \] where $w_i = |s|^{-1}$ for each $i \in s$.

Finset.sum_centroidWeights_eq_one_of_card_eq_add_one theorem

[CharZero k] {n : ℕ} (h : #s = n + 1) : ∑ i ∈ s, s.centroidWeights k i = 1

Full source

/-- In the characteristic zero case, the weights in the centroid sum
to 1 if the number of points is `n + 1`. -/
theorem sum_centroidWeights_eq_one_of_card_eq_add_one [CharZero k] {n : ℕ} (h : #s = n + 1) :
    ∑ i ∈ s, s.centroidWeights k i = 1 :=
  s.sum_centroidWeights_eq_one_of_card_ne_zero k (h.symm ▸ Nat.succ_ne_zero n)

Sum of Centroid Weights Equals One for Sets of Size $n+1$ in Characteristic Zero

Informal description

Let $k$ be a field of characteristic zero and $s$ be a finite set with cardinality $|s| = n + 1$ for some natural number $n$. Then the sum of the centroid weights over $s$ equals $1$, i.e., \[ \sum_{i \in s} w_i = 1, \] where $w_i = |s|^{-1} = (n + 1)^{-1}$ for each $i \in s$.

Finset.centroid definition

(p : ι → P) : P

Full source

/-- 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. -/
def centroid (p : ι → P) : P :=
  s.affineCombination k p (s.centroidWeights k)

Centroid of a finite set of points in an affine space

Informal description

Given a finite set $s$ of indices and a family of points $p : \iota \to P$ in an affine space over a field $k$, the centroid is the point obtained as the affine combination of $p$ with weights $(|s|)^{-1}$ for each index, where $|s|$ is the cardinality of $s$. More precisely, it is defined as $\sum_{i \in s} \frac{1}{|s|} \cdot (p_i - b) + b$ for an arbitrary base point $b \in P$, though the result is independent of the choice of $b$ since the weights sum to 1.

Finset.centroid_def theorem

(p : ι → P) : s.centroid k p = s.affineCombination k p (s.centroidWeights k)

Full source

/-- The definition of the centroid. -/
theorem centroid_def (p : ι → P) : s.centroid k p = s.affineCombination k p (s.centroidWeights k) :=
  rfl

Centroid as Affine Combination with Uniform Weights

Informal description

For a finite set $s$ of indices and a family of points $p : \iota \to P$ in an affine space over a field $k$, the centroid of $p$ over $s$ is equal to the affine combination of $p$ with weights given by the centroid weights of $s$. More precisely, $\text{centroid}_k(s, p) = \text{affineCombination}_k(s, p, w)$, where $w_i = \frac{1}{|s|}$ for each $i \in s$ are the centroid weights.

Finset.centroid_univ theorem

(s : Finset P) : univ.centroid k ((↑) : s → P) = s.centroid k id

Full source

theorem centroid_univ (s : Finset P) : univ.centroid k ((↑) : s → P) = s.centroid k id := by
  rw [centroid, centroid, ← s.attach_affineCombination_coe]
  congr
  ext
  simp

Equality of Centroids under Canonical Embedding and Identity Weights

Informal description

Let $P$ be an affine space over a field $k$, and let $s$ be a finite set of points in $P$. The centroid of the canonical embedding of $s$ into $P$ (considered as a universal finite set) is equal to the centroid of $s$ with the identity weight function. More precisely, for the universal finite set $\text{univ}$ of $s$, we have: \[ \text{centroid}_k(\text{univ}, (p \mapsto p)) = \text{centroid}_k(s, \text{id}) \] where $\text{id}$ is the identity function on $s$.

Finset.centroid_singleton theorem

(p : ι → P) (i : ι) : ({ i } : Finset ι).centroid k p = p i

Full source

/-- The centroid of a single point. -/
@[simp]
theorem centroid_singleton (p : ι → P) (i : ι) : ({i} : Finset ι).centroid k p = p i := by
  simp [centroid_def, affineCombination_apply]

Centroid of a Singleton is the Point Itself

Informal description

For any family of points $p \colon \iota \to P$ in an affine space over a field $k$ and any index $i \in \iota$, the centroid of the single-point set $\{i\}$ with respect to $p$ is equal to $p_i$.

Finset.centroid_pair theorem

 [DecidableEq ι] [Invertible (2 : k)] (p : ι → P) (i₁ i₂ : ι) :
  ({ i₁, i₂ } : Finset ι).centroid k p = (2⁻¹ : k) • (p i₂ -ᵥ p i₁) +ᵥ p i₁

Full source

/-- The centroid of two points, expressed directly as adding a vector
to a point. -/
theorem centroid_pair [DecidableEq ι] [Invertible (2 : k)] (p : ι → P) (i₁ i₂ : ι) :
    ({i₁, i₂} : Finset ι).centroid k p = (2⁻¹ : k) • (p i₂ -ᵥ p i₁) +ᵥ p i₁ := by
  by_cases h : i₁ = i₂
  · simp [h]
  · have hc : (#{i₁, i₂} : k) ≠ 0 := by
      rw [card_insert_of_not_mem (not_mem_singleton.2 h), card_singleton]
      norm_num
      exact Invertible.ne_zero _
    rw [centroid_def,
      affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ _
        (sum_centroidWeights_eq_one_of_cast_card_ne_zero _ hc) (p i₁)]
    simp [h, one_add_one_eq_two]

Centroid of Two Points in an Affine Space

Informal description

Let $k$ be a field where $2$ is invertible, and let $P$ be an affine space over $k$. For any two distinct indices $i_1, i_2$ in $\iota$ and any family of points $p \colon \iota \to P$, the centroid of the pair $\{i_1, i_2\}$ is given by: \[ \frac{1}{2} (p_{i_2} - p_{i_1}) + p_{i_1}, \] where $p_{i_2} - p_{i_1}$ denotes the vector from $p_{i_1}$ to $p_{i_2}$, and $\frac{1}{2}$ is the inverse of $2$ in $k$.

Finset.centroid_pair_fin theorem

[Invertible (2 : k)] (p : Fin 2 → P) : univ.centroid k p = (2⁻¹ : k) • (p 1 -ᵥ p 0) +ᵥ p 0

Full source

/-- The centroid of two points indexed by `Fin 2`, expressed directly
as adding a vector to the first point. -/
theorem centroid_pair_fin [Invertible (2 : k)] (p : Fin 2 → P) :
    univ.centroid k p = (2⁻¹ : k) • (p 1 -ᵥ p 0) +ᵥ p 0 := by
  rw [univ_fin2]
  convert centroid_pair k p 0 1

Centroid of Two Points in Affine Space: $\frac{1}{2}(p_1 - p_0) + p_0$

Informal description

Let $k$ be a field where $2$ is invertible, and let $P$ be an affine space over $k$. For any two points $p_0, p_1$ indexed by $\mathrm{Fin}(2)$, the centroid of the set $\{p_0, p_1\}$ is given by: \[ \frac{1}{2} (p_1 - p_0) + p_0, \] where $p_1 - p_0$ denotes the vector from $p_0$ to $p_1$, and $\frac{1}{2}$ is the inverse of $2$ in $k$.

Finset.centroid_map theorem

(e : ι₂ ↪ ι) (p : ι → P) : (s₂.map e).centroid k p = s₂.centroid k (p ∘ e)

Full source

/-- A centroid, over the image of an embedding, equals a centroid with
the same points and weights over the original `Finset`. -/
theorem centroid_map (e : ι₂ ↪ ι) (p : ι → P) :
    (s₂.map e).centroid k p = s₂.centroid k (p ∘ e) := by
  simp [centroid_def, affineCombination_map, centroidWeights]

Centroid Invariance under Injective Mapping

Informal description

Let $e : \iota_2 \hookrightarrow \iota$ be an injective function and $p : \iota \to P$ a family of points in an affine space over a field $k$. For any finite subset $s_2 \subseteq \iota_2$, the centroid of the points $p$ over the image $e(s_2)$ equals the centroid of the points $p \circ e$ over $s_2$. That is, \[ \text{centroid}(e(s_2), p) = \text{centroid}(s_2, p \circ e) \] where the centroid is computed with weights $(|s|)^{-1}$ for each point in the respective set $s$.

Finset.centroidWeightsIndicator definition

: ι → k

Full source

/-- `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`. -/
def centroidWeightsIndicator : ι → k :=
  Set.indicator (↑s) (s.centroidWeights k)

Indicator function for centroid weights

Informal description

The function `centroidWeightsIndicator` assigns to each index $i$ in a type $\iota$ the weight $(|s|)^{-1}$ if $i$ belongs to the finite set $s$, and $0$ otherwise, where $|s|$ denotes the cardinality of $s$ and the inverse is taken in the field $k$. This indicator function is used to compute the centroid of a subset of points within a larger set.

Finset.centroidWeightsIndicator_def theorem

: s.centroidWeightsIndicator k = Set.indicator (↑s) (s.centroidWeights k)

Full source

/-- The definition of `centroidWeightsIndicator`. -/
theorem centroidWeightsIndicator_def :
    s.centroidWeightsIndicator k = Set.indicator (↑s) (s.centroidWeights k) :=
  rfl

Definition of Centroid Weights Indicator Function

Informal description

For a finite set $s$ with weights in a field $k$, the centroid weights indicator function is equal to the indicator function of the set $s$ applied to the centroid weights of $s$. That is, for each index $i$ in the type $\iota$, the weight is $(|s|)^{-1}$ if $i \in s$ and $0$ otherwise, where $|s|$ denotes the cardinality of $s$.

Finset.sum_centroidWeightsIndicator theorem

[Fintype ι] : ∑ i, s.centroidWeightsIndicator k i = ∑ i ∈ s, s.centroidWeights k i

Full source

/-- The sum of the weights for the centroid indexed by a `Fintype`. -/
theorem sum_centroidWeightsIndicator [Fintype ι] :
    ∑ i, s.centroidWeightsIndicator k i = ∑ i ∈ s, s.centroidWeights k i :=
  sum_indicator_subset _ (subset_univ _)

Sum of Centroid Weight Indicators Equals Sum of Centroid Weights

Informal description

For a finite type $\iota$ and a finite subset $s \subseteq \iota$, the sum of the centroid weight indicators over all elements of $\iota$ equals the sum of the centroid weights over the elements of $s$. That is, \[ \sum_{i \in \iota} w_i = \sum_{i \in s} w_i, \] where $w_i$ is the centroid weight indicator function, defined as $(|s|)^{-1}$ if $i \in s$ and $0$ otherwise, and $|s|$ denotes the cardinality of $s$.

Finset.sum_centroidWeightsIndicator_eq_one_of_card_ne_zero theorem

[CharZero k] [Fintype ι] (h : #s ≠ 0) : ∑ i, s.centroidWeightsIndicator k i = 1

Full source

/-- 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 sum_centroidWeightsIndicator_eq_one_of_card_ne_zero [CharZero k] [Fintype ι]
    (h : #s#s ≠ 0) : ∑ i, s.centroidWeightsIndicator k i = 1 := by
  rw [sum_centroidWeightsIndicator]
  exact s.sum_centroidWeights_eq_one_of_card_ne_zero k h

Sum of Centroid Weight Indicators Equals One for Nonempty Finite Sets in Characteristic Zero

Informal description

Let $k$ be a field of characteristic zero and $\iota$ be a finite type. For any finite subset $s \subseteq \iota$ with nonzero cardinality, the sum of the centroid weight indicators over all elements of $\iota$ equals $1$, i.e., \[ \sum_{i \in \iota} w_i = 1, \] where $w_i = |s|^{-1}$ if $i \in s$ and $0$ otherwise, and $|s|$ denotes the cardinality of $s$.

Finset.sum_centroidWeightsIndicator_eq_one_of_nonempty theorem

[CharZero k] [Fintype ι] (h : s.Nonempty) : ∑ i, s.centroidWeightsIndicator k i = 1

Full source

/-- In the characteristic zero case, the weights in the centroid
indexed by a `Fintype` sum to 1 if the set is nonempty. -/
theorem sum_centroidWeightsIndicator_eq_one_of_nonempty [CharZero k] [Fintype ι] (h : s.Nonempty) :
    ∑ i, s.centroidWeightsIndicator k i = 1 := by
  rw [sum_centroidWeightsIndicator]
  exact s.sum_centroidWeights_eq_one_of_nonempty k h

Sum of Centroid Weight Indicators Equals One for Nonempty Finite Sets in Characteristic Zero

Informal description

Let $k$ be a field of characteristic zero and $\iota$ be a finite type. For any nonempty finite subset $s \subseteq \iota$, the sum of the centroid weight indicators over all elements of $\iota$ equals $1$, i.e., \[ \sum_{i \in \iota} w_i = 1, \] where $w_i = |s|^{-1}$ if $i \in s$ and $0$ otherwise, and $|s|$ denotes the cardinality of $s$.

Finset.sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one theorem

[CharZero k] [Fintype ι] {n : ℕ} (h : #s = n + 1) : ∑ i, s.centroidWeightsIndicator k i = 1

Full source

/-- 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 sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one [CharZero k] [Fintype ι] {n : ℕ}
    (h : #s = n + 1) : ∑ i, s.centroidWeightsIndicator k i = 1 := by
  rw [sum_centroidWeightsIndicator]
  exact s.sum_centroidWeights_eq_one_of_card_eq_add_one k h

Sum of Centroid Weight Indicators Equals One for Sets of Size $n+1$ in Characteristic Zero

Informal description

Let $k$ be a field of characteristic zero, $\iota$ be a finite type, and $s \subseteq \iota$ be a finite subset with cardinality $|s| = n + 1$ for some natural number $n$. Then the sum of the centroid weight indicators over all elements of $\iota$ equals $1$, i.e., \[ \sum_{i \in \iota} w_i = 1, \] where $w_i = (n + 1)^{-1}$ if $i \in s$ and $0$ otherwise.

Finset.centroid_eq_affineCombination_fintype theorem

[Fintype ι] (p : ι → P) : s.centroid k p = univ.affineCombination k p (s.centroidWeightsIndicator k)

Full source

/-- The centroid as an affine combination over a `Fintype`. -/
theorem centroid_eq_affineCombination_fintype [Fintype ι] (p : ι → P) :
    s.centroid k p = univ.affineCombination k p (s.centroidWeightsIndicator k) :=
  affineCombination_indicator_subset _ _ (subset_univ _)

Centroid as Affine Combination Over Finite Type

Informal description

Let $k$ be a ring, $V$ a module over $k$, and $P$ an affine space over $V$. For a finite type $\iota$ and a finite subset $s \subseteq \iota$, the centroid of a family of points $p : \iota \to P$ over $s$ equals the affine combination of $p$ over the universal finite set $\text{univ} \subseteq \iota$ with weights given by the centroid weight indicators of $s$. That is, \[ \text{centroid}(s, p) = \sum_{i \in \iota} w_i p_i, \] where $w_i = |s|^{-1}$ if $i \in s$ and $0$ otherwise, and $|s|$ denotes the cardinality of $s$.

Finset.centroid_eq_centroid_image_of_inj_on theorem

 {p : ι → P} (hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j) {ps : Set P} [Fintype ps] (hps : ps = p '' ↑s) :
  s.centroid k p = (univ : Finset ps).centroid k fun x => (x : P)

Full source

/-- 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 centroid_eq_centroid_image_of_inj_on {p : ι → P}
    (hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j) {ps : Set P} [Fintype ps]
    (hps : ps = p '' ↑s) : s.centroid k p = (univ : Finset ps).centroid k fun x => (x : P) := by
  let f : p '' ↑s → ι := fun x => x.property.choose
  have hf : ∀ x, f x ∈ sf x ∈ s ∧ p (f x) = x := fun x => x.property.choose_spec
  let f' : ps → ι := fun x => f ⟨x, hps ▸ x.property⟩
  have hf' : ∀ x, f' x ∈ sf' x ∈ s ∧ p (f' x) = x := fun x => hf ⟨x, hps ▸ x.property⟩
  have hf'i : Function.Injective f' := by
    intro x y h
    rw [Subtype.ext_iff, ← (hf' x).2, ← (hf' y).2, h]
  let f'e : ps ↪ ι := ⟨f', hf'i⟩
  have hu : Finset.univ.map f'e = s := by
    ext x
    rw [mem_map]
    constructor
    · rintro ⟨i, _, rfl⟩
      exact (hf' i).1
    · intro hx
      use ⟨p x, hps.symm ▸ Set.mem_image_of_mem _ hx⟩, mem_univ _
      refine hi _ (hf' _).1 _ hx ?_
      rw [(hf' _).2]
  rw [← hu, centroid_map]
  congr with x
  change p (f' x) = ↑x
  rw [(hf' x).2]

Centroid Invariance under Injective Mapping to Image Set

Informal description

Let $k$ be a field, $\iota$ a type, and $P$ an affine space over $k$. Given a finite subset $s \subseteq \iota$ and a family of points $p : \iota \to P$ that is injective on $s$ (i.e., for any $i, j \in s$, $p_i = p_j$ implies $i = j$), and given a set $ps \subseteq P$ that is equal to the image of $s$ under $p$ (i.e., $ps = p(s)$), then the centroid of $p$ over $s$ equals the centroid of the inclusion map $\iota : ps \hookrightarrow P$ over the universal finite set of $ps$. In other words, if $p$ is injective on $s$ and $ps$ is the image of $s$ under $p$, then: \[ \text{centroid}(s, p) = \text{centroid}(\text{univ}, \iota) \] where $\text{univ}$ is the universal finite set of $ps$ and $\iota$ is the inclusion of $ps$ into $P$.

Finset.centroid_eq_of_inj_on_of_image_eq theorem

 {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₂) : s.centroid k p = s₂.centroid k p₂

Full source

/-- 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. -/
theorem centroid_eq_of_inj_on_of_image_eq {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₂) :
    s.centroid k p = s₂.centroid k p₂ := by
  classical rw [s.centroid_eq_centroid_image_of_inj_on k hi rfl,
      s₂.centroid_eq_centroid_image_of_inj_on k hi₂ he]

Centroid Equality for Injective Families with Identical Images

Informal description

Let $k$ be a field, $\iota$ and $\iota_2$ be types, and $P$ an affine space over $k$. Given two finite subsets $s \subseteq \iota$ and $s_2 \subseteq \iota_2$, and two families of points $p : \iota \to P$ and $p_2 : \iota_2 \to P$ that are injective on $s$ and $s_2$ respectively (i.e., for any $i, j \in s$, $p_i = p_j$ implies $i = j$, and similarly for $p_2$ on $s_2$), if the images of $s$ and $s_2$ under $p$ and $p_2$ coincide (i.e., $p(s) = p_2(s_2)$), then the centroids of $p$ over $s$ and $p_2$ over $s_2$ are equal: \[ \text{centroid}(s, p) = \text{centroid}(s_2, p_2). \]

weightedVSub_mem_vectorSpan theorem

 {s : Finset ι} {w : ι → k} (h : ∑ i ∈ s, w i = 0) (p : ι → P) : s.weightedVSub p w ∈ vectorSpan k (Set.range p)

Full source

/-- A `weightedVSub` with sum of weights 0 is in the `vectorSpan` of
an indexed family. -/
theorem weightedVSub_mem_vectorSpan {s : Finset ι} {w : ι → k} (h : ∑ i ∈ s, w i = 0)
    (p : ι → P) : s.weightedVSub p w ∈ vectorSpan k (Set.range p) := by
  classical
    rcases isEmpty_or_nonempty ι with (hι | ⟨⟨i0⟩⟩)
    · simp [Finset.eq_empty_of_isEmpty s]
    · rw [vectorSpan_range_eq_span_range_vsub_right k p i0, ← Set.image_univ,
        Finsupp.mem_span_image_iff_linearCombination,
        Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero s w p h (p i0),
        Finset.weightedVSubOfPoint_apply]
      let w' := Set.indicator (↑s) w
      have hwx : ∀ i, w' i ≠ 0 → i ∈ s := fun i => Set.mem_of_indicator_ne_zero
      use Finsupp.onFinset s w' hwx, Set.subset_univ _
      rw [Finsupp.linearCombination_apply, Finsupp.onFinset_sum hwx]
      · apply Finset.sum_congr rfl
        intro i hi
        simp [w', Set.indicator_apply, if_pos hi]
      · exact fun _ => zero_smul k _

Weighted Vector Subtraction with Zero Sum Weights Lies in Vector Span

Informal description

For any finite set $s$ of indices $\iota$, any weights $w \colon \iota \to k$ such that $\sum_{i \in s} w_i = 0$, and any family of points $p \colon \iota \to P$ in an affine space over a vector space $V$, the weighted vector subtraction $\sum_{i \in s} w_i \cdot (p_i - b)$ (where $b$ is an arbitrary base point) lies in the vector span of the range of $p$.

affineCombination_mem_affineSpan theorem

 [Nontrivial k] {s : Finset ι} {w : ι → k} (h : ∑ i ∈ s, w i = 1) (p : ι → P) :
  s.affineCombination k p w ∈ affineSpan k (Set.range p)

Full source

/-- An `affineCombination` with sum of weights 1 is in the
`affineSpan` of an indexed family, if the underlying ring is
nontrivial. -/
theorem affineCombination_mem_affineSpan [Nontrivial k] {s : Finset ι} {w : ι → k}
    (h : ∑ i ∈ s, w i = 1) (p : ι → P) :
    s.affineCombination k p w ∈ affineSpan k (Set.range p) := by
  classical
    have hnz : ∑ i ∈ s, w i∑ i ∈ s, w i ≠ 0 := h.symm ▸ one_ne_zero
    have hn : s.Nonempty := Finset.nonempty_of_sum_ne_zero hnz
    obtain ⟨i1, hi1⟩ := hn
    let w1 : ι → k := Function.update (Function.const ι 0) i1 1
    have hw1 : ∑ i ∈ s, w1 i = 1 := by
      simp only [w1, Function.const_zero, Finset.sum_update_of_mem hi1, Pi.zero_apply,
          Finset.sum_const_zero, add_zero]
    have hw1s : s.affineCombination k p w1 = p i1 :=
      s.affineCombination_of_eq_one_of_eq_zero w1 p hi1 (Function.update_self ..) fun _ _ hne =>
        Function.update_of_ne hne ..
    have hv : s.affineCombination k p w -ᵥ p i1s.affineCombination k p w -ᵥ p i1 ∈ (affineSpan k (Set.range p)).direction := by
      rw [direction_affineSpan, ← hw1s, Finset.affineCombination_vsub]
      apply weightedVSub_mem_vectorSpan
      simp [Pi.sub_apply, h, hw1]
    rw [← vsub_vadd (s.affineCombination k p w) (p i1)]
    exact AffineSubspace.vadd_mem_of_mem_direction hv (mem_affineSpan k (Set.mem_range_self _))

Affine Combination with Sum of Weights 1 Lies in Affine Span

Informal description

Let $k$ be a nontrivial ring, $s$ a finite set of indices, $w \colon \iota \to k$ a weight function with $\sum_{i \in s} w_i = 1$, and $p \colon \iota \to P$ a family of points in an affine space over $k$. Then the affine combination $\sum_{i \in s} w_i p_i$ lies in the affine span of the range of $p$.

mem_vectorSpan_iff_eq_weightedVSub theorem

 {v : V} {p : ι → P} :
  v ∈ vectorSpan k (Set.range p) ↔ ∃ (s : Finset ι) (w : ι → k), ∑ i ∈ s, w i = 0 ∧ v = s.weightedVSub p w

Full source

/-- A vector is in the `vectorSpan` of an indexed family if and only
if it is a `weightedVSub` with sum of weights 0. -/
theorem mem_vectorSpan_iff_eq_weightedVSub {v : V} {p : ι → P} :
    v ∈ vectorSpan k (Set.range p)v ∈ vectorSpan k (Set.range p) ↔
      ∃ (s : Finset ι) (w : ι → k), ∑ i ∈ s, w i = 0 ∧ v = s.weightedVSub p w := by
  classical
    constructor
    · rcases isEmpty_or_nonempty ι with (hι | ⟨⟨i0⟩⟩)
      swap
      · rw [vectorSpan_range_eq_span_range_vsub_right k p i0, ← Set.image_univ,
          Finsupp.mem_span_image_iff_linearCombination]
        rintro ⟨l, _, hv⟩
        use insert i0 l.support
        set w :=
          (l : ι → k) - Function.update (Function.const ι 0 : ι → k) i0 (∑ i ∈ l.support, l i) with
          hwdef
        use w
        have hw : ∑ i ∈ insert i0 l.support, w i = 0 := by
          rw [hwdef]
          simp_rw [Pi.sub_apply, Finset.sum_sub_distrib,
            Finset.sum_update_of_mem (Finset.mem_insert_self _ _),
            Finset.sum_insert_of_eq_zero_if_not_mem Finsupp.not_mem_support_iff.1]
          simp only [Finsupp.mem_support_iff, ne_eq, Finset.mem_insert, true_or, not_true,
            Function.const_apply, Finset.sum_const_zero, add_zero, sub_self]
        use hw
        have hz : w i0 • (p i0 -ᵥ p i0 : V) = 0 := (vsub_self (p i0)).symm ▸ smul_zero _
        change (fun i => w i • (p i -ᵥ p i0 : V)) i0 = 0 at hz
        rw [Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ w p hw (p i0),
          Finset.weightedVSubOfPoint_apply, ← hv, Finsupp.linearCombination_apply,
          @Finset.sum_insert_zero _ _ l.support i0 _ _ _ hz]
        change (∑ i ∈ l.support, l i • _) = _
        congr with i
        by_cases h : i = i0
        · simp [h]
        · simp [hwdef, h]
      · rw [Set.range_eq_empty, vectorSpan_empty, Submodule.mem_bot]
        rintro rfl
        use ∅
        simp
    · rintro ⟨s, w, hw, rfl⟩
      exact weightedVSub_mem_vectorSpan hw p

Characterization of Vectors in the Vector Span via Weighted Subtractions with Zero Sum Weights

Informal description

A vector $v$ in the vector space $V$ associated with an affine space lies in the vector span of the range of a family of points $p : \iota \to P$ if and only if there exists a finite subset $s$ of $\iota$ and a weight function $w : \iota \to k$ such that the sum of weights is zero ($\sum_{i \in s} w_i = 0$) and $v$ equals the weighted vector subtraction $\sum_{i \in s} w_i \cdot (p_i - b)$, where $b$ is an arbitrary base point. In other words: \[ v \in \text{vectorSpan}_k(\text{range } p) \leftrightarrow \exists (s : \text{Finset } \iota) (w : \iota \to k), \sum_{i \in s} w_i = 0 \land v = \sum_{i \in s} w_i \cdot (p_i - b). \]

mem_affineSpan_iff_eq_affineCombination theorem

 [Nontrivial k] {p1 : P} {p : ι → P} :
  p1 ∈ affineSpan k (Set.range p) ↔ ∃ (s : Finset ι) (w : ι → k), ∑ i ∈ s, w i = 1 ∧ p1 = s.affineCombination k p w

Full source

/-- 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_affineCombination [Nontrivial k] {p1 : P} {p : ι → P} :
    p1 ∈ affineSpan k (Set.range p)p1 ∈ affineSpan k (Set.range p) ↔
      ∃ (s : Finset ι) (w : ι → k), ∑ i ∈ s, w i = 1 ∧ p1 = s.affineCombination k p w := by
  constructor
  · exact eq_affineCombination_of_mem_affineSpan
  · rintro ⟨s, w, hw, rfl⟩
    exact affineCombination_mem_affineSpan hw p

Characterization of Points in Affine Span via Affine Combinations

Informal description

Let $k$ be a nontrivial ring, $P$ an affine space over $k$, and $p \colon \iota \to P$ a family of points. A point $p_1 \in P$ lies in the affine span of the range of $p$ if and only if there exists a finite subset $s \subseteq \iota$ and a weight function $w \colon \iota \to k$ such that the sum of weights $\sum_{i \in s} w_i = 1$ and $p_1$ is equal to the affine combination $\sum_{i \in s} w_i p_i$.

mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd theorem

 [Nontrivial k] (p : ι → P) (j : ι) (q : P) :
  q ∈ affineSpan k (Set.range p) ↔ ∃ (s : Finset ι) (w : ι → k), q = s.weightedVSubOfPoint p (p j) w +ᵥ p j

Full source

/-- 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 mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd [Nontrivial k] (p : ι → P) (j : ι) (q : P) :
    q ∈ affineSpan k (Set.range p)q ∈ affineSpan k (Set.range p) ↔
      ∃ (s : Finset ι) (w : ι → k), q = s.weightedVSubOfPoint p (p j) w +ᵥ p j := by
  constructor
  · intro hq
    obtain ⟨s, w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan hq
    exact ⟨s, w, s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p hw (p j)⟩
  · rintro ⟨s, w, rfl⟩
    classical
      let w' : ι → k := Function.update w j (1 - (s \ {j}).sum w)
      have h₁ : (insert j s).sum w' = 1 := by
        by_cases hj : j ∈ s
        · simp [w', Finset.sum_update_of_mem hj, Finset.insert_eq_of_mem hj]
        · simp_rw [w', Finset.sum_insert hj, Finset.sum_update_of_not_mem hj, Function.update_self,
            ← Finset.erase_eq, Finset.erase_eq_of_not_mem hj, sub_add_cancel]
      have hww : ∀ i, i ≠ j → w i = w' i := by
        intro i hij
        simp [w', hij]
      rw [s.weightedVSubOfPoint_eq_of_weights_eq p j w w' hww, ←
        s.weightedVSubOfPoint_insert w' p j, ←
        (insert j s).affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w' p h₁ (p j)]
      exact affineCombination_mem_affineSpan h₁ p

Characterization of Affine Span Membership via Weighted Vector Subtraction

Informal description

Let $k$ be a nontrivial ring, $P$ an affine space over a module $V$ with scalar ring $k$, and $p \colon \iota \to P$ a family of points. For any index $j \in \iota$ and point $q \in P$, the following are equivalent: 1. $q$ lies in the affine span of the range of $p$. 2. There exists a finite set $s \subseteq \iota$ and a weight function $w \colon \iota \to k$ such that \[ q = \sum_{i \in s} w_i \cdot (p_i - p_j) + p_j, \] where $\cdot$ denotes scalar multiplication and $-$ denotes vector subtraction in $V$.

affineSpan_eq_affineSpan_lineMap_units theorem

 [Nontrivial k] {s : Set P} {p : P} (hp : p ∈ s) (w : s → Units k) :
  affineSpan k (Set.range fun q : s => AffineMap.lineMap p ↑q (w q : k)) = affineSpan k s

Full source

/-- 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 affineSpan_eq_affineSpan_lineMap_units [Nontrivial k] {s : Set P} {p : P} (hp : p ∈ s)
    (w : s → Units k) :
    affineSpan k (Set.range fun q : s => AffineMap.lineMap p ↑q (w q : k)) = affineSpan k s := by
  have : s = Set.range ((↑) : s → P) := by simp
  conv_rhs =>
    rw [this]

  apply le_antisymm
    <;> intro q hq
    <;> erw [mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd k V _ (⟨p, hp⟩ : s) q] at hq ⊢
    <;> obtain ⟨t, μ, rfl⟩ := hq
    <;> use t
    <;> [use fun x => μ x * ↑(w x); use fun x => μ x * ↑(w x)⁻¹]
    <;> simp [smul_smul]

Invariance of Affine Span Under Scaled Line Transports from Base Point

Informal description

Let $k$ be a nontrivial ring, $P$ an affine space over $k$, $s \subseteq P$ a set of points, and $p \in s$ a chosen base point. For any function $w \colon s \to k^\times$ assigning an invertible scalar to each point in $s$, the affine span of the set $\{\text{lineMap}(p, q)(w_q) \mid q \in s\}$ (where $\text{lineMap}(p, q)(w_q)$ denotes the point obtained by scaling the vector from $p$ to $q$ by $w_q$ and adding it to $p$) is equal to the affine span of $s$.

centroid_mem_affineSpan_of_cast_card_ne_zero theorem

{s : Finset ι} (p : ι → P) (h : (#s : k) ≠ 0) : s.centroid k p ∈ affineSpan k (range p)

Full source

/-- The centroid lies in the affine span if the number of points,
converted to `k`, is not zero. -/
theorem centroid_mem_affineSpan_of_cast_card_ne_zero {s : Finset ι} (p : ι → P)
    (h : (#s : k) ≠ 0) : s.centroid k p ∈ affineSpan k (range p) :=
  affineCombination_mem_affineSpan (s.sum_centroidWeights_eq_one_of_cast_card_ne_zero h) p

Centroid Lies in Affine Span When Cardinality is Nonzero in Field

Informal description

Let $k$ be a field, $s$ a finite set of indices, and $p \colon \iota \to P$ a family of points in an affine space over $k$. If the cardinality of $s$ is nonzero when interpreted in $k$ (i.e., $|s| \neq 0$ in $k$), then the centroid of the points $p_i$ for $i \in s$ lies in the affine span of the range of $p$.

centroid_mem_affineSpan_of_card_ne_zero theorem

[CharZero k] {s : Finset ι} (p : ι → P) (h : #s ≠ 0) : s.centroid k p ∈ affineSpan k (range p)

Full source

/-- 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_card_ne_zero [CharZero k] {s : Finset ι} (p : ι → P)
    (h : #s#s ≠ 0) : s.centroid k p ∈ affineSpan k (range p) :=
  affineCombination_mem_affineSpan (s.sum_centroidWeights_eq_one_of_card_ne_zero k h) p

Centroid Lies in Affine Span for Nonempty Finite Sets in Characteristic Zero

Informal description

Let $k$ be a field of characteristic zero, $s$ a finite set of indices with cardinality $|s| \neq 0$, and $p \colon \iota \to P$ a family of points in an affine space over $k$. Then the centroid of $p$ over $s$ lies in the affine span of the range of $p$.

centroid_mem_affineSpan_of_nonempty theorem

[CharZero k] {s : Finset ι} (p : ι → P) (h : s.Nonempty) : s.centroid k p ∈ affineSpan k (range p)

Full source

/-- In the characteristic zero case, the centroid lies in the affine
span if the set is nonempty. -/
theorem centroid_mem_affineSpan_of_nonempty [CharZero k] {s : Finset ι} (p : ι → P)
    (h : s.Nonempty) : s.centroid k p ∈ affineSpan k (range p) :=
  affineCombination_mem_affineSpan (s.sum_centroidWeights_eq_one_of_nonempty k h) p

Centroid Lies in Affine Span for Nonempty Sets in Characteristic Zero

Informal description

Let $k$ be a field of characteristic zero, $s$ a nonempty finite set of indices, and $p \colon \iota \to P$ a family of points in an affine space over $k$. Then the centroid of $p$ over $s$ lies in the affine span of the range of $p$.

centroid_mem_affineSpan_of_card_eq_add_one theorem

[CharZero k] {s : Finset ι} (p : ι → P) {n : ℕ} (h : #s = n + 1) : s.centroid k p ∈ affineSpan k (range p)

Full source

/-- In the characteristic zero case, the centroid lies in the affine
span if the number of points is `n + 1`. -/
theorem centroid_mem_affineSpan_of_card_eq_add_one [CharZero k] {s : Finset ι} (p : ι → P) {n : ℕ}
    (h : #s = n + 1) : s.centroid k p ∈ affineSpan k (range p) :=
  affineCombination_mem_affineSpan (s.sum_centroidWeights_eq_one_of_card_eq_add_one k h) p

Centroid in Affine Span for Sets of Size $n+1$ in Characteristic Zero

Informal description

Let $k$ be a field of characteristic zero, $s$ a finite set of indices with cardinality $|s| = n + 1$ for some natural number $n$, and $p \colon \iota \to P$ a family of points in an affine space over $k$. Then the centroid of $p$ over $s$ lies in the affine span of the range of $p$.

AffineMap.weightedVSubOfPoint definition

(w : ι → k) : (ι → P) × P →ᵃ[k] V

Full source

/-- A weighted sum, as an affine map on the points involved. -/
def weightedVSubOfPoint (w : ι → k) : (ι → P) × P(ι → P) × P →ᵃ[k] V where
  toFun p := s.weightedVSubOfPoint p.fst p.snd w
  linear := ∑ i ∈ s, w i • ((LinearMap.proj i).comp (LinearMap.fst _ _ _) - LinearMap.snd _ _ _)
  map_vadd' := by
    rintro ⟨p, b⟩ ⟨v, b'⟩
    simp [LinearMap.sum_apply, Finset.weightedVSubOfPoint, vsub_vadd_eq_vsub_sub,
     vadd_vsub_assoc, add_sub, ← sub_add_eq_add_sub, smul_add, Finset.sum_add_distrib]

Weighted vector subtraction from a base point as an affine map

Informal description

For a finite set $s$ of indices $\iota$, a family of weights $w : \iota \to k$, and a pair consisting of a family of points $p : \iota \to P$ and a base point $b \in P$ in an affine space, the affine map $\text{weightedVSubOfPoint}$ computes the weighted sum $\sum_{i \in s} w_i \cdot (p_i - b)$. Here, $p_i - b$ denotes the vector from $b$ to $p_i$. The linear part of this affine map is given by $\sum_{i \in s} w_i \cdot (\text{proj}_i \circ \text{fst} - \text{snd})$, where $\text{proj}_i$ is the projection onto the $i$-th component, $\text{fst}$ is the first projection, and $\text{snd}$ is the second projection.

Mathlib.LinearAlgebra.AffineSpace.Combination

Main definitions

References