English
A weighted subtracted vector lies in the vector span of two affine combinations if and only if its weights are multiples of the difference of the two affine weights.
Русский
Вектор, полученный взвеcенной разностью, лежит в векторной оболочке пары аффинных комбинаций тогда и только тогда, когда веса кратны разности двух весов.
LaTeX
$$$\\text{(conditions on } p,w,w_1,w_2,s)\\;:\\; s.weightedVSub p w \\in \\operatorname{vectorSpan}\\big(k, \\{s.affineCombination k p w_1, s.affineCombination k p w_2\\}\\big) \\iff \\exists r\\in k,\\; \\forall i\\in s,\\ w_i = r\\,(w_2 i - w_1 i).$$$
Lean4
/-- Given an affinely independent family of points, a weighted subtraction lies in the
`vectorSpan` of two points given as affine combinations if and only if it is a weighted
subtraction with weights a multiple of the difference between the weights of the two points. -/
theorem weightedVSub_mem_vectorSpan_pair {p : ι → P} (h : AffineIndependent k p) {w w₁ w₂ : ι → k} {s : Finset ι}
(hw : ∑ i ∈ s, w i = 0) (hw₁ : ∑ i ∈ s, w₁ i = 1) (hw₂ : ∑ i ∈ s, w₂ i = 1) :
s.weightedVSub p w ∈ vectorSpan k ({s.affineCombination k p w₁, s.affineCombination k p w₂} : Set P) ↔
∃ r : k, ∀ i ∈ s, w i = r * (w₁ i - w₂ i) :=
by
rw [mem_vectorSpan_pair]
refine ⟨fun h => ?_, fun h => ?_⟩
· rcases h with ⟨r, hr⟩
refine ⟨r, fun i hi => ?_⟩
rw [s.affineCombination_vsub, ← s.weightedVSub_const_smul, ← sub_eq_zero, ← map_sub] at hr
have hw' : (∑ j ∈ s, (r • (w₁ - w₂) - w) j) = 0 := by
simp_rw [Pi.sub_apply, Pi.smul_apply, Pi.sub_apply, smul_sub, Finset.sum_sub_distrib, ← Finset.smul_sum, hw, hw₁,
hw₂, sub_self]
have hr' := h s _ hw' hr i hi
rw [eq_comm, ← sub_eq_zero, ← smul_eq_mul]
exact hr'
· rcases h with ⟨r, hr⟩
refine ⟨r, ?_⟩
let w' i := r * (w₁ i - w₂ i)
change ∀ i ∈ s, w i = w' i at hr
rw [s.weightedVSub_congr hr fun _ _ => rfl, s.affineCombination_vsub, ← s.weightedVSub_const_smul]
congr
