English
If p : ι → P and j : ι, then q ∈ affineSpan k (Set.range p) if and only if there exist s and w such that q equals s.weightedVSubOfPoint p (p j) w plus q_vec at p_j.
Русский
Для p и j: q принадлежит афинному span тогда и только тогда существует s и w так, что q равно s.weightedVSubOfPoint p (p_j) w плюс p_j.
LaTeX
$$$q ∈ \affineSpan_k(\Set.range p) \iff \exists s,w, q = s.weightedVSubOfPoint p (p j) w +\!_v p j$$$
Lean4
/-- Given a family of points together with a chosen base point in that family, membership of the
affine span of this family corresponds to an identity in terms of `weightedVSubOfPoint`, with
weights that are not required to sum to 1. -/
theorem mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd [Nontrivial k] (p : ι → P) (j : ι) (q : P) :
q ∈ affineSpan k (Set.range p) ↔ ∃ (s : Finset ι) (w : ι → k), q = s.weightedVSubOfPoint p (p j) w +ᵥ p j :=
by
constructor
· intro hq
obtain ⟨s, w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan hq
exact ⟨s, w, s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p hw (p j)⟩
· rintro ⟨s, w, rfl⟩
classical
let w' : ι → k := Function.update w j (1 - (s \ { j }).sum w)
have h₁ : (insert j s).sum w' = 1 := by
by_cases hj : j ∈ s
· simp [w', Finset.sum_update_of_mem hj, Finset.insert_eq_of_mem hj]
·
simp_rw [w', Finset.sum_insert hj, Finset.sum_update_of_notMem hj, Function.update_self, ← Finset.erase_eq,
Finset.erase_eq_of_notMem hj, sub_add_cancel]
have hww : ∀ i, i ≠ j → w i = w' i := by
intro i hij
simp [w', hij]
rw [s.weightedVSubOfPoint_eq_of_weights_eq p j w w' hww, ← s.weightedVSubOfPoint_insert w' p j, ←
(insert j s).affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w' p h₁ (p j)]
exact affineCombination_mem_affineSpan h₁ p
