English
A finsum version of the convex combination lies in a convex set when appropriate nonnegativity and sum-to-one conditions hold.
Русский
Версия для finsum: линейная комбинация из выпуклого множества принадлежит этому множеству при соответствующих условиях неотрицательности и нормализации.
LaTeX
$$finsum_mem$$
Lean4
/-- A version of `Convex.sum_mem` for `finsum`s. If `s` is a convex set, `w : ι → R` is a family of
nonnegative weights with sum one and `z : ι → E` is a family of elements of a module over `R` such
that `z i ∈ s` whenever `w i ≠ 0`, then the sum `∑ᶠ i, w i • z i` belongs to `s`. See also
`PartitionOfUnity.finsum_smul_mem_convex`. -/
theorem finsum_mem {ι : Sort*} {w : ι → R} {z : ι → E} {s : Set E} (hs : Convex R s) (h₀ : ∀ i, 0 ≤ w i)
(h₁ : ∑ᶠ i, w i = 1) (hz : ∀ i, w i ≠ 0 → z i ∈ s) : (∑ᶠ i, w i • z i) ∈ s :=
by
have hfin_w : (support (w ∘ PLift.down)).Finite := by
by_contra H
rw [finsum, dif_neg H] at h₁
exact zero_ne_one h₁
have hsub : support ((fun i => w i • z i) ∘ PLift.down) ⊆ hfin_w.toFinset :=
(support_smul_subset_left _ _).trans hfin_w.coe_toFinset.ge
rw [finsum_eq_sum_plift_of_support_subset hsub]
refine hs.sum_mem (fun _ _ => h₀ _) ?_ fun i hi => hz _ ?_
· rwa [finsum, dif_pos hfin_w] at h₁
· rwa [hfin_w.mem_toFinset] at hi
