Theorems · Theorem · convex and discrete geometry

Convex.finsum_mem

∀ {R : Type u_1} {E : Type u_3} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] {ι : Sort u_8} {w : ι → R} {z : ι → E} {s : Set E},
  Convex R s → (∀ (i : ι), 0 ≤ w i) → ∑ᶠ (i : ι), w i = 1 → (∀ (i : ι), w i ≠ 0 → z i ∈ s) → ∑ᶠ (i : ι), w i • z i ∈ s

A version of Convex.sum_mem for finsums. 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.

Defined in

Mathlib.Analysis.Convex.Combination

Cited by

3 results in Mathlib

Foundations

Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldAddCommGroupModuleLinearOrderIsStrictOrderedRing