Finset.weightedVSubOfPoint_apply
theorem Finset.weightedVSubOfPoint_apply :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) (b : P),
(s.weightedVSubOfPoint p b) w = s.sum fun i => w i • (p i -ᵥ b)
The theorem `Finset.weightedVSubOfPoint_apply` states that for any types `k`, `V`, `P`, `ι`, given a ring structure on `k`, an additive commutative group structure on `V`, a module structure of `k` over `V`, an additive torsor structure of `V` over `P`, a finite set `s` of elements of type `ι`, a weight function `w` mapping elements of `ι` to `k`, a point function `p` mapping elements of `ι` to `P`, and a reference point `b` of type `P`, the weighted difference of vectors from `b` to points `p i` in `s` according to the weight function `w` is equal to the sum over `s` of the scaled vectors `w i • (p i -ᵥ b)`.
In mathematical terms, $\sum_{i\in s} w(i)\cdot (p(i)-b)$ gives the weighted difference of vectors from `b` to `p i` for each `i` in the finite set `s`, where the scaling of each vector is determined by the function `w`.
More concisely: For any finite set `s`, weight function `w`, additive torsor `P`, point function `p`, module structure `V`, ring `k`, and reference point `b`, the weighted difference of vectors from `b` to `p i` for each `i` in `s`, where the scaling of each vector is determined by `w`, equals the sum over `s` of the scaled vectors `w i • (p i - b)`.
|
Finset.weightedVSubOfPoint_filter_of_ne
theorem Finset.weightedVSubOfPoint_filter_of_ne :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) (b : P) {pred : ι → Prop}
[inst_3 : DecidablePred pred],
(∀ i ∈ s, w i ≠ 0 → pred i) →
((Finset.filter pred s).weightedVSubOfPoint p b) w = (s.weightedVSubOfPoint p b) w
This theorem states that for any types `k`, `V`, `P`, and `ι`, along with a ring structure on `k`, an additive commutative group structure on `V`, a module structure for `k` and `V`, and an additive torsor structure for `V` and `P`, given a finite set `s` of type `ι`, a weight function `w : ι → k`, a point function `p : ι → P`, a base point `b : P`, and a decidable predicate `pred : ι → Prop`, if for all elements `i` in `s`, `w i` is not zero only if `pred i` holds, then the weighted difference of the points in `s` that satisfy `pred` from `b` is the same as the weighted difference of all points in `s` from `b`. Here, the weighted difference is calculated using the weights provided by `w`.
In simpler terms, if the weights of the elements in `s` that do not satisfy `pred` are all zero, the weighted sum over the subset of `s` satisfying `pred` equals the one over the whole set `s`.
More concisely: Given a module `V` over a ring `k` with an additive torsor structure `P`, a finite set `s ⊆ V` with a decidable predicate `pred : ι → Prop`, and weight function `w : ι → k` such that `w i ≠ 0` if and only if `pred i` holds, the weighted difference of elements in `s` satisfying `pred` from a base point equals the weighted difference of all elements in `s`.
|
Finset.affineCombination_linear
theorem Finset.affineCombination_linear :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (p : ι → P),
(Finset.affineCombination k s p).linear = s.weightedVSub p
This theorem states that for any ring `k`, additive commutative group `V`, module formed from `k` and `V`, and an additive torsor `S` formed from `V` and `P`, the linear map corresponding to an 'affine combination' of a finite set `s` and a function `p`, where elements of `s` are mapped to points in `P` by `p`, is equal to the 'weighted difference' over `s` using the same function `p`. In other words, the linear part of an affine combination is the sum of the differences from a chosen point, each weighted by a scalar.
More concisely: For any ring `k`, additive commutative group `V`, module `M = k �oder V`, additive torsor `S` over `V` with structure map `p : S → V`, and finite set `s ⊆ S`, the linear map defined by `x ↦ ∑ i in s (p x i - p x₀)` for some fixed `x₀ ∈ S`, is equal to the affine combination `∑ i in s (λx. (xi - x₀) * c i)` for scalars `c i ∈ k`, where `xi` denotes `p(si)`.
|
Finset.sum_centroidWeights_eq_one_of_nonempty
theorem Finset.sum_centroidWeights_eq_one_of_nonempty :
∀ (k : Type u_1) [inst : DivisionRing k] {ι : Type u_4} (s : Finset ι) [inst_1 : CharZero k],
s.Nonempty → (s.sum fun i => Finset.centroidWeights k s i) = 1
The theorem `Finset.sum_centroidWeights_eq_one_of_nonempty` states that for any division ring `k` of characteristic zero and any nonempty finite set `s`, the sum of the centroid weights for the elements in `s` is equal to one. These centroid weights are defined as the reciprocal of the size of the set. This theorem is specifically for the case where the ring has characteristic zero, which means that it has no nonzero element `n` such that `n*n = 0`.
More concisely: For any division ring of characteristic zero and a nonempty finite set, the sum of the reciprocals of the set's sizes equals one.
|
Finset.weightedVSub_sdiff
theorem Finset.weightedVSub_sdiff :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [inst_3 : DecidableEq ι] {s₂ : Finset ι},
s₂ ⊆ s → ∀ (w : ι → k) (p : ι → P), ((s \ s₂).weightedVSub p) w + (s₂.weightedVSub p) w = (s.weightedVSub p) w
This theorem states that for any type `k` forming a ring, any type `V` forming an additive commutative group, any type `P` acting as an additive torsor over `V`, any type `ι`, a subset `s₂` of a finset `s` of type `ι`, and any two functions `w : ι → k` and `p : ι → P`, with decidable equality on `ι`, the weighted vertical subtraction (`weightedVSub`) over the set difference of `s` and `s₂` and the weighted vertical subtraction over `s₂` sum up to the weighted vertical subtraction over `s`. In other words, a weighted sum over a set can be divided into weighted sums over two disjoint subsets of the original set.
More concisely: For any ring `k`, additive commutative group `V`, additive torsor `P` over `V`, decidable equality `ι`, subset `s₂` of a finset `s` of type `ι`, and functions `w : ι → k` and `p : ι → P`, the weighted vertical subtractions of `s \ s₂` and `s₂` sum up to the weighted vertical subtraction over `s`.
|
Finset.centroid_eq_centroid_image_of_inj_on
theorem Finset.centroid_eq_centroid_image_of_inj_on :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] {ι : Type u_4} (s : Finset ι) {p : ι → P},
(∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j) →
∀ {ps : Set P} [inst_4 : Fintype ↑ps],
ps = p '' ↑s → Finset.centroid k s p = Finset.centroid k Finset.univ fun x => ↑x
This theorem states that if you have an indexed family of points that is injective on a given finite set, then the centroid of those points is the same as the centroid of the image of that finite set. In other words, if you have a mapping that uniquely assigns each element in the finite set with a point, then the average (centroid) of the assigned points is the same whether you consider the set as the indices of the points or as the points themselves. This is expressed under the condition that the set of points is equal to the set of images of the elements in the finite set. This theorem is specifically useful in controlling the definitional equality for the index type used for the centroid of the image.
More concisely: If a function maps a finite set injectively to an indexed family of points, then the centroid of the points is equal to the centroid of the images of the finite set.
|
Finset.affineCombinationSingleWeights_apply_of_ne
theorem Finset.affineCombinationSingleWeights_apply_of_ne :
∀ (k : Type u_1) [inst : Ring k] {ι : Type u_4} [inst_1 : DecidableEq ι] {i j : ι},
j ≠ i → Finset.affineCombinationSingleWeights k i j = 0
The theorem `Finset.affineCombinationSingleWeights_apply_of_ne` states that for any Ring `k` and any type `ι` that has decidable equality, if `i` and `j` are two distinct elements of `ι` (i.e., `j ≠ i`), then the result of applying the `Finset.affineCombinationSingleWeights` function with `k` as the ring, `i` as the first argument and `j` as the second argument is zero. In other words, in the context of affine combinations, if the weight is associated with a point different from the given one, it is zero.
More concisely: For any ring `k` and decidably equal type `ι`, `Finset.affineCombinationSingleWeights _ _ i j` equals zero when `i ≠ j`.
|
Finset.affineCombination_subtype_eq_filter
theorem Finset.affineCombination_subtype_eq_filter :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) (pred : ι → Prop)
[inst_3 : DecidablePred pred],
((Finset.affineCombination k (Finset.subtype pred s) fun i => p ↑i) fun i => w ↑i) =
(Finset.affineCombination k (Finset.filter pred s) p) w
This theorem states that for any ring `k`, any additive commutative group `V`, any module `V` over `k`, an add-torsor `P` of `V`, a finset `s` of elements of type `ι`, weight function `w : ι → k`, position function `p : ι → P`, and a decidable predicate `pred : ι → Prop`, the affine combination over the subtype of `s` that satisfy `pred`, using `p` and `w` to define positions and weights respectively, is equal to the affine combination over the elements of `s` that satisfy `pred`, using `p` and `w` to define positions and weights respectively.
In other words, the result of the affine combination operation does not change whether we first filter the elements satisfying the predicate and then perform the affine combination, or we perform the affine combination on the subtype satisfying the predicate.
More concisely: For any ring `k`, additive commutative group `V`, module `V` over `k`, add-torsor `P` of `V`, finset `s` of `V` satisfying a decidable predicate `pred`, weight function `w : ι → k`, and position function `p : ι → P`, the affine combination over `s` using `p` and `w` for positions and weights is equal to the affine combination over the subtype of `s` satisfying `pred` using the same `p` and `w`.
|
mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd
theorem mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd :
∀ {ι : Type u_1} (k : Type u_2) (V : Type u_3) {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Nontrivial k] (p : ι → P) (j : ι) (q : P),
q ∈ affineSpan k (Set.range p) ↔ ∃ s w, q = (s.weightedVSubOfPoint p (p j)) w +ᵥ p j
This theorem states that for a given family of points (denoted by `p : ι → P`) and a selected base point within that family (denoted by `j : ι`), a point `q : P` is in the affine span of the family of points if and only if there exists a weight function `w` and a scalar `s` such that `q` can be expressed as the sum of the scaled weighted difference of the points from the base point and the base point itself. This identity is written as `q = (s.weightedVSubOfPoint p (p j)) w +ᵥ p j` in the Lean theorem. It is important to note that the weights are not required to sum up to 1.
More concisely: Given a family of points `p : ι → P` and a base point `j : ι`, a point `q : P` lies in the affine span of `p` if and only if there exist weights `w` and a scalar `s` such that `q = s * (∑ (i : ι). w(i) * (p i - p j)) + p j`. (Here, `∑` denotes summation over the index set `ι`.)
|
Finset.weightedVSub_congr
theorem Finset.weightedVSub_congr :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) {w₁ w₂ : ι → k},
(∀ i ∈ s, w₁ i = w₂ i) →
∀ {p₁ p₂ : ι → P}, (∀ i ∈ s, p₁ i = p₂ i) → (s.weightedVSub p₁) w₁ = (s.weightedVSub p₂) w₂
The theorem `Finset.weightedVSub_congr` states that, given any ring `k`, an additive commutative group `V`, a module over `k` and `V`, and an additive torsor `S` over `V` and some space `P`, for any finite set `s` of some type `ι`, and any two mappings `w₁` and `w₂` from `ι` to `k` and `p₁` and `p₂` from `ι` to `P` such that `w₁ i = w₂ i` and `p₁ i = p₂ i` for all `i` in `s`, applying the `weightedVSub` function on `s` with `p₁` and `w₁` yields the same result as applying `weightedVSub` on `s` with `p₂` and `w₂`. In other words, the weighted difference of `p₁` and `p₂` using weights `w₁` and `w₂` is the same if `w₁` equals `w₂` and `p₁` equals `p₂` over the set `s`.
More concisely: Given a ring `k`, an additive commutative group `V`, a `k`-module and `V`-additive torsor `S`, and finite set `s` with elements mapped to the same elements of `P` under functions `p₁` and `p₂`, and `k`-valued functions `w₁` and `w₂` with equal values over `s`, the weighted differences `weightedVSub s p₁ w₁` and `weightedVSub s p₂ w₂` are equal.
|
Finset.affineCombination_affineCombinationSingleWeights
theorem Finset.affineCombination_affineCombinationSingleWeights :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [inst_3 : DecidableEq ι] (p : ι → P) {i : ι},
i ∈ s → (Finset.affineCombination k s p) (Finset.affineCombinationSingleWeights k i) = p i
This theorem states that for any type `k` with a ring structure, a type `V` forming an additive commutative group, a type `P` forming an add-torsor with `V`, a finite set `s` of index type `ι`, and any function `p` mapping `ι` to `P`. Given a decidable equality on `ι` and an `i` in `s`, if we form an affine combination of points in `P` (indexed by elements in `s`) using `Finset.affineCombination` and single weights provided by `Finset.affineCombinationSingleWeights`, we will obtain the point `p i`. In other words, an affine combination with single weights corresponding to an index `i` reproduces the point at `p i`.
More concisely: For any additive commutative group `V` with a ring structure `k`, any add-torsor `P` over `V`, finite set `s` with decidable equality, and function `p : ι → P`, the affine combination using `Finset.affineCombinationSingleWeights` of points `p i` for `i` in `s` equals `p i`.
|
Finset.weightedVSubOfPoint_const_smul
theorem Finset.weightedVSubOfPoint_const_smul :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) (b : P) (c : k),
(s.weightedVSubOfPoint p b) (c • w) = c • (s.weightedVSubOfPoint p b) w
This theorem states that for a given set `s` of elements of type `ι`, a function `w` mapping elements of `ι` to a ring `k`, a function `p` mapping elements of `ι` to a point `P`, a constant point `b`, and a constant multiplier `c` from the ring `k`, the effect of scaling the weights in the `weightedVSubOfPoint` operation by `c` is the same as scaling the entire `weightedVSubOfPoint` operation by `c`. Here, `weightedVSubOfPoint` refers to a certain sum involving vectors and points, `k` is a ring of scalars, `V` is an additive commutative group serving as a space of vectors, and `P` is a torsor for `V`, serving as a space of points.
More concisely: For any set `s` of elements of type `ι`, function `w` mapping elements of `ι` to a ring `k`, function `p` mapping elements of `ι` to a point `P` in a torsor `V` over an additive commutative group `V`, constant point `b` in `V`, and constant multiplier `c` in `k`, the operation `weightedVSubOfPoint b (map c . w) (map c . p)` is equal to the operation `c * weightedVSubOfPoint b w p`.
|
Finset.centroidWeights_eq_const
theorem Finset.centroidWeights_eq_const :
∀ (k : Type u_1) [inst : DivisionRing k] {ι : Type u_4} (s : Finset ι),
Finset.centroidWeights k s = Function.const ι (↑s.card)⁻¹
This theorem states that for any DivisionRing `k` and any type `ι`, the centroid weights of any finite set `s` (which is of type `Finset ι`) is equal to a constant function. More precisely, the centroid weights for any point in the set is given by the reciprocal of the cardinality of the set, i.e., the number of elements in the set. This is essentially saying that in the centroid of a finite set, each point in the set has an equal weight that is the reciprocal of the total number of points.
More concisely: For any DivisionRing `k` and finite set `s` of type `Finset ι`, the centroid weights of `s` is a constant function equal to the reciprocal of its cardinality.
|
Finset.weightedVSubOfPoint_map
theorem Finset.weightedVSubOfPoint_map :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} {ι₂ : Type u_5} (s₂ : Finset ι₂) (e : ι₂ ↪ ι) (w : ι → k) (p : ι → P) (b : P),
((Finset.map e s₂).weightedVSubOfPoint p b) w = (s₂.weightedVSubOfPoint (p ∘ ⇑e) b) (w ∘ ⇑e)
This theorem states that for any ring `k`, additively commutative group `V`, module `V` over `k`, and an additive torsor `S` of `V` with base points `P`, along with types `ι` and `ι₂`, an embedding `e` of `ι₂` into `ι`, a weight function `w` from `ι` to `k`, a point function `p` from `ι` to `P`, and a base point `b` in `P`, the weighted sum of vectors subtracted from `b` (also known as the weighted V sub of point) over the image of the embedding equals the same weighted sum over the original `Finset`. In other words, the result of computing the weighted sum over the image of an embedding `e` remains the same as computing the weighted sum over the original `Finset` but with the point and weight functions composed with `e`.
More concisely: For any ring `k`, additively commutative group `V`, module `V` over `k`, additive torsor `S` with base points `P`, types `ι` and `ι₂`, an embedding `e` of `ι₂` into `ι`, a weight function `w` from `ι` to `k`, a point function `p` from `ι` to `P`, and a base point `b` in `P`, the weighted sum of `w(i) * (p(i) - b)` over `ι` equals the weighted sum of `w(e(j)) * (p(e(j)) - b)` over `ι₂`.
|
Finset.weightedVSub_eq_linear_combination
theorem Finset.weightedVSub_eq_linear_combination :
∀ {k : Type u_1} {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] {ι : Type u_6}
(s : Finset ι) {w : ι → k} {p : ι → V}, s.sum w = 0 → (s.weightedVSub p) w = s.sum fun i => w i • p i
This theorem states that for any ring `k`, additively commutative group `V` and `V` being a module over `k`, along with a finite set `s` indexed by `ι`, a weight function `w` from `ι` to `k`, and a point function `p` from `ι` to `V`, if the sum of the weights is zero, then calculating the `weightedVSub` of `p` by weights `w` over the set `s` is equivalent to calculating the sum of the scaled points `w i • p i` over the set `s`. In other words, viewing a module as an affine space modeled on itself, a 'weightedVSub' operation is simply a linear combination of the points, scaled by the weights.
More concisely: For any ring `k`, additively commutative group `V` being a `k`-module, finite indexed set `ι`, weight function `w : ι → k`, and point function `p : ι → V`, if the sum of the weights `∑ i in ι w i = 0`, then `weightedVSub p w s = ∑ i in s w i • p i`, where `weightedVSub` is the weighted difference of points in `V`, and `•` denotes scalar multiplication in `V`.
|
Finset.affineCombinationSingleWeights_apply_self
theorem Finset.affineCombinationSingleWeights_apply_self :
∀ (k : Type u_1) [inst : Ring k] {ι : Type u_4} [inst_1 : DecidableEq ι] (i : ι),
Finset.affineCombinationSingleWeights k i i = 1
This theorem states that for any type `k` that forms a ring, and any type `ι` with decidable equality, and any element `i` of type ι, the value of the function `affineCombinationSingleWeights` (defined on `k` and `ι`) at `i` is 1. In simpler terms, when the function `affineCombinationSingleWeights` is applied to the same index twice, it always returns 1. This function is used to create a set of weights for an affine combination where all weights are zero except for the weight at a single point `i`, which is 1. In this context, an affine combination is a weighted sum where the weights sum to 1.
More concisely: For any ring type `k` and decidably equal type `ι`, the function `affineCombinationSingleWeights` on `k` and `ι` returns 1 when applied to the same element `i` of type `ι`.
|
Finset.weightedVSubOfPoint_subtype_eq_filter
theorem Finset.weightedVSubOfPoint_subtype_eq_filter :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) (b : P) (pred : ι → Prop)
[inst_3 : DecidablePred pred],
(((Finset.subtype pred s).weightedVSubOfPoint (fun i => p ↑i) b) fun i => w ↑i) =
((Finset.filter pred s).weightedVSubOfPoint p b) w
This theorem states that for any ring `k`, an additive commutative group `V`, a module `k` over `V`, an additive torsor `S` over `V` and `P`, indices `ι`, a finite set `s` of `ι`, a weight function `w` from `ι` to `k`, a point function `p` from `ι` to `P`, a point `b` in `P`, and a decidable predicate `pred` on `ι`, the weighted sum over the subset of `s` where `pred` holds, where each index `i` is replaced by `p ↑i` and `b` is subtracted, and then each result is multiplied by `w ↑i`, is equal to the weighted sum over the elements of `s` for which `pred` holds, where each index is replaced by `p i`, `b` is subtracted, and then each result is multiplied by `w i`. This essentially shows that the operation of taking a weighted sum over a subset of a finite set can be expressed in terms of filtering the set and then taking a weighted sum over the filtered set.
More concisely: For any ring `k`, additive commutative group `V`, module `k` over `V`, additive torsor `S` over `V`, finite set `s` with decidable `ι`, weight function `w`, point function `p`, point `b`, and predicate `pred` on `ι`, the weighted sum over `{i ∈ s | pred i}` with weights `w ↑i` and elements `p ↑i - b` is equal to the weighted sum over `s` with weights `w i` and elements `p i - b`.
|
affineSpan_eq_affineSpan_lineMap_units
theorem affineSpan_eq_affineSpan_lineMap_units :
∀ {k : Type u_2} {V : Type u_3} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] [inst_4 : Nontrivial k] {s : Set P} {p : P},
p ∈ s → ∀ (w : ↑s → kˣ), affineSpan k (Set.range fun q => (AffineMap.lineMap p ↑q) ↑(w q)) = affineSpan k s
This theorem states that for a given set of points, along with a chosen base point in that set, if we affinely transport all other members of the set along the line joining them to this base point, the affine span of the set remains unchanged. Here, the affine transport is performed using the affine map which represents the line between the base point and the other points. The transportation is such that it doesn't change the ring over which the set and the transformations are defined. The proof of this theorem is not provided (as indicated by "sorry").
More concisely: Given a set of points and a base point in the set, the affine spans of the original points and the affinely transported points along the line joining the base point to each point are equal.
|
Finset.sum_smul_vsub_const_eq_weightedVSub
theorem Finset.sum_smul_vsub_const_eq_weightedVSub :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p₁ : ι → P) (p₂ : P),
(s.sum fun i => w i) = 0 → (s.sum fun i => w i • (p₁ i -ᵥ p₂)) = (s.weightedVSub p₁) w
This theorem states that for any Ring `k`, Additive Commutative Group `V`, `Module` structure over `k` and `V`, `AddTorsor` structure over `V` and `P`, and for any type `ι`, given a finset `s` of type `ι`, a function `w` from `ι` to `k`, a function `p₁` from `ι` to `P`, and a point `p₂` of type `P`, if the sum of the weights `w i` for each element `i` in the finset equals zero, then the sum of the scaled differences `(p₁ i -ᵥ p₂)` across the finset, scaled by `w i`, equals the result of applying the weighted subtraction function `s.weightedVSub p₁` to `w`. In simpler terms, the theorem states that if the weights sum to zero, the weighted sum of the differences between points and a constant point is equal to the weighted subtraction of the points.
More concisely: For any ring `k`, Additive Commutative Group `V` with Module and AddTorsor structures over `k`, and `P` an AddTorsor over `V`, if `w : ι → k`, `p₁ : ι → P`, `p₂ : P`, and the sum of `w i` equals zero for all `i` in finset `s`, then the sum of scaled differences `(p₁ i -ᵥ p₂) * w i` equals the weighted subtraction `s.weightedVSub p₁ w`.
|
Finset.weightedVSubOfPoint_sdiff
theorem Finset.weightedVSubOfPoint_sdiff :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [inst_3 : DecidableEq ι] {s₂ : Finset ι},
s₂ ⊆ s →
∀ (w : ι → k) (p : ι → P) (b : P),
((s \ s₂).weightedVSubOfPoint p b) w + (s₂.weightedVSubOfPoint p b) w = (s.weightedVSubOfPoint p b) w
The theorem `Finset.weightedVSubOfPoint_sdiff` states that for any type `k` with a ring structure, a type `V` with an additive commutative group structure and a module structure over `k`, a type `P` equipped with an additive torsor structure over `V`, an index type `ι`, a finset `s` of `ι`, a decidable equality on `ι`, and a subset `s₂` of `s`, for any weighting function `w : ι → k`, and any point mapping function `p : ι → P`, and any point `b : P`, the weighted vector of the difference of `s` and `s₂` from point `b`, plus the weighted vector of `s₂` from point `b`, equals the weighted vector of `s` from point `b`. This essentially means that a weighted sum may be split into such sums over two subsets.
More concisely: For any ring `k`, additive commutative group `V` with a `k`-module structure, additive torsor `P` over `V`, index type `ι` with decidable equality, finset `s` of `ι`, and weighting function `w : ι → k` and point mapping `p : ι → P`: The weighted sum of `s` from point `b : P` is equal to the weighted sum of `s₂` from `b` plus the weighted sum of the complement of `s₂` in `s` from `b`, for any subset `s₂` of `s`.
|
Finset.sum_smul_vsub_eq_weightedVSubOfPoint_sub
theorem Finset.sum_smul_vsub_eq_weightedVSubOfPoint_sub :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p₁ p₂ : ι → P) (b : P),
(s.sum fun i => w i • (p₁ i -ᵥ p₂ i)) = (s.weightedVSubOfPoint p₁ b) w - (s.weightedVSubOfPoint p₂ b) w
This theorem states that for any ring `k`, an additive commutative group `V`, a module `V` over `k`, an additive torsor `V` over a type `P`, a finite set `s` of elements of some type `ι`, a weight function `w` from `ι` to `k`, and two functions `p₁` and `p₂` from `ι` to `P`, and a base point `b` in `P`, the sum over `s` of the scalar multiples of the differences of the images of each element in `s` under `p₁` and `p₂` is equal to the difference of the weighted vectors of `p₁` and `p₂` with respect to `b`, both weighted by `w`. In mathematical terms, it says that $\sum_{i \in s} w(i) \cdot (p_1(i) - p_2(i)) = wVSub(p_1, b) - wVSub(p_2, b)$, where $wVSub$ denotes the weighted vector subtraction.
More concisely: For any ring `k`, additive commutative group `V`, module `V` over `k`, additive torsor `P`, finite set `s`, weight function `w`, and functions `p₁` and `p₂` from `s` to `P`, and base point `b` in `P`, the weighted sum of scalar multiples of differences of images of elements in `s` under `p₁` and `p₂` equals the weighted difference of the images of `p₁` and `p₂` with respect to `b`.
|
Finset.weightedVSubOfPoint_sdiff_sub
theorem Finset.weightedVSubOfPoint_sdiff_sub :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [inst_3 : DecidableEq ι] {s₂ : Finset ι},
s₂ ⊆ s →
∀ (w : ι → k) (p : ι → P) (b : P),
((s \ s₂).weightedVSubOfPoint p b) w - (s₂.weightedVSubOfPoint p b) (-w) = (s.weightedVSubOfPoint p b) w
The theorem `Finset.weightedVSubOfPoint_sdiff_sub` states that for any types `k`, `V`, `P`, and `ι` with `k` a ring, `V` an additive commutative group, `V` a `k`-module, `P` an additive torsor over `V`, and a decidable equality on `ι`; given a finite set `s` of type `ι` and a subset `s₂` of `s`, any weight function `w : ι → k`, any point function `p : ι → P`, and any point `b : P`; the weighted vector subtraction of points `p` from `b` over the set difference `s \ s₂`, minus the negative of the weighted vector subtraction of `p` from `b` over `s₂`, equals the weighted vector subtraction of `p` from `b` over `s`. In other words, a weighted sum over a set can be decomposed into the difference of two weighted sums over two disjoint subsets.
More concisely: For any ring `k`, additive commutative group `V` with `k`-module structure, additive torsor `P` over `V`, decidable equality on index set `ι`, finite set `s` of type `ι`, subset `s₂` of `s`, weight function `w : ι → k`, point function `p : ι → P`, and point `b : P`, the weighted vector subtraction of `p` from `b` over `s \ s₂` equals the difference of the weighted vector subtraction of `p` from `b` over `s` and the negative of the weighted vector subtraction of `p` from `b` over `s₂`.
|
Finset.sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one
theorem Finset.sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one :
∀ (k : Type u_1) [inst : DivisionRing k] {ι : Type u_4} (s : Finset ι) [inst_1 : CharZero k] [inst_2 : Fintype ι]
{n : ℕ}, s.card = n + 1 → (Finset.univ.sum fun i => Finset.centroidWeightsIndicator k s i) = 1
This theorem states that in the context of a division ring `k` which has characteristic zero, given a finite set `s` of type `ι`, if the number of elements in this set `s` is `n + 1` (`s.card = n + 1`), then the sum of the centroid weights (as determined by the `Finset.centroidWeightsIndicator` function) over the universal set (`Finset.univ`) equals 1. This holds true for every possible index `i` in the universal set.
In mathematical terms, it says that ∑_{i ∈ univ} centroidWeightsIndicator(k, s, i) = 1, given |s| = n + 1, where centroidWeightsIndicator is a function that assigns weights to the elements of the set `s` contributing to the calculation of a centroid and 'univ' is the universal set. Here, the universal set refers to a finite set that includes all possible values of a certain type.
More concisely: Given a division ring `k` of characteristic zero and a finite set `s` of cardinality `n+1`, the sum of the centroid weights assigned to every element in the universal set equals 1.
|
Finset.weightedVSub_indicator_subset
theorem Finset.weightedVSub_indicator_subset :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (w : ι → k) (p : ι → P) {s₁ s₂ : Finset ι},
s₁ ⊆ s₂ → (s₁.weightedVSub p) w = (s₂.weightedVSub p) ((↑s₁).indicator w)
This theorem states that in the context of vectors (from a module over a ring), torsors (a group-based mathematical structure), and a finite set, the weighted sum of vectors subtracted from a reference point (weighted V-sub) remains the same even if we change the weight function to an indicator function (a function that takes the value 1 at elements in the subset and 0 elsewhere) and add more points to the set. Specifically, if we have a smaller set `s₁` which is a subset of a larger set `s₂`, the weighted V-sub of `s₁` equals the weighted V-sub of `s₂` when we use the indicator function for `s₁` as the weight function.
More concisely: Given sets `s₁ ⊆ s₂`, and vectors `v` in a module over a ring, the weighted difference of `s₁` and a reference point with respect to the indicator function of `s₁` is equal to the weighted difference of `s₂` and the reference point.
|
Finset.weightedVSubOfPoint_eq_of_sum_eq_zero
theorem Finset.weightedVSubOfPoint_eq_of_sum_eq_zero :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P),
(s.sum fun i => w i) = 0 → ∀ (b₁ b₂ : P), (s.weightedVSubOfPoint p b₁) w = (s.weightedVSubOfPoint p b₂) w
This theorem states that for a given finite set `s` of elements of any type `ι`, a function `w` from `ι` to a ring `k`, and a function `p` from `ι` to an additive torsor `P` over a module of `k`, if the sum of the weights `w i` for all `i` in `s` is zero, then the weighted sum of the vectors `p i - b₁` and `p i - b₂` (where `b₁` and `b₂` are any points in `P`) are equal. In other words, if the weights sum up to zero, the base point used in the weighted sum of vectors does not matter. This is a generalization of the fact from vector geometry that for points with weights summing to zero, the choice of the origin does not change the weighted sum.
More concisely: For any finite set `s` of elements from a type `ι`, functions `w : ι → k` from `s` to a ring `k`, and functions `p : ι → P` from `s` to an additive torsor `P` over a module of `k`, if the sum of `w i` for all `i` in `s` is zero, then the weighted sums of `p i - b` for any `b ∈ P` are equal.
|
centroid_mem_affineSpan_of_nonempty
theorem centroid_mem_affineSpan_of_nonempty :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] {ι : Type u_4} [inst_4 : CharZero k] {s : Finset ι} (p : ι → P),
s.Nonempty → Finset.centroid k s p ∈ affineSpan k (Set.range p)
This theorem states that for any division ring `k` with characteristic zero, any additively commutative group `V`, any module `k` over `V`, any additive torsor `V` over `P`, and any finitely-indexed set of points `s` with mapping `p`, if the set `s` is nonempty, then the centroid of `s` (calculated as the affine combination of the `p` mapping values with the centroid weights of `s`) lies within the smallest affine subspace that contains the range of `p`. In simpler terms, if you have a nonempty set of points, the "center of mass" of these points is contained within the smallest flat space that can contain all of the points.
More concisely: For any division ring `k` of characteristic zero, any additively commutative group `V`, any `k`-module `M` over `V`, any additive torsor `V` over a point `P`, and any nonempty finite set `s` of points in `M` with mapping `p : s → V`, the centroid of `s` lies in the affine subspace spanned by `p[s]`.
|
Finset.affineCombination_apply
theorem Finset.affineCombination_apply :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P),
(Finset.affineCombination k s p) w = (s.weightedVSubOfPoint p (Classical.choice ⋯)) w +ᵥ Classical.choice ⋯
This theorem pertains to an operation called `affineCombination` on finite sets in the context of affine spaces. In essence, it states that for any ring `k`, additive commutative group `V`, `k`-module structure on `V`, and an affine torsor `S` over `V`, along with a finite set `s` of index type `ι`, a weight function `w` mapping indices to elements of `k`, and a point function `p` mapping indices to points in `P`, the result of applying the `affineCombination` operation with these weights and point function corresponds to the result of calculating the weighted difference of the points from a default base point (given by the `Classical.choice` operation), and then adding this difference vector to the default base point. The theorem can be more typically used by first selecting a preferred base point and then applying `weightedVSubOfPoint_apply`.
More concisely: For any ring `k`, additive commutative group `V`, `k`-module structure on `V`, affine torsor `S` over `V`, finite set `s` of indices `ι`, weight function `w` mapping indices to `k`, and point function `p` mapping indices to points in `P`, the `affineCombination` operation on `S` with weights `w` and point function `p` is equal to the weighted difference of the points from a default base point, followed by adding this difference vector to the default base point.
|
centroid_mem_affineSpan_of_cast_card_ne_zero
theorem centroid_mem_affineSpan_of_cast_card_ne_zero :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] {ι : Type u_4} {s : Finset ι} (p : ι → P),
↑s.card ≠ 0 → Finset.centroid k s p ∈ affineSpan k (Set.range p)
This theorem states that if the cardinality (number of elements) of a finite set `s` of indices, when converted to a type `k` (which is a division ring), is not zero, then the centroid of points determined by `s` and a function `p` from these indices to points in an affine space over `k` is contained in the affine span of the range of the function `p`. The affine space is defined over a module `V` and an add-torsor `P`. In other words, the geometric center (centroid) of a non-empty collection of points lies within the smallest affine subspace that contains those points.
More concisely: If `s` is a finite non-empty set of indices, and `p` is a function from `s` to an affine space over a division ring `k` with module `V` and add-torsor `P`, then the centroid of `p(s)` lies in the affine span of `p(s)`.
|
Finset.affineCombination_indicator_subset
theorem Finset.affineCombination_indicator_subset :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (w : ι → k) (p : ι → P) {s₁ s₂ : Finset ι},
s₁ ⊆ s₂ → (Finset.affineCombination k s₁ p) w = (Finset.affineCombination k s₂ p) ((↑s₁).indicator w)
The theorem `Finset.affineCombination_indicator_subset` states that for any two finite sets `s₁` and `s₂` of indices of type `ι`, where `s₁` is a subset of `s₂`, the affine combination of points `p` weighted by `w` over `s₁` is equal to the affine combination of the same points `p` over `s₂` but with weights given by the indicator function of `s₁` applied to `w`. This essentially means that the affine combination is not affected when we extend the set of indices and adjust the weights correspondingly. This is valid in the context where `k` is a ring, `V` is an additive commutative group, `P` is an addTorsor over `V`, i.e., a set on which `V` acts freely and transitively, and `k` acts on `V` as a module.
More concisely: For any sets of indices `s₁ ⊆ s₂` and weight vectors `w : Finset ι → k`, the affine combination of points in `P` over `s₁` with weights `w` is equal to the affine combination of the same points over `s₂` with weights given by the indicator function of `s₁` applied to `w`.
|
Finset.sum_centroidWeightsIndicator_eq_one_of_nonempty
theorem Finset.sum_centroidWeightsIndicator_eq_one_of_nonempty :
∀ (k : Type u_1) [inst : DivisionRing k] {ι : Type u_4} (s : Finset ι) [inst_1 : CharZero k] [inst_2 : Fintype ι],
s.Nonempty → (Finset.univ.sum fun i => Finset.centroidWeightsIndicator k s i) = 1
This theorem states that for any division ring `k` of characteristic zero, any finite set `s` of arbitrary type `ι`, if `s` is nonempty, then the sum of the centroid weights (given by the `Finset.centroidWeightsIndicator` function) over all elements of the universal set `Finset.univ`, which represents all possible elements of type `ι`, is equal to 1. This basically means that in a division ring of characteristic zero, the weights assigned to the elements of any nonempty finite set when calculating the centroid add up to 1.
More concisely: In a division ring of characteristic zero, the sum of centroid weights of any nonempty finite set equals 1.
|
Finset.centroid_pair
theorem Finset.centroid_pair :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] {ι : Type u_4} [inst_4 : DecidableEq ι] [inst_5 : Invertible 2]
(p : ι → P) (i₁ i₂ : ι), Finset.centroid k {i₁, i₂} p = 2⁻¹ • (p i₂ -ᵥ p i₁) +ᵥ p i₁
This theorem, `Finset.centroid_pair`, asserts that for any division ring `k` and types `V` (an additive commutative group), `P` (a torsor for `V`), and `ι` (with decidable equality), given a function `p : ι → P` and two elements `i₁, i₂ : ι`, the centroid of `i₁` and `i₂` with respect to `p` can be expressed directly as adding a scaled vector to a point. This scaled vector is calculated by taking half of the vector from `p i₁` to `p i₂` (denoted by `2⁻¹ • (p i₂ -ᵥ p i₁)`) and adding it to the point `p i₁`. In mathematical terms, it is essentially stating that the centroid of two points is the midpoint of the line segment connecting the two points.
More concisely: Given a division ring `k`, an additive commutative group `V`, a torsor `P` for `V`, and a function `p : ι → P` from a decidably equaliable index type `ι` to `P`, the centroid of `p(i₁)` and `p(i₂)` is equal to `p(i₁) + ½ • (p(i₂) - p(i₁))`.
|
centroid_mem_affineSpan_of_card_ne_zero
theorem centroid_mem_affineSpan_of_card_ne_zero :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] {ι : Type u_4} [inst_4 : CharZero k] {s : Finset ι} (p : ι → P),
s.card ≠ 0 → Finset.centroid k s p ∈ affineSpan k (Set.range p)
This theorem, `centroid_mem_affineSpan_of_card_ne_zero`, states that in a characteristic zero division ring 'k', given a set 's' of indices of non-zero size, a function 'p' from these indices to points 'P' in an affine space with underlying vector space 'V', the centroid of the points determined by 's' and 'p' lies in the affine span of the range of 'p'. In simpler terms, if you have a non-empty set of points in a space, the centroid (or geometric center) of these points is contained within the smallest affine subspace that contains these points.
More concisely: In a characteristic zero division ring, the centroid of a non-empty set of points in an affine space lies in the affine span of those points.
|
Finset.weightedVSub.proof_1
theorem Finset.weightedVSub.proof_1 :
∀ {V : Type u_2} {P : Type u_1} [inst : AddCommGroup V] [S : AddTorsor V P], Nonempty P
This theorem states that for any given type `V` which is an additive commutative group, and any given type `P` which is an additive torsor over `V`, there is at least one non-empty instance of `P`. In other words, if you have a vector space `V` and a point space `P` over `V`, then `P` cannot be empty.
More concisely: For any additive commutative group `V` and an additive torsor `P` over `V`, there exists a non-empty `x : P`.
|
Finset.affineCombination_sdiff_sub
theorem Finset.affineCombination_sdiff_sub :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [inst_3 : DecidableEq ι] {s₂ : Finset ι},
s₂ ⊆ s →
∀ (w : ι → k) (p : ι → P),
(Finset.affineCombination k (s \ s₂) p) w -ᵥ (Finset.affineCombination k s₂ p) (-w) = (s.weightedVSub p) w
This theorem states that for any types `k`, `V`, `P`, and `ι`, where `k` is a ring, `V` is an additive commutative group, `P` is an add-torsor for `V`, and `ι` is a type with decidable equality, given any subset 's₂' of a finite set 's' of type `ι`, any function 'w' from `ι` to `k`, and any function 'p' from `ι` to `P`, the difference between the affine combination of the elements of 's' excluding 's₂' and the affine combination of the elements of 's₂' with weights negated is equal to the weighted sum of the vectors from 'p' over 's'. In mathematical terms, it's expressing the property: $w \sum_{i \in s \setminus s_2} p_i - w \sum_{i \in s_2} -p_i = w \sum_{i \in s} p_i$ for all `i` in `ι`.
More concisely: For any ring `k`, additive commutative group `V`, add-torsor `P` over `V`, and decidable equality type `ι`, given a finite set `s` of type `ι`, a function `w` from `ι` to `k`, and a function `p` from `ι` to `P`, the affine combination of `p` over `s \ s₂` subtracted from the affine combination of `p` over `s₂` with negated weights equals the affine combination of `p` over `s`, where `s₂` is a subset of `s`. In mathematical notation: $w \sum\_{i \in s \setminus s\_2} p\_i - w \sum\_{i \in s\_2} -p\_i = w \sum\_{i \in s} p\_i$.
|
Finset.affineCombination_eq_of_weightedVSub_eq_zero_of_eq_neg_one
theorem Finset.affineCombination_eq_of_weightedVSub_eq_zero_of_eq_neg_one :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) {w : ι → k} {p : ι → P},
(s.weightedVSub p) w = 0 →
∀ {i : ι} [inst_3 : DecidablePred fun x => x ≠ i],
i ∈ s → w i = -1 → (Finset.affineCombination k (Finset.filter (fun x => x ≠ i) s) p) w = p i
The theorem `Finset.affineCombination_eq_of_weightedVSub_eq_zero_of_eq_neg_one` says that given a set `s` of indices of type `ι`, a weight function `w : ι → k` from indices to a ring `k`, and a point function `p : ι → P` from indices to a point in an affine space `P` over a vector space `V`, if the weighted difference of points (computed by `s.weightedVSub p`) using the weights `w` is zero and a particular index `i` in the set `s` has a weight of `-1`, then the point corresponding to `i` is the affine combination of the other points with the given weights. Here, `affineCombination` is computed over the set `s` excluding `i` (obtained by `Finset.filter (fun x => x ≠ i) s`). The `DecidablePred fun x => x ≠ i` is a predicate that decides for each index whether it is different from `i`.
More concisely: Given a set `s` of indices, a weight function `w : ι → k` with a negative weight `-1` for some index `i ∈ s`, and a point function `p : ι → P` from indices to a point in an affine space `P` over a vector space `V`, if the weighted difference of points `s.weightedVSub p` is zero, then the point `p(i)` is the negative of the affine combination of the other points in `s\{i}` with weights `w`.
|
Finset.centroid_def
theorem Finset.centroid_def :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (p : ι → P),
Finset.centroid k s p = (Finset.affineCombination k s p) (Finset.centroidWeights k s)
The theorem `Finset.centroid_def` states that for any division ring `k`, an additive commutative group `V`, a module `V` over `k`, an additive torsor `P` over `V`, and a set `s` of type `ι`, the centroid of a set of points `p` (which is a function from `ι` to `P`) is defined as the affine combination of the points `p` with the weights given by the `centroidWeights` of the set `s`. The weights for the centroid are defined as the inverse of the cardinality of the set `s`. In mathematical terms, the centroid is a kind of weighted average of the points, where each point is assigned an equal weight proportional to the inverse of the number of points.
More concisely: The centroid of a set of points in a module over a division ring is the affine combination of the points with weights equal to the inverse of the cardinality of the set.
|
Finset.affineCombination_apply_const
theorem Finset.affineCombination_apply_const :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : P),
(s.sum fun i => w i) = 1 → (Finset.affineCombination k s fun x => p) w = p
This theorem states that for a given set of points (represented by a finite set `s`), weights function `w`, and a point `p` in an affine space (where the base ring is `k`, the vector space is `V`, and the affine space is `P`), if the sum of the weights is 1, then the affine combination of the points, where each point is equal to `p`, is equal to `p` itself. This essentially encapsulates the property that in an affine combination where all points are the same and the weights sum up to 1, the result will be that same point.
More concisely: For any finite set `s` of points in an affine space over a base ring `k` with vector space `V` and affine space `P`, if points `p` in `P` and weights `w` in `k^s` satisfy the sum of `w` equals 1, then the affine combination of `p` and `w` equals `p`.
|
Finset.weightedVSub_filter_of_ne
theorem Finset.weightedVSub_filter_of_ne :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) {pred : ι → Prop}
[inst_3 : DecidablePred pred],
(∀ i ∈ s, w i ≠ 0 → pred i) → ((Finset.filter pred s).weightedVSub p) w = (s.weightedVSub p) w
The theorem `Finset.weightedVSub_filter_of_ne` states that for any given ring `k`, an additive commutative group `V`, a module over `k` and `V`, and an additive torsor `S` over `V` and `P`, along with a finset `s` of indices of type `ι`, a weight function `w: ι → k`, a point function `p: ι → P` and a decidable predicate `pred`, if all weights `w i` for `i ∈ s` that are non-zero satisfy the predicate `pred`, then the weighted vector subtraction over the filtered finset `s.filter pred` equals the weighted vector subtraction over the entire finset `s`. In other words, the contributions to the weighted sum from elements of `s` that do not satisfy `pred` are zero.
More concisely: If `s` is a finset of indices, `w` is a weight function, `p` is a point function, and `pred` is a decidable predicate such that all non-zero weights `w i` for `i ∈ s` satisfy `pred`, then the weighted vector subtraction over the filtered finset `s.filter pred` equals the weighted vector subtraction over the entire finset `s`.
|
Finset.sum_centroidWeightsIndicator_eq_one_of_card_ne_zero
theorem Finset.sum_centroidWeightsIndicator_eq_one_of_card_ne_zero :
∀ (k : Type u_1) [inst : DivisionRing k] {ι : Type u_4} (s : Finset ι) [inst_1 : CharZero k] [inst_2 : Fintype ι],
s.card ≠ 0 → (Finset.univ.sum fun i => Finset.centroidWeightsIndicator k s i) = 1
This theorem states that, in the case where the characteristic of the division ring `k` is zero, the sum of the weights in the centroid indexed by a `Fintype` equals 1, as long as the number of points in the finite set `s` is not zero. The weights are calculated using the `centroidWeightsIndicator` function which assigns each point in the `Finset` a weight and takes into account all points in the universal set `univ`. This theorem asserts the property that the sum of the weights assigned to each point of the centroid will be equal to 1, given that the set of points is not empty.
More concisely: For a finite set `s` in a division ring `k` of characteristic zero, the sum of the weights assigned by `centroidWeightsIndicator` to each point in the centroid of `s` equals 1.
|
Finset.affineCombination_vsub
theorem Finset.affineCombination_vsub :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w₁ w₂ : ι → k) (p : ι → P),
(Finset.affineCombination k s p) w₁ -ᵥ (Finset.affineCombination k s p) w₂ = (s.weightedVSub p) (w₁ - w₂)
This theorem states that for any set `s` of indices `ι`, any two weight functions `w₁` and `w₂` from the indices to a ring `k`, and any function `p` from the indices to points in an affine space `P` over a vector space `V` (also over `k`), the vector difference between the affine combinations of the points `p` with weights `w₁` and `w₂` respectively, is equal to the weighted vector subtraction of the points `p` with weights given by the difference `w₁ - w₂`. The vector space `V` is presumed to have an addition operation that forms a commutative group, and `P` is an affine space over `V` (i.e., a `V`-torsor).
More concisely: For any set `s` of indices `ι`, any weight functions `w₁, w₂` from `ι` to a ring `k`, and any function `p : ι → P` from indices to points in an affine space `P` over a vector space `V` (both over `k`), the affine combination of `p` with weights `w₁` subtracted from the affine combination of `p` with weights `w₂` is equal to the weighted vector subtraction of the points `p` with weights `w₁ - w₂`.
|
Finset.sum_smul_const_vsub_eq_sub_weightedVSubOfPoint
theorem Finset.sum_smul_const_vsub_eq_sub_weightedVSubOfPoint :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p₂ : ι → P) (p₁ b : P),
(s.sum fun i => w i • (p₁ -ᵥ p₂ i)) = (s.sum fun i => w i) • (p₁ -ᵥ b) - (s.weightedVSubOfPoint p₂ b) w
This theorem states that in a vector space over a ring, for a given finite set of indices, a set of weights, two sets of points, and a base point, the sum of the scaled distances (as vectors) from a constant point to the points determined by the indices, is equal to the difference of the scaled distance from the constant point to the base point and the weighted average distance from the points determined by the indices to the base point. The operation `•` is the scalar multiplication, `-ᵥ` gives the vector from one point to another, and the function `weightedVSubOfPoint` computes a weighted sum of vectors from given points to a base point.
More concisely: For any vector space over a ring, given a finite set of indices, sets of weights and points, and a base point, the sum of the weighted distances from the constant point to the points determined by the indices is equal to the weighted difference between the distance from the constant point to the base point and the average distance from the base point to the points determined by the indices.
|
Finset.weightedVSub_apply_const
theorem Finset.weightedVSub_apply_const :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : P),
(s.sum fun i => w i) = 0 → (s.weightedVSub fun x => p) w = 0
This theorem states that for any given set `s` of indices, a function `w` mapping these indices to weights, and a point `p`, if the sum of the weights is zero, then the value of the weighted subtraction of vectors (`weightedVSub`), where all the vectors are equivalent to point `p`, equals to zero. The space is defined over a ring `k` and a commutative-additive group `V` which is a `k`-module, and the point `p` is in an affine space `P` over `V`.
More concisely: Given a set `s` of indices, a function `w : s → ℝ` of weights, a point `p` in an affine space over a commutative-additive group `V` that is a `k`-module, if the sum of `w` is zero then `∑ i in s (wi * (p - vector i)) = vector.zero`.
|
Finset.centroid_singleton
theorem Finset.centroid_singleton :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] {ι : Type u_4} (p : ι → P) (i : ι),
Finset.centroid k {i} p = p i
The theorem `Finset.centroid_singleton` states that for any Division Ring `k`, an Additive Commutative Group `V`, a Module `k V`, an Additive Torsor `V P`, a type `ι`, and a mapping from `ι` to `P` denoted as `p`, and a single point `i` of type `ι`, the centroid of the singleton set `{i}` under the map `p` is equal to `p i`. In other words, if you have a single point, its centroid (the "center of mass") is the point itself.
More concisely: For any Division Ring `k`, Additive Commutative Group `V`, Module `k V`, Additive Torsor `V P`, type `ι` and mapping `p : ι → P`, the centroid of the singleton set `{i}`, for any `i : ι`, under `p` equals `p i`.
|
Finset.centroid_eq_affineCombination_fintype
theorem Finset.centroid_eq_affineCombination_fintype :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [inst_4 : Fintype ι] (p : ι → P),
Finset.centroid k s p = (Finset.affineCombination k Finset.univ p) (Finset.centroidWeightsIndicator k s)
The theorem `Finset.centroid_eq_affineCombination_fintype` states that for any division ring `k`, add commutative group `V`, module `V` over `k`, affine torsor `P` over `V`, index type `ι`, finite set `s` of type `ι`, and function `p` from `ι` to `P`, the centroid of the set `s` with respect to `p` is equal to the affine combination of the universal set (implied from the assumption that `ι` is a finite type) with respect to `p`, where the weights are given by the centroid weights indicator function applied to `k` and `s`. This theorem provides a computation method for the centroid under the context of an affine space, where the centroid is computed as an affine combination over a finite type.
More concisely: For any division ring `k`, add commutative group `V`, module `V` over `k`, affine torsor `P` over `V`, finite type `ι`, finite set `s` of type `ι`, and function `p` from `ι` to `P`, the centroid of `s` with respect to `p` equals the affine combination of the universal set with respect to `p`, where weights are given by the centroid weights indicator function applied to `k` and `s`.
|
Finset.weightedVSubOfPoint_congr
theorem Finset.weightedVSubOfPoint_congr :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) {w₁ w₂ : ι → k},
(∀ i ∈ s, w₁ i = w₂ i) →
∀ {p₁ p₂ : ι → P},
(∀ i ∈ s, p₁ i = p₂ i) → ∀ (b : P), (s.weightedVSubOfPoint p₁ b) w₁ = (s.weightedVSubOfPoint p₂ b) w₂
The theorem `Finset.weightedVSubOfPoint_congr` states that for any finset `s`, two families of weights `w₁` and `w₂`, and two families of points `p₁` and `p₂` in a space with a ring structure, an additive commutative group structure, a module structure, and an additive torsor structure, if `w₁` and `w₂` are equal on `s` and `p₁` and `p₂` are equal on `s`, then the weighted differences of the points from a base point `b` using `w₁` and `w₂` respectively are also equal. This theorem essentially states that the weighted difference operation is consistent across equal weights and points.
More concisely: For any finset `s`, and families of weights `w₁` and `w₂`, and points `p₁` and `p₂` in a ring-carrying additive abelian group with an additive torsor structure, if `w₁ = w₂` on `s` and `p₁ = p₂` on `s`, then `Finset.weightedVSubOfPoint w₁ b p₁ = Finset.weightedVSubOfPoint w₂ b p₂`.
|
Finset.centroidWeightsIndicator_def
theorem Finset.centroidWeightsIndicator_def :
∀ (k : Type u_1) [inst : DivisionRing k] {ι : Type u_4} (s : Finset ι),
Finset.centroidWeightsIndicator k s = (↑s).indicator (Finset.centroidWeights k s)
The theorem `Finset.centroidWeightsIndicator_def` states that for any division ring `k`, any type `ι`, and any finite set `s` of type `ι`, the weight indicator function for the centroid of the set `s` (given by `Finset.centroidWeightsIndicator k s`) is equal to the indicator function that assigns to each element in `s` the weight for the centroid of `s` (given by `Finset.centroidWeights k s`), and assigns zero to all other elements. In other words, the centroid weight indicator function is an indicator function that extracts the weights assigned to the points of the set for the purpose of computing the centroid, and treats all points not in the set as having zero weight.
More concisely: For any division ring `k` and finite set `s` of type `ι` in Lean 4, the centroid weight indicator function `Finset.centroidWeightsIndicator k s` equals the indicator function assigning the centroid weights of `s` to its elements and zero to all other elements.
|
Finset.sum_centroidWeightsIndicator
theorem Finset.sum_centroidWeightsIndicator :
∀ (k : Type u_1) [inst : DivisionRing k] {ι : Type u_4} (s : Finset ι) [inst_1 : Fintype ι],
(Finset.univ.sum fun i => Finset.centroidWeightsIndicator k s i) = s.sum fun i => Finset.centroidWeights k s i
The theorem `Finset.sum_centroidWeightsIndicator` states that for any division ring `k` and any finite type `ι`, for any finite set `s` of type `ι`, the sum of the centroid weights (given by the function `Finset.centroidWeightsIndicator`) over all elements in the universal set `Finset.univ` is equal to the sum of the centroid weights (given by the function `Finset.centroidWeights`) over the elements of `s` itself. In other words, summing the weights of the centroid of a set where the weights are defined to be zero outside the set is the same as summing the weights of the centroid over the set itself.
More concisely: For any division ring `k` and finite type `ι`, the sum of centroid weights of the universal set `Finset.univ` for elements of type `ι` equals the sum of centroid weights of a finite set `s` of type `ι`.
|
Finset.sum_smul_const_vsub_eq_neg_weightedVSub
theorem Finset.sum_smul_const_vsub_eq_neg_weightedVSub :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p₂ : ι → P) (p₁ : P),
(s.sum fun i => w i) = 0 → (s.sum fun i => w i • (p₁ -ᵥ p₂ i)) = -(s.weightedVSub p₂) w
This theorem states that for a given set of points, if the sum of their assigned weights is zero, then the weighted sum of the vector differences between a constant point and each of the points in the set is equal to the negative of the weighted sum of the vector differences between the points in the set and their corresponding points in another set. Here, a vector difference is the difference between the coordinates of two points. The theorem is formulated within the context of a ring, an additive commutative group, a module, and an additively torsion-free group, which are mathematical structures that provide the necessary operations for the theorem.
More concisely: Given sets of points in a ring with additive commutative group, module, and additively torsion-free group structures, if the weighted sum of the coordinates between a constant point and each point in one set equals the negative of the weighted sum of the coordinates between the corresponding points in another set and their respective points in the first set, then the sum of their assigned weights is zero.
|
Finset.eq_affineCombination_subset_iff_eq_affineCombination_subtype
theorem Finset.eq_affineCombination_subset_iff_eq_affineCombination_subtype :
∀ (k : Type u_1) (V : Type u_2) {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} {p0 : P} {s : Set ι} {p : ι → P},
(∃ fs, ↑fs ⊆ s ∧ ∃ w, (fs.sum fun i => w i) = 1 ∧ p0 = (Finset.affineCombination k fs p) w) ↔
∃ fs w, (fs.sum fun i => w i) = 1 ∧ p0 = (Finset.affineCombination k fs fun i => p ↑i) w
This theorem provides a condition for expressing a point as an affine combination of points from an indexed family. Specifically, given an indexed family of points, a subset of the index type, and a point, the theorem states that the point can be expressed as an affine combination with weights summing to 1 using a `Finset` from the subset if and only if it can be expressed as an affine combination with weights summing to 1 for the corresponding indexed family with the index type being the subtype corresponding to the subset.
More concisely: Given an indexed family of points, a subset of the index type, and a point, the point can be expressed as an affine combination with weights summing to 1 using points from the subset if and only if it can be expressed as an affine combination with weights summing to 1 using the corresponding points from the indexed family with the index type restricted to the subset.
|
Finset.centroid_map
theorem Finset.centroid_map :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] {ι : Type u_4} {ι₂ : Type u_5} (s₂ : Finset ι₂) (e : ι₂ ↪ ι)
(p : ι → P), Finset.centroid k (Finset.map e s₂) p = Finset.centroid k s₂ (p ∘ ⇑e)
This theorem, named `Finset.centroid_map`, states that for any division ring `k`, additively commutative group `V`, module `k V`, and torsor `V P`, and for any types `ι` and `ι₂`, given a finite set `s₂` of type `ι₂`, an embedding `e` from `ι₂` to `ι`, and a function `p` from `ι` to `P`, the centroid of the image of the finite set under the embedding (calculated using `Finset.centroid k (Finset.map e s₂) p`) is equal to the centroid of the original finite set (calculated using `Finset.centroid k s₂ (p ∘ ⇑e)`). In other words, the process of calculating the centroid commutes with the process of applying an embedding to a finite set.
More concisely: For any division ring `k`, additively commutative group `V`, module `k V`, torsor `P`, types `ι` and `ι₂`, finite set `s₂` of type `ι₂`, embedding `e` from `ι₂` to `ι`, and function `p` from `ι` to `P`, the centroid of `Finset.map e s₂` under `p` equals the centroid of `s₂` under `p ∘ ⇑e`.
|
Finset.weightedVSubOfPoint_erase
theorem Finset.weightedVSubOfPoint_erase :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [inst_3 : DecidableEq ι] (w : ι → k) (p : ι → P) (i : ι),
((s.erase i).weightedVSubOfPoint p (p i)) w = (s.weightedVSubOfPoint p (p i)) w
This theorem, titled "Finset.weightedVSubOfPoint_erase", states that for any set of points in a vector space over a field (or more generally, a module over a ring), the weighted sum of the vectors subtracted from a given base point is unchanged even if the base point itself is removed from the set of points. Specifically, given a ring `k`, an additive commutative group `V`, a `k`-module structure on `V`, an additively translatable structure `S` on `V` and `P`, a finite set `s` of indices of type `ι` (with decidable equality), a weight function `w` from `ι` to `k`, and a point function `p` from `ι` to `P`, and an index `i` of type `ι`, the weighted sum of vectors subtracted from point `p i` remains the same whether or not index `i` is included in the set `s`.
More concisely: For any ring `k`, `k`-module `V` over a vector space, additively translatable structure `S` on `V`, finite set `s` of indices `ι` with decidable equality, weight function `w` from `ι` to `k`, and point function `p` from `ι` to a point `P` in `V`, the weighted sum of subtracting vectors from points `p i` in `s` is equal to the weighted sum of subtracting vectors from the same points excluding index `i`.
|
Finset.affineCombination_eq_linear_combination
theorem Finset.affineCombination_eq_linear_combination :
∀ {k : Type u_1} {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] {ι : Type u_4}
(s : Finset ι) (p : ι → V) (w : ι → k),
(s.sum fun i => w i) = 1 → (Finset.affineCombination k s p) w = s.sum fun i => w i • p i
This theorem states that for any ring `k`, additively commutative group `V`, and module structure on `V` over `k`, given an indexed set `s` in some index type `ι`, a function `p` mapping indices to `V`, and a function `w` mapping indices to `k`, if the sum of the `w` values over the set `s` equals 1, then the affine combination of `s` with coefficients given by `w` equals the sum of the scalar multiples of each `p` value by its corresponding `w` value. In simpler terms, it says that when viewing a module as an affine space modelled on itself, affine combinations are actually just linear combinations.
More concisely: For any ring `k`, additively commutative group `V` with a `k`-module structure, indexed set `s` in some type `ι`, functions `p : ι → V`, and `w : ι → k` with sum equal to 1, the affine combination of `s` with coefficients `w` equals the sum of the scalar multiples of each `p(i)` by `w(i)`.
|
Finset.sum_smul_vsub_const_eq_weightedVSubOfPoint_sub
theorem Finset.sum_smul_vsub_const_eq_weightedVSubOfPoint_sub :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p₁ : ι → P) (p₂ b : P),
(s.sum fun i => w i • (p₁ i -ᵥ p₂)) = (s.weightedVSubOfPoint p₁ b) w - (s.sum fun i => w i) • (p₂ -ᵥ b)
This theorem states that for a finite set of indices, a given weight function, a function mapping indices to points, and two given points, the sum of the products of the weights and the vector difference between the point mapped from the index and a constant point, is equal to the difference between the weighted sum of vector differences from the points mapped from the indices to another fixed point, and the product of the sum of the weights and the vector difference between the constant point and the other fixed point. This result holds in a context where we have a ring of scalars, an additive commutative group, and a module structure over the group, and the points form an affine space over the group.
More concisely: For a finite set of indices, a weight function, a function mapping indices to points in an affine space over a ring of scalars with module structure, and two fixed points, the sum of the weighted vector differences from the constant point to the points mapped from the indices is equal to the weighted sum of vector differences between the points mapped from the indices and the other fixed point, minus the product of the sum of the weights and the vector difference between the constant point and the other fixed point.
|
Finset.weightedVSub_sdiff_sub
theorem Finset.weightedVSub_sdiff_sub :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [inst_3 : DecidableEq ι] {s₂ : Finset ι},
s₂ ⊆ s →
∀ (w : ι → k) (p : ι → P), ((s \ s₂).weightedVSub p) w - (s₂.weightedVSub p) (-w) = (s.weightedVSub p) w
This theorem, `Finset.weightedVSub_sdiff_sub`, states that for any types `k`, `V`, `P`, and `ι`, given a ring structure on `k`, an additive commutative group structure on `V`, a module structure of `k` on `V`, and an additive torsor structure of `V` on `P`. If we have a finite set `s` of elements of type `ι`, and if type `ι` has decidable equality, then for any subset `s₂` of `s`, any function `w` from `ι` to `k`, and any function `p` from `ι` to `P`, the difference between the weighted sum over the set difference `s \ s₂` and the negated weighted sum over `s₂` is equal to the weighted sum over `s`. This essentially describes a distributive property of the weighted sum operation over finite sets with respect to set difference.
More concisely: For any type `ι` with decidable equality, given a ring `k`, an additive commutative group `V` with a module structure over `k`, and an additive torsor `P` over `V`, the weighted sum of a function `w` over the set difference of a finite set `s` and a subset `s₂` equals the weighted sum over `s` minus the negated weighted sum over `s₂`.
|
Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero
theorem Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P),
(s.sum fun i => w i) = 0 → ∀ (b : P), (s.weightedVSub p) w = (s.weightedVSubOfPoint p b) w
This theorem states that for any type of scalars `k`, vector space `V`, and affine space `P` (with `V` as the associated vector space), given a set of indices `s`, a weight function `w` assigning a scalar to each index, and a point function `p` assigning a point to each index, if the sum of all weights is zero, then the weighted subtraction of points from the `p` function is equivalent to the weighted subtraction of points from `p` relative to any base point `b`.
More concisely: For any vector space `V`, affine space `P` with associated vector space `V`, set of indices `s`, weight function `w` assigning scalars to indices, point function `p` assigning points to indices, and base point `b`, if the sum of `w` is zero, then the weighted subtraction of `p` from itself is equivalent to the subtraction of `p` from each point and the scalar multiplication of the base point by the corresponding weight.
|
Finset.weightedVSubOfPoint_indicator_subset
theorem Finset.weightedVSubOfPoint_indicator_subset :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (w : ι → k) (p : ι → P) (b : P) {s₁ s₂ : Finset ι},
s₁ ⊆ s₂ → (s₁.weightedVSubOfPoint p b) w = (s₂.weightedVSubOfPoint p b) ((↑s₁).indicator w)
This theorem states that for any given types `k` (ring), `V` (additive commutative group), `P` (module over the ring `k`), and `ι` (index set), and any given functions `w: ι → k` (weights), `p: ι → P` (points), and a point `b: P`, along with two finite sets `s₁` and `s₂` of type `ι`, if `s₁` is a subset of `s₂`, then the weighted sum (with weights `w`) of the vectors from point `b` to points `p` over the set `s₁` is equal to the weighted sum over the set `s₂` where the weights are specified by the indicator function of `s₁` times `w`. In other words, changing the weights to their corresponding indicator function and adding points to the set do not affect the weighted sum.
More concisely: For any ring `k`, additive commutative group `V`, module `P` over `k`, index set `ι`, functions `w: ι → k` and `p: ι → P`, and point `b: P`, if `s₁` is a subset of `s₂` in `ι`, then the weighted sum of `b-p(i)` with weights `w(i)` over `i` in `s₁` equals the weighted sum over `i` in `s₂` with weights `1_{s₁}(i) * w(i)`.
|
Finset.sum_smul_vsub_eq_affineCombination_vsub
theorem Finset.sum_smul_vsub_eq_affineCombination_vsub :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p₁ p₂ : ι → P),
(s.sum fun i => w i • (p₁ i -ᵥ p₂ i)) =
(Finset.affineCombination k s p₁) w -ᵥ (Finset.affineCombination k s p₂) w
This theorem states that for any ring `k`, additively commutative group `V`, module `V` over `k`, and an additive torsor `S` over `V` and `P`, along with a finite set `s` of type `ι`, a function `w` from `ι` to `k`, and two point functions `p₁` and `p₂` from `ι` to `P`, the weighted sum of difference between corresponding points in `p₁` and `p₂`, given by `(s.sum fun i => w i • (p₁ i -ᵥ p₂ i))`, is equal to the difference of the affine combinations of `p₁` and `p₂` using the same weights `w`, given by `(Finset.affineCombination k s p₁) w -ᵥ (Finset.affineCombination k s p₂) w`. In simpler terms, it describes a relationship between a weighted sum of pairwise subtractions and a subtraction of two affine combinations.
More concisely: For any ring `k`, additively commutative group `V`, module `V` over `k`, additive torsor `S` over `V` and `P`, finite set `s` of type `ι`, function `w` from `ι` to `k`, and point functions `p₁` and `p₂` from `ι` to `P`, the weighted sum of differences between corresponding points in `p₁` and `p₂` is equal to the difference of their affine combinations with the same weights.
|
Finset.centroid_pair_fin
theorem Finset.centroid_pair_fin :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Invertible 2] (p : Fin 2 → P),
Finset.centroid k Finset.univ p = 2⁻¹ • (p 1 -ᵥ p 0) +ᵥ p 0
This theorem states that given any division ring `k`, an additive commutative group `V`, a type `P` that forms an affine space with `V`, and a mapping `p` from a finite set of cardinality 2 to `P`, the centroid of the image of this mapping is equal to the midpoint of the two points in `P` that are the images of the elements of the finite set. In other words, the centroid of any two points in an affine space is just the average (midpoint) of those two points.
More concisely: Given a division ring `k`, an additive commutative group `V` forming an affine space `P`, and a mapping `p` from a finite set of cardinality 2 to `P`, the centroid of the image of `p` equals the midpoint of `p`'s two images in `P`.
|
Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one
theorem Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P),
(s.sum fun i => w i) = 1 → ∀ (b : P), (Finset.affineCombination k s p) w = (s.weightedVSubOfPoint p b) w +ᵥ b
The theorem `Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one` states that for any base point `b`, the affine combination of a set of points `p` with weights `w`, provided by the function `Finset.affineCombination`, equals the vector addition of `b` and the weighted difference of points `p` and `b`, provided by the function `Finset.weightedVSubOfPoint`, when the sum of the weights `w` is equal to 1. Here, `s` is a finite set of indices, `ι` is the index type, `k` is the scalar field (which forms a ring), `V` is a commutative group under addition, `P` is a space equipped with a distinguished point (an affine space), and `S` is an additively translatable point in `P`.
More concisely: For any finite set of points `p` in an affine space `P` with weights `w` summing to 1 in a scalar field `k`, the affine combination of `p` with weights `w` is equal to the point in `P` obtained by vector adding the base point `b` to the weighted difference of `p` and `b`.
|
weightedVSub_mem_vectorSpan
theorem weightedVSub_mem_vectorSpan :
∀ {ι : Type u_1} {k : Type u_2} {V : Type u_3} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] {s : Finset ι} {w : ι → k},
(s.sum fun i => w i) = 0 → ∀ (p : ι → P), (s.weightedVSub p) w ∈ vectorSpan k (Set.range p)
The theorem `weightedVSub_mem_vectorSpan` states that for any index set `ι`, field `k`, additive commutative group `V`, torsor `P` over `V`, finite set `s` within `ι`, and weight function `w` mapping elements of `ι` to `k`, if the sum of weights given by `w` over all elements of `s` equals zero, then for any function `p` mapping elements of `ι` to `P`, the weighted difference (given by `s.weightedVSub p w`) belongs to the vector span (given by `vectorSpan k (Set.range p)`), where the vector span is defined as the submodule spanning the differences of a (possibly empty) set of points and the range of a function is the set of all possible output values.
More concisely: If the weighted sum of elements in a finite subset of an index set is zero, then the weighted difference of a function's values at those elements lies in the vector space spanned by the function's outputs.
|
Finset.weightedVSub_map
theorem Finset.weightedVSub_map :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} {ι₂ : Type u_5} (s₂ : Finset ι₂) (e : ι₂ ↪ ι) (w : ι → k) (p : ι → P),
((Finset.map e s₂).weightedVSub p) w = (s₂.weightedVSub (p ∘ ⇑e)) (w ∘ ⇑e)
This theorem states that for any ring `k`, additively commutative group `V`, and module `V` over `k`, and given a set `s₂` of type `ι₂`, an embedding `e` from `ι₂` to `ι`, a weight function `w` from `ι` to `k`, and a point function `p` from `ι` to `P`, the weighted subtraction computed over the image of the set `s₂` under the embedding `e` is equal to the weighted subtraction computed over the original set `s₂`, with the weight and point functions composed with the embedding `e`. In mathematical terms, this can be expressed as ∀s₂,e,w,p, ((s₂.map e).weightedVSub p) w = (s₂.weightedVSub (p ∘ e)) (w ∘ e), where ∘ denotes function composition.
More concisely: For any ring `k`, additively commutative group `V`, module `V` over `k`, set `s₂`, embedding `e` from `ι₂` to `ι`, weight function `w` from `ι` to `k`, and point function `p` from `ι` to `P`, the weighted subtraction of `s₂` with respect to `p` and `w` is equal to the weighted subtraction of the image of `s₂` under `e` with respect to `p` composed with `e` and `w` composed with `e`.
|
eq_affineCombination_of_mem_affineSpan
theorem eq_affineCombination_of_mem_affineSpan :
∀ {ι : Type u_1} {k : Type u_2} {V : Type u_3} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] {p1 : P} {p : ι → P},
p1 ∈ affineSpan k (Set.range p) → ∃ s w, (s.sum fun i => w i) = 1 ∧ p1 = (Finset.affineCombination k s p) w
This theorem states that for any point `p1` in the affine span of an indexed family `p` of points in an affine space over a ring `k`, with the associated vector space `V` and an additively torsion-free type `P`, there exists a finite set of indices `s` and a weight function `w` such that the sum of the weights is 1 and `p1` is the affine combination of the points indexed by `s` with weights given by `w`. In other words, `p1` can be expressed as an affine combination of the points in `p`, and the weights of this combination sum to 1.
More concisely: Given an indexed family `p` of points in an affine space over a ring `k` with associated vector space `V` and an additively torsion-free type `P`, for any point `p1` in the affine span of `p`, there exist a finite set of indices `s` and weights `w` summing to 1 such that `p1` is the affine combination of the points indexed by `s` with weights `w`.
|
Finset.sum_centroidWeights_eq_one_of_cast_card_ne_zero
theorem Finset.sum_centroidWeights_eq_one_of_cast_card_ne_zero :
∀ {k : Type u_1} [inst : DivisionRing k] {ι : Type u_4} (s : Finset ι),
↑s.card ≠ 0 → (s.sum fun i => Finset.centroidWeights k s i) = 1
This theorem states that for any division ring `k` and set `s` of type `ι`, if the cardinality of `s` is not zero when converted to `k`, then the sum of the centroid weights of `s` is equal to 1. In other words, if we have a non-empty set of points, then the weights assigned to these points (which are inversely proportional to the number of points) will always sum up to 1. This corresponds to the mathematical concept of the centroid, where the weights of all points in a geometric shape sum to one.
More concisely: For any division ring `k` and non-empty set `s` of cardinality `n` in `k`, the sum of the centroid weights of `s` equals 1, i.e., `∑ (w : s) w.weight = 1`.
|
Finset.sum_smul_vsub_const_eq_affineCombination_vsub
theorem Finset.sum_smul_vsub_const_eq_affineCombination_vsub :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p₁ : ι → P) (p₂ : P),
(s.sum fun i => w i) = 1 → (s.sum fun i => w i • (p₁ i -ᵥ p₂)) = (Finset.affineCombination k s p₁) w -ᵥ p₂
This theorem states that for a given set of points and weights in an affine space, where the sum of the weights equals 1, the weighted sum of the pairwise differences between each point and a constant point is equal to the difference between the affine combination of the points with the given weights and the constant point. Here, the weights and the points are elements of a ring and an affine torsor respectively, and the subtraction operation denotes the difference between two points in an affine space.
More concisely: For any set of points and weights in an affine space over a ring with the property that the sum of the weights equals 1, the weighted sum of pairwise differences between points and a constant point equals the difference between the affine combination of the points with the given weights and the constant point.
|
Finset.weightedVSubOfPoint_vadd_eq_of_sum_eq_one
theorem Finset.weightedVSubOfPoint_vadd_eq_of_sum_eq_one :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P),
(s.sum fun i => w i) = 1 →
∀ (b₁ b₂ : P), (s.weightedVSubOfPoint p b₁) w +ᵥ b₁ = (s.weightedVSubOfPoint p b₂) w +ᵥ b₂
This theorem states that in a vector space over a ring, given a finite set of points and a set of weights such that the sum of the weights equals to 1, the sum of weighted differences between the points and a base point, when added to the base point, doesn't depend on the base point. Specifically, for two different base points, the sum of the weighted differences from the first base point, when added to the first base point, is equal to the sum of the weighted differences from the second base point, when added to the second base point.
More concisely: Given a vector space over a ring, for any finite set of points, weights summing to 1, and base points, the sum of weighted differences between points and one base point equals the sum of weighted differences between the same points and the other base point.
|
Finset.weightedVSubOfPoint_insert
theorem Finset.weightedVSubOfPoint_insert :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [inst_3 : DecidableEq ι] (w : ι → k) (p : ι → P) (i : ι),
((insert i s).weightedVSubOfPoint p (p i)) w = (s.weightedVSubOfPoint p (p i)) w
This theorem states that for any base point `i`, the weighted difference from the base point of a set of points `s` (expressed as `(s.weightedVSubOfPoint p (p i)) w`), is the same as the weighted difference from the base point of the set of points obtained by adding the base point to `s` (expressed as `(insert i s).weightedVSubOfPoint p (p i)) w`).
This holds for any type `k` with a ring structure, any type `V` that forms an additive commutative group, any `P` that forms an AddTorsor with `V`, any finset `s` of points of type `ι`, and any functions `w` and `p` mapping from `ι` to `k` and `P` respectively. The equality of elements of type `ι` is assumed to be decidable.
More concisely: For any type `k` with a ring structure, any type `V` forming an additive commutative group, any AddTorsor `P` over `V`, any finset `s` of points of type `ι`, and functions `w : ι -> k` and `p : ι -> P`, the weighted differences `(s.weightedVSubOfPoint p (p i)) w` and `(insert i s).weightedVSubOfPoint p (p i)) w` are equal.
|
Finset.eq_weightedVSub_subset_iff_eq_weightedVSub_subtype
theorem Finset.eq_weightedVSub_subset_iff_eq_weightedVSub_subtype :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} {v : V} {s : Set ι} {p : ι → P},
(∃ fs, ↑fs ⊆ s ∧ ∃ w, (fs.sum fun i => w i) = 0 ∧ v = (fs.weightedVSub p) w) ↔
∃ fs w, (fs.sum fun i => w i) = 0 ∧ v = (fs.weightedVSub fun i => p ↑i) w
This theorem states that for a given index family of points and a subset of the index type, a vector can be expressed using the `weightedVSub` function over a `Finset` within that subset with a sum of weights equal to 0 if and only if it can be expressed using the `weightedVSub` function with a sum of weights equal to 0 for the corresponding indexed family whose index type is the subtype corresponding to that subset. Here, `weightedVSub` refers to the weighted subtraction operation on vectors, `Finset` is a finite set, and the index family refers to a collection of points indexed by elements from the index set. The theorem also involves several type constraints, including the requirement that the weights form a ring, the vectors form an additive commutative group, and the vectors form a module over the ring, in addition to the assumption that the set of vectors is an additive torsor.
More concisely: For a given index family of vectors over a ring, a vector can be expressed as the weighted subtraction of vectors within a subset of the index type using weights summing to 0 if and only if it can be expressed as the weighted subtraction of vectors in the corresponding subfamily indexed by that subset with weights summing to 0.
|
mem_vectorSpan_iff_eq_weightedVSub
theorem mem_vectorSpan_iff_eq_weightedVSub :
∀ {ι : Type u_1} (k : Type u_2) {V : Type u_3} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] {v : V} {p : ι → P},
v ∈ vectorSpan k (Set.range p) ↔ ∃ s w, (s.sum fun i => w i) = 0 ∧ v = (s.weightedVSub p) w
This theorem states that for any index type `ι`, field `k`, additive commutative group `V`, and torsor `P` over `V`, any vector `v` from `V` is in the `vectorSpan` of an indexed family `p` if and only if it is a `weightedVSub` of `p` with the sum of weights equalling 0. In other words, a vector is in the spanning set of differences of a set of points defined by `p` if and only if it can be expressed as a linear combination of vectors from this set, where the coefficients of this combination sum up to zero.
More concisely: For any index type `ι`, additive commutative group `V`, torsor `P` over `V`, and vector `v` in `V`, `v` is in the span of `P` if and only if there exist weights `w : ∏ i, ℤ` summing to zero such that `v = ∑ i, w(i) * (P i)`.
|
affineCombination_mem_affineSpan
theorem affineCombination_mem_affineSpan :
∀ {ι : Type u_1} {k : Type u_2} {V : Type u_3} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Nontrivial k] {s : Finset ι} {w : ι → k},
(s.sum fun i => w i) = 1 → ∀ (p : ι → P), (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
This theorem states that for any indexed family of points `p : ι → P` in an affine space `P`, with `k` being the underlying nontrivial ring, `V` the associated vector space and `ι` indexing the family, if we consider a finite set `s` of indices and a weight function `w : ι → k` such that the sum of weights over `s` equals 1, then the affine combination `Finset.affineCombination k s p w` lies in the affine span of the range of points `p`. In other words, any affine combination of points from the family where the weights sum to 1 is contained in the smallest affine subspace containing the points in the family.
More concisely: Given an indexed family of points `p : ι → P` in an affine space `P` over a nontrivial ring `k`, any finite set `s` of indices and a weight function `w : ι → k` with `∑ i in s w i = 1`, the affine combination `Finset.affineCombination k s p w` lies in the affine span of `{p i | i ∈ s}`.
|
Finset.sum_centroidWeights_eq_one_of_card_eq_add_one
theorem Finset.sum_centroidWeights_eq_one_of_card_eq_add_one :
∀ (k : Type u_1) [inst : DivisionRing k] {ι : Type u_4} (s : Finset ι) [inst_1 : CharZero k] {n : ℕ},
s.card = n + 1 → (s.sum fun i => Finset.centroidWeights k s i) = 1
The theorem `Finset.sum_centroidWeights_eq_one_of_card_eq_add_one` states that for any division ring `k` of characteristic zero and any finite set `s` of type `ι`, if the cardinality of `s` is `n + 1`, then the sum of the centroid weights for `s` is equal to 1. Here, the centroid weight for each element of `s` is defined as the reciprocal of the cardinality of `s`. Essentially, this theorem guarantees that in a division ring of characteristic zero, when you compute the centroid of `n + 1` points, the sum of the weights used to compute the centroid is precisely 1.
More concisely: In a division ring of characteristic zero, the sum of the reciprocal centroid weights of a finite set with `n + 1` elements is equal to 1.
|
Finset.sum_smul_const_vsub_eq_vsub_affineCombination
theorem Finset.sum_smul_const_vsub_eq_vsub_affineCombination :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p₂ : ι → P) (p₁ : P),
(s.sum fun i => w i) = 1 → (s.sum fun i => w i • (p₁ -ᵥ p₂ i)) = p₁ -ᵥ (Finset.affineCombination k s p₂) w
This theorem states that for any given set of indices `s`, a function `w` mapping each index to a scalar, a function `p₂` mapping each index to a point in an affine space, and a fixed point `p₁` in that same space, if the sum of the scalars from the function `w` equals 1, then the sum of the scalar-multiplications (`w i`) of the difference vectors (`p₁ -ᵥ p₂ i`) is equal to the difference vector between `p₁` and the affine combination of `s` and `p₂` by `w`. Essentially, this links the concept of a weighted sum of pairwise subtractions where the point on the left is constant and the sum of the weights equals 1, to the concept of affine combinations in a vector space.
More concisely: For any set of indices `s`, functions `w` mapping each index to a scalar, and `p₂` mapping each index to a point in an affine space, if `∑ i in s (w i) = 1`, then `∑ i in s (w i * (p₁ - p₂ i)) = p₁ - ∑ i in s (w i * p₂ i)`.
|
mem_affineSpan_iff_eq_affineCombination
theorem mem_affineSpan_iff_eq_affineCombination :
∀ {ι : Type u_1} (k : Type u_2) (V : Type u_3) {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Nontrivial k] {p1 : P} {p : ι → P},
p1 ∈ affineSpan k (Set.range p) ↔ ∃ s w, (s.sum fun i => w i) = 1 ∧ p1 = (Finset.affineCombination k s p) w
This theorem states that for any indexed family of points `p` in an affine space `P` over a vector space `V` and a nontrivial ring `k`, a point `p1` is in the affine span of this family if and only if there exists a finite subset `s` and a weight function `w` such that the sum of these weights is `1` and `p1` is the affine combination of the points in this subset with respect to these weights. This underpins the concept of the affine span as the collection of all possible affine combinations of a set of points.
More concisely: For any indexed family of points in an affine space over a vector space and a nontrivial ring, a point is in the affine span if and only if it is an affine combination of a finite subset with respect to weights summing to 1.
|
Finset.weightedVSub_empty
theorem Finset.weightedVSub_empty :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (w : ι → k) (p : ι → P), (∅.weightedVSub p) w = 0
This theorem states that the `weightedVSub` (weighted vector subtraction) for an empty set is always zero. Specifically, it's applicable for any types `k`, `V`, `P`, and `ι`, where `k` is a ring, `V` is an additive commutative group, `V` is also a `k`-module, and `S` is an additive torsor of `V` on `P`. The weights are given by a function `w : ι → k` and the points are given by a function `p : ι → P`. It doesn't matter what `w` and `p` are; when applied to an empty set, the `weightedVSub` always returns zero.
More concisely: For any ring `k`, additive commutative group `V` with `k`-module structure, and additive torsor `S` over `V` on a type `P`, the weighted vector subtraction `weightedVSub` of the empty set with respect to weights `w : ι → k` and points `p : ι → P` is equal to the zero element of `k`.
|
Finset.affineCombination_congr
theorem Finset.affineCombination_congr :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) {w₁ w₂ : ι → k},
(∀ i ∈ s, w₁ i = w₂ i) →
∀ {p₁ p₂ : ι → P},
(∀ i ∈ s, p₁ i = p₂ i) → (Finset.affineCombination k s p₁) w₁ = (Finset.affineCombination k s p₂) w₂
The theorem `Finset.affineCombination_congr` states that given two families of weights (`w₁` and `w₂`), and two families of points (`p₁` and `p₂`), over a certain type `ι` across a finite set `s`, if both these families of weights and points are equal for every element in `s`, then the affine combinations of the two families of points with their corresponding weights are equal. Here, an affine combination refers to a linear combination where the sum of the scalars (weights) is 1. This theorem is established under the context of a commutative (additive) group structure on the vector space `V`, a module structure of the ring `k` on `V`, and an add-torsor structure on `P` over `V`.
More concisely: Given families of weights `w₁`, `w₂` and points `p₁`, `p₂` over a finite set `s`, if `w₁ = w₂` and `p₁ = p₂` for all `i ∈ s`, then the affine combinations of `p₁` and `w₁` and of `p₂` and `w₂` are equal.
|
Finset.centroid_eq_of_inj_on_of_image_eq
theorem Finset.centroid_eq_of_inj_on_of_image_eq :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] {ι : Type u_4} (s : Finset ι) {ι₂ : Type u_5} (s₂ : Finset ι₂)
{p : ι → P},
(∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j) →
∀ {p₂ : ι₂ → P},
(∀ i ∈ s₂, ∀ j ∈ s₂, p₂ i = p₂ j → i = j) →
p '' ↑s = p₂ '' ↑s₂ → Finset.centroid k s p = Finset.centroid k s₂ p₂
The theorem `Finset.centroid_eq_of_inj_on_of_image_eq` states that, given two indexed sets of points that are injective (i.e., no two different indices map to the same point) on their respective finsets, if the set of points obtained from both finsets are the same, then the centroids of these two sets of points are also the same. This is stated within the context of a certain division ring `k`, an additive commutative group `V`, a module of `V` over `k`, and an additive torsor `P` of `V`. The centroids are calculated according to the function `Finset.centroid`, which assigns to each finset and each function from the index set to `P` a point in `P`. The theorem essentially says that the centroids are invariant under a one-to-one correspondence between the indices which preserves the points.
More concisely: Given injective functions from index sets to an additive torsor over a division ring, if the images of these functions map the same finsets to the same set of points, then the centroids of these sets of points are equal.
|
Finset.centroidWeights_apply
theorem Finset.centroidWeights_apply :
∀ (k : Type u_1) [inst : DivisionRing k] {ι : Type u_4} (s : Finset ι) (i : ι),
Finset.centroidWeights k s i = (↑s.card)⁻¹
The theorem `Finset.centroidWeights_apply` states that for any division ring `k`, any finset `s` of type ι, and any element `i` of type ι, the application of the function `centroidWeights` to `k`, `s`, and `i` equals the reciprocal of the cardinality of the finset `s`. In simpler terms, the weight for any point in the finset in the centroid calculation is equal to one over the total number of points in the finset.
More concisely: For any division ring `k`, finset `s` of type ι, and element `i` of type ι, `centroidWeights k s i` equals the reciprocal of the cardinality of `s`. In other words, the weight assigned to each element in the centroid calculation is 1 over the total number of elements in the finset.
|
Finset.weightedVSub_weightedVSubVSubWeights
theorem Finset.weightedVSub_weightedVSubVSubWeights :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [inst_3 : DecidableEq ι] (p : ι → P) {i j : ι},
i ∈ s → j ∈ s → (s.weightedVSub p) (Finset.weightedVSubVSubWeights k i j) = p i -ᵥ p j
This theorem states that for any type `k` that forms a ring, types `V` and `P` such that `V` forms an additive commutative group and `P` can be viewed as an affine space over `V`, a `Finset` `s` of type `ι` with decidable equality, and a mapping `p` from `ι` to `P`, if `i` and `j` are elements of `s`, then the weighted subtraction of the mapping over the `Finset` using the `weightedVSubVSubWeights` function gives the same result as subtracting the images of `i` and `j` under `p` in the affine space. In mathematical notations, it means that $(s.\text{weightedVSub} \: p) \: (\text{Finset.weightedVSubVSubWeights} \: k \: i \: j) = p(i) - p(j)$, where "$-ᵥ$" represents the subtraction in the affine space.
More concisely: For any ring `k`, additive commutative group `V` over `k`, affine space `P` over `V`, finite set `s` with decidable equality, and mapping `p` from `s` to `P`, the weighted subtraction of `p` over `s` using `weightedVSubVSubWeights` equals the sum of subtracting the images of each pair of elements in `s`. In other words, $(s.\text{weightedVSub} \: p) \: (\text{Finset.weightedVSubVSubWeights} \: k \: i \: j) = \sum\_{l \in s, l \neq i, l \neq j} (-p(l)) + (p(i) - p(j))$.
|
Finset.weightedVSubOfPoint_apply_const
theorem Finset.weightedVSubOfPoint_apply_const :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p b : P),
(s.weightedVSubOfPoint (fun x => p) b) w = (s.sum fun i => w i) • (p -ᵥ b)
This theorem states that for any set `s` of indices of type `ι`, any weight function `w : ι → k` from the indices to a ring `k`, and any two points `p` and `b` in an affine space `P` over a vector space `V` with scalars from `k`, the weighted subtraction of point `b` from each point in the set `s`, where each point in the set is the same and equal to `p`, is equal to the sum of the weights of the elements in `s` scaled by the vector from `b` to `p`. This is under the assumptions that `V` forms an additive commutative group, and `V` is a `k`-module. The operation `p -ᵥ b` denotes the subtraction of the point `b` from `p` in the affine space `P`.
More concisely: For any set `s` of indices, any weight function `w : ι → k`, and any point `p, b` in an additive commutative `k`-module `V`, the sum of weights of elements in `s` scaled by the vector `p - b` equals the weighted subtraction of `b` from each point `p` in `s` in the affine space over `V`.
|
Finset.weightedVSub_apply
theorem Finset.weightedVSub_apply :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P),
(s.weightedVSub p) w = s.sum fun i => w i • (p i -ᵥ Classical.choice ⋯)
This theorem, `Finset.weightedVSub_apply`, states that for any set `s` of elements of type `ι`, any function `w` mapping from `ι` to a ring `k`, and any function `p` mapping from `ι` to a AddTorsor `P` (which is a module over `k`), the weighted difference from the base point (computed using `weightedVSub`) of the points designated by `p`, when applied to the weights `w`, equals the sum over all elements of the set `s` of the scalar multiples (with scalar given by `w`) of the difference between the point `p i` and an arbitrary base point (chosen by `Classical.choice`). The base point is from the same torsor as the values of `p`.
More concisely: For any set `s`, function `w` mapping from `ι` to a ring `k`, and function `p` mapping from `ι` to an AddTorsor `P` over `k`, the weighted difference of the points `p i` (with weights `wi`) is equal to the sum of the scalar multiples of the differences between `p i` and a base point, over all `i` in `s`.
|
Finset.weightedVSub_subtype_eq_filter
theorem Finset.weightedVSub_subtype_eq_filter :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) (pred : ι → Prop)
[inst_3 : DecidablePred pred],
(((Finset.subtype pred s).weightedVSub fun i => p ↑i) fun i => w ↑i) =
((Finset.filter pred s).weightedVSub p) w
The theorem `Finset.weightedVSub_subtype_eq_filter` states that for any ring `k`, Additive Commutative Group `V`, Module of `k` over `V`, Additive Torsor `S` of `V` over `P`, a set `s` of elements of some type `ι`, along with a weighting function `w` from `ι` to `k`, a function `p` from `ι` to `P`, and a predicate `pred` on `ι`, if the predicate `pred` is decidable, then the weighted subtraction over the subset of `s` that satisfy `pred` (represented as `s.subtype pred`), using `p` applied to the elements of `s` as coordinates and `w` as weights, is equal to the weighted subtraction over the elements of `s` that satisfy `pred` (represented as `s.filter pred`), using `p` as coordinates and `w` as weights.
In more simple terms, when considering elements of a set `s` that satisfy a certain condition, the result of a weighted subtraction operation doesn't change whether we treat these elements as a subtype or filter them out of the original set.
More concisely: For any ring `k`, Additive Commutative Group `V`, Module of `k` over `V`, Additive Torsor `S` of `V` over `P`, set `s` of elements of type `ι`, weighting function `w` from `ι` to `k`, function `p` from `ι` to `P`, and decidable predicate `pred` on `ι`, the weighted subtraction over the subtype `s.subtype pred` using `p` and `w` is equal to the weighted subtraction over the filter `s.filter pred` using `p` and `w`.
|
Finset.sum_smul_vsub_eq_weightedVSub_sub
theorem Finset.sum_smul_vsub_eq_weightedVSub_sub :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p₁ p₂ : ι → P),
(s.sum fun i => w i • (p₁ i -ᵥ p₂ i)) = (s.weightedVSub p₁) w - (s.weightedVSub p₂) w
This theorem states that for any set of indices `s`, any function `w` from these indices to a ring `k`, and any two functions `p₁` and `p₂` from the indices to a torsor `P` over a module `V` over `k`, the weighted sum of the differences between the results of applying `p₁` and `p₂` to each index (scaled by the weight of the index) is equal to the difference between the weighted sum of vectors from the origin to the results of `p₁` and the weighted sum of vectors from the origin to the results of `p₂`. This theorem is generally applicable in the context of vector spaces or affine spaces, where `weightedVSub` is defined as the sum of the scaled vectors from the origin to the points determined by a function.
More concisely: For any set of indices `s`, any function `w` from `s` to a ring `k`, and functions `p₁` and `p₂` from `s` to a torsor `P` over a module `V` over `k`, the weighted sum of the differences between `p₁` and `p₂` applied to each index, scaled by the corresponding weight, equals the difference between the weighted sums of the vectors from the origin to `p₁` and `p₂`'s images.
|
Finset.sum_centroidWeights_eq_one_of_card_ne_zero
theorem Finset.sum_centroidWeights_eq_one_of_card_ne_zero :
∀ (k : Type u_1) [inst : DivisionRing k] {ι : Type u_4} (s : Finset ι) [inst_1 : CharZero k],
s.card ≠ 0 → (s.sum fun i => Finset.centroidWeights k s i) = 1
The theorem `Finset.sum_centroidWeights_eq_one_of_card_ne_zero` states that in the characteristic zero case (this is the scenario where zero cannot be represented as a finite sum of units), the sum of the weights in the centroid equals to 1, if the number of points is non-zero. Here the centroid is calculated for a finite set 's' of elements of some type 'ι' in a division ring 'k'. The weights of the centroid are defined as the reciprocal of the cardinality (number of elements) of the set 's'. The sum is taken over all elements 'i' of the set 's'. This theorem essentially establishes a key property of centroids, that the sum of the weights of all the points contributing to the centroid equals to 1, provided that the set of points is not empty.
More concisely: In characteristic zero, the sum of the reciprocal cardinalities of a non-empty finite set's elements equals 1 for the centroid weights.
|
Finset.affineCombination_map
theorem Finset.affineCombination_map :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} {ι₂ : Type u_5} (s₂ : Finset ι₂) (e : ι₂ ↪ ι) (w : ι → k) (p : ι → P),
(Finset.affineCombination k (Finset.map e s₂) p) w = (Finset.affineCombination k s₂ (p ∘ ⇑e)) (w ∘ ⇑e)
The theorem states that for any ring `k`, a commutative add group `V`, a module `V` over `k`, an add torsor `S` over `V`, types `ι` and `ι₂`, a finset `s₂` of type `ι₂`, an embedding `e` from `ι₂` to `ι`, and functions `w: ι → k` and `p: ι → P`, the affine combination over the image of the embedding (the finset `s₂` mapped by `e`) using the functions `w` and `p`, is equal to the affine combination over the original finset `s₂` using the compositions of the functions `w` and `p` with the embedding `e`. In simpler terms, it means that the result of an affine combination doesn't change if we first apply an embedding to the finset and then calculate the combination, or if we first apply the embedding to the function inputs and then calculate the combination.
More concisely: For any ring `k`, commutative add group `V`, module `V` over `k`, add torsor `S` over `V`, types `ι` and `ι₂`, finset `s₂` of type `ι₂`, embedding `e` from `ι₂` to `ι`, functions `w: ι → k`, and `p: ι → P`: The affine combination over `s₂` using `w` and `p` is equal to the affine combination over `e[s₂]` using `w ∘ e` and `p ∘ e`, where `e[s₂]` is the image of `s₂` under the embedding.
|
Finset.weightedVSub_const_smul
theorem Finset.weightedVSub_const_smul :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) (c : k),
(s.weightedVSub p) (c • w) = c • (s.weightedVSub p) w
This theorem states that for a given finset `s`, a given set of weights `w`, a given set of points `p`, and a scalar `c`, the weighted difference of `p` with weights `c` times `w` is equal to `c` times the weighted difference of `p` with weights `w`. Here, `weightedVSub` represents the weighted difference of a set of points in a module over a ring, with the weights given by a function from the elements of the finset to the ring. The constant multiplier `c` can be moved outside the sum, which reflects the distributive property of scalar multiplication over summation in a vector space.
More concisely: For any finset `s`, set of weights `w`, points `p`, scalar `c`, and with `weightedVSub` denoting weighted difference, we have `c * (weightedVSub p w) = weightedVSub (c * p) w`.
|
Finset.map_affineCombination
theorem Finset.map_affineCombination :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) {V₂ : Type u_6} {P₂ : Type u_7} [inst_3 : AddCommGroup V₂]
[inst_4 : Module k V₂] [inst_5 : AddTorsor V₂ P₂] (p : ι → P) (w : ι → k),
s.sum w = 1 →
∀ (f : P →ᵃ[k] P₂), f ((Finset.affineCombination k s p) w) = (Finset.affineCombination k s (⇑f ∘ p)) w
This theorem states that for any given ring `k`, commutative additive groups `V` and `V₂`, modules `V` and `V₂` over the ring `k`, affine spaces `P` and `P₂` over `V` and `V₂` respectively, a finite set `s` of type `ι`, a function `p` mapping elements of `s` to `P`, and a weight function `w` mapping elements of `s` to `k`, if the sum of the weights equals one, then for any affine map `f` from `P` to `P₂`, applying `f` to the affine combination of `p` with respect to `w` is the same as the affine combination of the mapped points (i.e., `f` applied to `p`) with respect to `w`. In other words, affine maps commute with affine combinations.
More concisely: Given a ring `k`, commutative additive groups `V` and `V₂`, modules `V` and `V₂` over `k`, affine spaces `P` and `P₂` over `V` and `V₂` respectively, a finite set `s` with weight function `w` on `s` such that `∑(w i) = 1`, any affine map `f` from `P` to `P₂`, the affine combination of `f(p i)` with respect to `w` equals `f` applied to the affine combination of `p i` with respect to `w` for all `i` in `s`.
|
Finset.eq_weightedVSubOfPoint_subset_iff_eq_weightedVSubOfPoint_subtype
theorem Finset.eq_weightedVSubOfPoint_subset_iff_eq_weightedVSubOfPoint_subtype :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} {v : V} {x : k} {s : Set ι} {p : ι → P} {b : P},
(∃ fs, ↑fs ⊆ s ∧ ∃ w, (fs.sum fun i => w i) = x ∧ v = (fs.weightedVSubOfPoint p b) w) ↔
∃ fs w, (fs.sum fun i => w i) = x ∧ v = (fs.weightedVSubOfPoint (fun i => p ↑i) b) w
The theorem `Finset.eq_weightedVSubOfPoint_subset_iff_eq_weightedVSubOfPoint_subtype` states that for a ring `k`, a commutative group `V`, a module `V` over `k`, an additive torsor `S` over `V`, a set `s` of indices `ι`, a mapping `p` from `ι` to points `P`, a point `b` in `P`, a vector `v` in `V`, and a scalar `x` in `k`, a vector can be expressed as the weighted difference (`weightedVSubOfPoint`) of points with respect to `b` using weights that sum to `x` and a finite set (`Finset`) within the subset `s` if and only if it can also be expressed as the `weightedVSubOfPoint` for the corresponding mapping `p` whose index type is the subtype corresponding to the subset `s` with weights that sum to `x`.
More concisely: For a ring `k`, a commutative group `V`, a module `V` over `k`, an additive torsor `S` over `V`, a set `s` of indices `ι`, a mapping `p` from `ι` to points `P`, a point `b` in `P`, a vector `v` in `V`, and a scalar `x` in `k`, the vector `v` is the weighted difference of points in `s` with respect to `b` using weights that sum to `x` if and only if it is the weighted difference of points in the subtype of `p` corresponding to `s` with respect to `b` using weights that sum to `x`.
|
centroid_mem_affineSpan_of_card_eq_add_one
theorem centroid_mem_affineSpan_of_card_eq_add_one :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] {ι : Type u_4} [inst_4 : CharZero k] {s : Finset ι} (p : ι → P)
{n : ℕ}, s.card = n + 1 → Finset.centroid k s p ∈ affineSpan k (Set.range p)
This theorem states that in a characteristic zero division ring, for any set of points represented by a function `p : ι → P` and a finite set `s : Finset ι` with `n + 1` elements, the centroid of those points lies in the affine span of the range of the function `p`. The terms `affineSpan` and `centroid` are defined in terms of certain mathematical structures, including a division ring, an additive commutative group, and a module, and the theorem is stated in a context where these structures have certain properties (e.g., the ring is a division ring with characteristic zero). In simpler terms, if you have `n + 1` points in a vector space over a field of characteristic zero, the center of mass of those points (the centroid) is contained within the smallest affine subspace that contains all of those points.
More concisely: In a division ring of characteristic zero, the centroid of a finite set of points lies in the affine span of those points.
|
Finset.affineCombination_filter_of_ne
theorem Finset.affineCombination_filter_of_ne :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) {pred : ι → Prop}
[inst_3 : DecidablePred pred],
(∀ i ∈ s, w i ≠ 0 → pred i) →
(Finset.affineCombination k (Finset.filter pred s) p) w = (Finset.affineCombination k s p) w
The theorem `Finset.affineCombination_filter_of_ne` states that for any given Ring `k`, Additive Commutative Group `V`, and Module `k V` over an Additive Torsor `V P`, and for any `Finset ι` (a finite set of elements of type `ι`), a function `w : ι → k` (assigning weights of type `k` to each element in `ι`), a function `p : ι → P` (assigning points of type `P` to each element in `ι`), and a predicate `pred : ι → Prop`, if all weights `w i` for each `i` in the finite set `s` that don't satisfy the predicate `pred` are zero, then the affine combination over the filtered set `s.filter pred` equals the affine combination over the entire set `s`. In other words, if weights are zero for all elements that fail the predicate, filtering those elements out has no impact on the result of the affine combination.
More concisely: If `w : ι → k` and `p : ι → P` are functions for a Ring `k`, Additive Commutative Group `V`, and Module `k V` over an Additive Torsor `V P`, and `pred : ι → Prop` is a predicate such that all weights `w i` with `i` not in the filter of `s.filter pred` are zero, then the affine combinations of `(w i, p i)` over `s` and `s.filter pred` are equal.
|
Finset.weightedVSub_vadd_affineCombination
theorem Finset.weightedVSub_vadd_affineCombination :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w₁ w₂ : ι → k) (p : ι → P),
(s.weightedVSub p) w₁ +ᵥ (Finset.affineCombination k s p) w₂ = (Finset.affineCombination k s p) (w₁ + w₂)
This theorem states that for any finitely indexed set `s` with indices of type `ι`, if `w₁` and `w₂` are two weight functions (functions from indices to a ring `k`), and `p` maps indices to points in an affine space `P` (built over a vector space `V` with scalars in `k`), then adding the weighted sum of vectors in `V` (calculated using `s`, `w₁`, and `p`) to an affine combination of points in `P` (calculated using `s`, `p`, and `w₂`) equals the affine combination calculated using `s`, `p`, and the sum of `w₁` and `w₂`. This theorem is a property of operations in affine spaces over vector spaces.
More concisely: For any finitely indexed set `s` with values in an affine space `P` over a vector space `V` with scalars in a ring `k`, and any weight functions `w₁` and `w₂` on `s`, the affine combination of points in `P` using weights `w₁` and index function `p`, plus the weighted sum of vectors in `V` using weights `w₂` and index function `p`, equals the affine combination using weights `w₁ + w₂`.
|
Finset.affineCombination_of_eq_one_of_eq_zero
theorem Finset.affineCombination_of_eq_one_of_eq_zero :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) {i : ι},
i ∈ s → w i = 1 → (∀ i2 ∈ s, i2 ≠ i → w i2 = 0) → (Finset.affineCombination k s p) w = p i
This theorem states that, given a ring `k`, an Abelian group `V`, a module `V` over `k`, an affine torsor `S` over `V` and `P`, a set `s` of indices of type `ι`, a weight function `w` from `ι` to `k`, and a point function `p` from `ι` to `P`, if an index `i` belongs to `s` such that the weight of `i` is 1 and the weight of all other indices in `s` (different from `i`) is 0, then the affine combination (which is a sum of the product of the weight of each point and the point itself) of `s` with respect to `w` and `p` equals the point `p i`. In simple terms, it means that in an affine combination, a point with weight 1 and all other points with weight 0 will result in the weighted point itself.
More concisely: Given a ring `k`, an Abelian group `V` with a module structure over `k`, an affine torsor `S` over `V`, a weight function `w : ι -> k`, and a point function `p : ι -> P`, if there exists `i` in `s` (an index set) such that `w i = 1` and `w j = 0` for all `j` in `s` different from `i`, then the affine combination of `s` with respect to `w` and `p` equals `p i`.
|
Finset.affineCombination_affineCombinationLineMapWeights
theorem Finset.affineCombination_affineCombinationLineMapWeights :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [inst_3 : DecidableEq ι] (p : ι → P) {i j : ι},
i ∈ s →
j ∈ s →
∀ (c : k),
(Finset.affineCombination k s p) (Finset.affineCombinationLineMapWeights i j c) =
(AffineMap.lineMap (p i) (p j)) c
This theorem states that for any ring `k`, an additive commutative group `V`, a `k`-module `V`, and an affine space `P` over `V`, given a finite set `s` of indices type `ι` with decidable equality, and a function `p` from `ι` to points in `P`, if `i` and `j` are members of `s`, then for any scalar `c` in `k`, the affine combination of `s` using the weights determined by `affineCombinationLineMapWeights i j c` is equal to the result of applying the linear map from `k` to `P` that sends `0` to `p i` and `1` to `p j` to the scalar `c`. In other words, it asserts that the result of the `line_map` from the points `p i` to `p j` applied to a scalar `c` can be expressed as an affine combination of the points using the weights given by `affineCombinationLineMapWeights i j c`.
More concisely: For any ring `k`, additive commutative group `V`, `k`-module `V`, and affine space `P` over `V`, given a finite set `s` of indices `ι` with decidable equality and a function `p` from `ι` to points in `P`, the affine combination of `s` using the weights determined by `affineCombinationLineMapWeights i j c` equals the result of applying the linear map from `k` to `P` that sends `0` to `p i` and `1` to `p j` to the scalar `c`.
|
Finset.weightedVSubOfPoint_eq_of_weights_eq
theorem Finset.weightedVSubOfPoint_eq_of_weights_eq :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (p : ι → P) (j : ι) (w₁ w₂ : ι → k),
(∀ (i : ι), i ≠ j → w₁ i = w₂ i) → (s.weightedVSubOfPoint p (p j)) w₁ = (s.weightedVSubOfPoint p (p j)) w₂
The theorem `Finset.weightedVSubOfPoint_eq_of_weights_eq` states that, given a family of points represented by a function `p` from an index set `ι` to a type `P` of points in a module over a ring, if we use one member of the family as a base point, the vector subtraction operation `weightedVSubOfPoint` does not depend on the value of the weights at this base point. More specifically, if we have two weight functions `w₁` and `w₂` from the index set to the ring, and these functions are equal at every point except possibly the base point, then the results of `weightedVSubOfPoint` with these two weight functions (and the same family of points and base point) are equal.
More concisely: Given a family of points and two weight functions that agree on all indices except possibly the base point, the `weightedVSubOfPoint` operation with respect to these weight functions and the same base point yields the same result.
|