English
The membership of a point q in the affine span of the range p is equivalent to the existence of a finite subset s and weights w such that q equals the weightedVSubOfPoint expression with base point p_j.
Русский
Членство точки q в афинном span эквивалентно существованию конечного множества s и весов w, для которых q равно выражению weightedVSubOfPoint с базовой точкой p_j.
LaTeX
$$$q = s.weightedVSubOfPoint p (p j) w +\!_v p j$$$
Lean4
/-- A point in the `affineSpan` of an indexed family is an
`affineCombination` with sum of weights 1. See also
`eq_affineCombination_of_mem_affineSpan_of_fintype`. -/
theorem eq_affineCombination_of_mem_affineSpan {p1 : P} {p : ι → P} (h : p1 ∈ affineSpan k (Set.range p)) :
∃ (s : Finset ι) (w : ι → k), ∑ i ∈ s, w i = 1 ∧ p1 = s.affineCombination k p w := by
classical
have hn : (affineSpan k (Set.range p) : Set P).Nonempty := ⟨p1, h⟩
rw [affineSpan_nonempty, Set.range_nonempty_iff_nonempty] at hn
obtain ⟨i0⟩ := hn
have h0 : p i0 ∈ affineSpan k (Set.range p) := mem_affineSpan k (Set.mem_range_self i0)
have hd : p1 -ᵥ p i0 ∈ (affineSpan k (Set.range p)).direction := AffineSubspace.vsub_mem_direction h h0
rw [direction_affineSpan, mem_vectorSpan_iff_eq_weightedVSub] at hd
rcases hd with ⟨s, w, h, hs⟩
let s' := insert i0 s
let w' := Set.indicator (↑s) w
have h' : ∑ i ∈ s', w' i = 0 := by rw [← h, Finset.sum_indicator_subset _ (Finset.subset_insert i0 s)]
have hs' : s'.weightedVSub p w' = p1 -ᵥ p i0 := by
rw [hs]
exact (Finset.weightedVSub_indicator_subset _ _ (Finset.subset_insert i0 s)).symm
let w0 : ι → k := Function.update (Function.const ι 0) i0 1
have hw0 : ∑ i ∈ s', w0 i = 1 :=
by
rw [Finset.sum_update_of_mem (Finset.mem_insert_self _ _)]
simp only [Function.const_apply, Finset.sum_const_zero, add_zero]
have hw0s : s'.affineCombination k p w0 = p i0 :=
s'.affineCombination_of_eq_one_of_eq_zero w0 p (Finset.mem_insert_self _ _) (Function.update_self ..) fun _ _ hne =>
Function.update_of_ne hne _ _
refine ⟨s', w0 + w', ?_, ?_⟩
· simp [Pi.add_apply, Finset.sum_add_distrib, hw0, h']
· rw [add_comm, ← Finset.weightedVSub_vadd_affineCombination, hw0s, hs', vsub_vadd]
