mathlib docs: linear_algebra.affine

source

def finset.weighted_vsub_of_point {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : affine_space V P] {ι : Type u_4} :

finset ι → (ι → P) → P → ((ι → k) →ₗ[k] V)

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

Equations

s.weighted_vsub_of_point p b = s.sum (λ (i : ι), (linear_map.proj i).smul_right (p i -ᵥ b))

source

@[simp]

theorem finset.weighted_vsub_of_point_apply {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : affine_space V P] {ι : Type u_4} (s : finset ι) (w : ι → k) (p : ι → P) (b : P) :

⇑(s.weighted_vsub_of_point p b) w = s.sum (λ (i : ι), w i • (p i -ᵥ b))

source

theorem finset.weighted_vsub_of_point_eq_of_sum_eq_zero {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : affine_space V P] {ι : Type u_4} (s : finset ι) (w : ι → k) (p : ι → P) (h : s.sum (λ (i : ι), w i) = 0) (b₁ b₂ : P) :

⇑(s.weighted_vsub_of_point p b₁) w = ⇑(s.weighted_vsub_of_point p b₂) w

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

source

theorem finset.weighted_vsub_of_point_vadd_eq_of_sum_eq_one {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : affine_space V P] {ι : Type u_4} (s : finset ι) (w : ι → k) (p : ι → P) (h : s.sum (λ (i : ι), w i) = 1) (b₁ b₂ : P) :

⇑(s.weighted_vsub_of_point p b₁) w +ᵥ b₁ = ⇑(s.weighted_vsub_of_point p b₂) w +ᵥ b₂

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

source

@[simp]

theorem finset.weighted_vsub_of_point_erase {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : affine_space V P] {ι : Type u_4} (s : finset ι) (w : ι → k) (p : ι → P) (i : ι) :

⇑((s.erase i).weighted_vsub_of_point p (p i)) w = ⇑(s.weighted_vsub_of_point p (p i)) w

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

source

@[simp]

theorem finset.weighted_vsub_of_point_insert {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : affine_space V P] {ι : Type u_4} (s : finset ι) (w : ι → k) (p : ι → P) (i : ι) :

⇑((has_insert.insert i s).weighted_vsub_of_point p (p i)) w = ⇑(s.weighted_vsub_of_point p (p i)) w

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

source

theorem finset.weighted_vsub_of_point_indicator_subset {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : affine_space V P] {ι : Type u_4} (w : ι → k) (p : ι → P) (b : P) {s₁ s₂ : finset ι} :

s₁ ⊆ s₂ → ⇑(s₁.weighted_vsub_of_point p b) w = ⇑(s₂.weighted_vsub_of_point p b) (↑s₁.indicator w)

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

source

def finset.weighted_vsub {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : affine_space V P] {ι : Type u_4} :

finset ι → (ι → P) → ((ι → k) →ₗ[k] V)

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

Equations

s.weighted_vsub p = s.weighted_vsub_of_point p (classical.choice finset.weighted_vsub._proof_1)

source

theorem finset.weighted_vsub_apply {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : affine_space V P] {ι : Type u_4} (s : finset ι) (w : ι → k) (p : ι → P) :

⇑(s.weighted_vsub p) w = s.sum (λ (i : ι), w i • (p i -ᵥ classical.choice add_torsor.nonempty))

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

source

theorem finset.weighted_vsub_eq_weighted_vsub_of_point_of_sum_eq_zero {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : affine_space V P] {ι : Type u_4} (s : finset ι) (w : ι → k) (p : ι → P) (h : s.sum (λ (i : ι), w i) = 0) (b : P) :

⇑(s.weighted_vsub p) w = ⇑(s.weighted_vsub_of_point p b) w

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

source

@[simp]

theorem finset.weighted_vsub_empty {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : affine_space V P] {ι : Type u_4} (w : ι → k) (p : ι → P) :

