English
A point lies in the affine span if and only if it can be written as an affineCombination with weights summing to 1.
Русский
Точка принадлежит афинному span тогда и только тогда, когда её можно записать как аффинное сочетание со сумма весов, равной 1.
LaTeX
$$$p_1 \in \ affineSpan_k(\{ p_i : i \in \} ) \iff \exists s,w, \sum_{i\in s} w_i = 1 \land p_1 = s.affineCombination k p w$$$
Lean4
/-- A vector is in the `vectorSpan` of an indexed family if and only
if it is a `weightedVSub` with sum of weights 0. -/
theorem mem_vectorSpan_iff_eq_weightedVSub {v : V} {p : ι → P} :
v ∈ vectorSpan k (Set.range p) ↔ ∃ (s : Finset ι) (w : ι → k), ∑ i ∈ s, w i = 0 ∧ v = s.weightedVSub p w := by
classical
constructor
· rcases isEmpty_or_nonempty ι with (hι | ⟨⟨i0⟩⟩)
swap
· rw [vectorSpan_range_eq_span_range_vsub_right k p i0, ← Set.image_univ,
Finsupp.mem_span_image_iff_linearCombination]
rintro ⟨l, _, hv⟩
use insert i0 l.support
set w := (l : ι → k) - Function.update (Function.const ι 0 : ι → k) i0 (∑ i ∈ l.support, l i) with hwdef
use w
have hw : ∑ i ∈ insert i0 l.support, w i = 0 := by
rw [hwdef]
simp_rw [Pi.sub_apply, Finset.sum_sub_distrib, Finset.sum_update_of_mem (Finset.mem_insert_self _ _),
Finset.sum_insert_of_eq_zero_if_notMem Finsupp.notMem_support_iff.1]
simp only [Function.const_apply, Finset.sum_const_zero, add_zero, sub_self]
use hw
have hz : w i0 • (p i0 -ᵥ p i0 : V) = 0 := (vsub_self (p i0)).symm ▸ smul_zero _
change (fun i => w i • (p i -ᵥ p i0 : V)) i0 = 0 at hz
rw [Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ w p hw (p i0), Finset.weightedVSubOfPoint_apply, ←
hv, Finsupp.linearCombination_apply, @Finset.sum_insert_zero _ _ l.support i0 _ _ _ hz]
change (∑ i ∈ l.support, l i • _) = _
congr with i
by_cases h : i = i0
· simp [h]
· simp [hwdef, h]
· rw [Set.range_eq_empty, vectorSpan_empty, Submodule.mem_bot]
rintro rfl
use ∅
simp
· rintro ⟨s, w, hw, rfl⟩
exact weightedVSub_mem_vectorSpan hw p