⇑(∅.weighted_vsub p) w = 0

The weighted_vsub for an empty set is 0.

source

theorem finset.weighted_vsub_indicator_subset {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : affine_space V P] {ι : Type u_4} (w : ι → k) (p : ι → P) {s₁ s₂ : finset ι} :

s₁ ⊆ s₂ → ⇑(s₁.weighted_vsub p) w = ⇑(s₂.weighted_vsub p) (↑s₁.indicator w)

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

source

def finset.affine_combination {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : affine_space V P] {ι : Type u_4} :

finset ι → (ι → P) → affine_map k (ι → k) P

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

Equations

s.affine_combination p = {to_fun := λ (w : ι → k), ⇑(s.weighted_vsub_of_point p (classical.choice finset.affine_combination._proof_1)) w +ᵥ classical.choice finset.affine_combination._proof_1, linear := s.weighted_vsub p, map_vadd' := _}

source

@[simp]

theorem finset.affine_combination_linear {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : affine_space V P] {ι : Type u_4} (s : finset ι) (p : ι → P) :

(s.affine_combination p).linear = s.weighted_vsub p

The linear map corresponding to affine_combination is weighted_vsub.

source

theorem finset.affine_combination_apply {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : affine_space V P] {ι : Type u_4} (s : finset ι) (w : ι → k) (p : ι → P) :

⇑(s.affine_combination p) w = ⇑(s.weighted_vsub_of_point p (classical.choice add_torsor.nonempty)) w +ᵥ classical.choice add_torsor.nonempty

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

source

theorem finset.affine_combination_eq_weighted_vsub_of_point_vadd_of_sum_eq_one {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : affine_space V P] {ι : Type u_4} (s : finset ι) (w : ι → k) (p : ι → P) (h : s.sum (λ (i : ι), w i) = 1) (b : P) :

⇑(s.affine_combination p) w = ⇑(s.weighted_vsub_of_point p b) w +ᵥ b

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

source

theorem finset.weighted_vsub_vadd_affine_combination {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : affine_space V P] {ι : Type u_4} (s : finset ι) (w₁ w₂ : ι → k) (p : ι → P) :

⇑(s.weighted_vsub p) w₁ +ᵥ ⇑(s.affine_combination p) w₂ = ⇑(s.affine_combination p) (w₁ + w₂)

Adding a weighted_vsub to an affine_combination.

source

theorem finset.affine_combination_vsub {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : affine_space V P] {ι : Type u_4} (s : finset ι) (w₁ w₂ : ι → k) (p : ι → P) :

⇑(s.affine_combination p) w₁ -ᵥ ⇑(s.affine_combination p) w₂ = ⇑(s.weighted_vsub p) (w₁ - w₂)

Subtracting two affine_combinations.

source

@[simp]

theorem finset.affine_combination_of_eq_one_of_eq_zero {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : affine_space V P] {ι : Type u_4} (s : finset ι) (w : ι → k) (p : ι → P) {i : ι} :

i ∈ s → w i = 1 → (∀ (i2 : ι), i2 ∈ s → i2 ≠ i → w i2 = 0) → ⇑(s.affine_combination p) w = p i

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

source

theorem finset.affine_combination_indicator_subset {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : affine_space V P] {ι : Type u_4} (w : ι → k) (p : ι → P) {s₁ s₂ : finset ι} :

s₁ ⊆ s₂ → ⇑(s₁.affine_combination p) w = ⇑(s₂.affine_combination p) (↑s₁.indicator w)

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

source

theorem finset.eq_weighted_vsub_of_point_subset_iff_eq_weighted_vsub_of_point_subtype {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : affine_space V P] {ι : Type u_4} {v : V} {x : k} {s : set ι} {p : ι → P} {b : P} :

(∃ (fs : finset ι) (hfs : ↑fs ⊆ s) (w : ι → k) (hw : fs.sum (λ (i : ι), w i) = x), v = ⇑(fs.weighted_vsub_of_point p b) w) ↔ ∃ (fs : finset ↥s) (w : ↥s → k) (hw : fs.sum (λ (i : ↥s), w i) = x), v = ⇑(fs.weighted_vsub_of_point (λ (i : ↥s), p ↑i) b) w

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

source

theorem finset.eq_weighted_vsub_subset_iff_eq_weighted_vsub_subtype (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : affine_space V P] {ι : Type u_4} {v : V} {s : set ι} {p : ι → P} :

(∃ (fs : finset ι) (hfs : ↑fs ⊆ s) (w : ι → k) (hw : fs.sum (λ (i : ι), w i) = 0), v = ⇑(fs.weighted_vsub p) w) ↔ ∃ (fs : finset ↥s) (w : ↥s → k) (hw : fs.sum (λ (i : ↥s), w i) = 0), v = ⇑(fs.weighted_vsub (λ (i : ↥s), p ↑i)) w

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

source

theorem finset.eq_affine_combination_subset_iff_eq_affine_combination_subtype (k : Type u_1) (V : Type u_2) {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : affine_space V P] {ι : Type u_4} {p0 : P} {s : set ι} {p : ι → P} :

(∃ (fs : finset ι) (hfs : ↑fs ⊆ s) (w : ι → k) (hw : fs.sum (λ (i : ι), w i) = 1), p0 = ⇑(fs.affine_combination p) w) ↔ ∃ (fs : finset ↥s) (w : ↥s → k) (hw : fs.sum (λ (i : ↥s), w i) = 1), p0 = ⇑(fs.affine_combination (λ (i : ↥s), p ↑i)) w

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

source

def finset.centroid_weights (k : Type u_1) [division_ring k] {ι : Type u_4} :

finset ι → ι → k

The weights for the centroid of some points.

Equations

finset.centroid_weights k s = function.const ι (↑(s.card))⁻¹

source

@[simp]

theorem finset.centroid_weights_apply (k : Type u_1) [division_ring k] {ι : Type u_4} (s : finset ι) (i : ι) :

finset.centroid_weights k s i = (↑(s.card))⁻¹

centroid_weights at any point.

source

theorem finset.centroid_weights_eq_const (k : Type u_1) [division_ring k] {ι : Type u_4} (s : finset ι) :

finset.centroid_weights k s = function.const ι (↑(s.card))⁻¹

centroid_weights equals a constant function.

source

theorem finset.sum_centroid_weights_eq_one_of_cast_card_ne_zero {k : Type u_1} [division_ring k] {ι : Type u_4} (s : finset ι) :

↑(s.card) ≠ 0 → s.sum (λ (i : ι), finset.centroid_weights k s i) = 1

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

source

theorem finset.sum_centroid_weights_eq_one_of_card_ne_zero (k : Type u_1) [division_ring k] {ι : Type u_4} (s : finset ι) [char_zero k] :

s.card ≠ 0 → s.sum (λ (i : ι), finset.centroid_weights k s i) = 1

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

source

theorem finset.sum_centroid_weights_eq_one_of_nonempty (k : Type u_1) [division_ring k] {ι : Type u_4} (s : finset ι) [char_zero k] :

s.nonempty → s.sum (λ (i : ι), finset.centroid_weights k s i) = 1

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

source

theorem finset.sum_centroid_weights_eq_one_of_card_eq_add_one (k : Type u_1) [division_ring k] {ι : Type u_4} (s : finset ι) [char_zero k] {n : ℕ} :

s.card = n + 1 → s.sum (λ (i : ι), finset.centroid_weights k s i) = 1

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

source

def finset.centroid (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} :

finset ι → (ι → P) → P

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

Equations

finset.centroid k s p = ⇑(s.affine_combination p) (finset.centroid_weights k s)

source

theorem finset.centroid_def (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} (s : finset ι) (p : ι → P) :

finset.centroid k s p = ⇑(s.affine_combination p) (finset.centroid_weights k s)

The definition of the centroid.

source

@[simp]

theorem finset.centroid_singleton (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} (p : ι → P) (i : ι) :

finset.centroid k {i} p = p i

The centroid of a single point.

source

theorem weighted_vsub_mem_vector_span {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} {s : finset ι} {w : ι → k} (h : s.sum (λ (i : ι), w i) = 0) (p : ι → P) :

⇑(s.weighted_vsub p) w ∈ vector_span k (set.range p)

A weighted_vsub with sum of weights 0 is in the vector_span of an indexed family.

source

theorem affine_combination_mem_affine_span {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} [nontrivial k] {s : finset ι} {w : ι → k} (h : s.sum (λ (i : ι), w i) = 1) (p : ι → P) :

⇑(s.affine_combination p) w ∈ affine_span k (set.range p)

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

source

theorem mem_vector_span_iff_eq_weighted_vsub (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} {v : V} {p : ι → P} :

v ∈ vector_span k (set.range p) ↔ ∃ (s : finset ι) (w : ι → k) (h : s.sum (λ (i : ι), w i) = 0), v = ⇑(s.weighted_vsub p) w

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

source

theorem eq_affine_combination_of_mem_affine_span {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} {p1 : P} {p : ι → P} :

p1 ∈ affine_span k (set.range p) → (∃ (s : finset ι) (w : ι → k) (hw : s.sum (λ (i : ι), w i) = 1), p1 = ⇑(s.affine_combination p) w)

A point in the affine_span of an indexed family is an affine_combination with sum of weights 1.

source

theorem mem_affine_span_iff_eq_affine_combination (k : Type u_1) (V : Type u_2) {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} [nontrivial k] {p1 : P} {p : ι → P} :

p1 ∈ affine_span k (set.range p) ↔ ∃ (s : finset ι) (w : ι → k) (hw : s.sum (λ (i : ι), w i) = 1), p1 = ⇑(s.affine_combination p) w

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

source

theorem centroid_mem_affine_span_of_cast_card_ne_zero {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} {s : finset ι} (p : ι → P) :

↑(s.card) ≠ 0 → finset.centroid k s p ∈ affine_span k (set.range p)

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

source

theorem centroid_mem_affine_span_of_card_ne_zero (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} [char_zero k] {s : finset ι} (p : ι → P) :

s.card ≠ 0 → finset.centroid k s p ∈ affine_span k (set.range p)

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

source

theorem centroid_mem_affine_span_of_nonempty (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} [char_zero k] {s : finset ι} (p : ι → P) :

s.nonempty → finset.centroid k s p ∈ affine_span k (set.range p)

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

source

theorem centroid_mem_affine_span_of_card_eq_add_one (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} [char_zero k] {s : finset ι} (p : ι → P) {n : ℕ} :

s.card = n + 1 → finset.centroid k s p ∈ affine_span k (set.range p)

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

source

def affine_map.weighted_vsub_of_point {k : Type u_1} {V : Type u_2} (P : Type u_3) [comm_ring k] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} :

finset ι → (ι → k) → affine_map k ((ι → P) × P) V

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

Equations

affine_map.weighted_vsub_of_point P s w = {to_fun := λ (p : (ι → P) × P), ⇑(s.weighted_vsub_of_point p.fst p.snd) w, linear := s.sum (λ (i : ι), w i • ((linear_map.proj i).comp (linear_map.fst k (ι → V) V) - linear_map.snd k (ι → V) V)), map_vadd' := _}

mathlib documentation

linear_algebra.affine_space.combination

Affine combinations of points

Main definitions

References

General documentation

Additional documentation

Library

mathlib documentation

linear_algebra.​affine_space.​combination

Affine combinations of points

Main definitions

References

General documentation

Additional documentation

Library

linear_algebra.affine_space.combination