ConvexCoverRegroup.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Regrouping a convex hull over a finite cover

For a finite family of nonempty sets, every point in the convex hull of their union is a convex combination with one point from each individual convex hull. The proof establishes convexity of the represented set. Zero coefficients are handled by choosing points inside the corresponding sets, without assuming that those sets contain the origin.

def OAI.Tingley.finiteMixtures line 24
Source documentation
Points represented by probability weights and one point in each member of a finite family of sets. Membership is required even at zero-weight indices.
```
def finiteMixtures (B : ι → Set E) : Set E :=
…
```
theorem OAI.Tingley.convex_finiteMixtures line 31
Source documentation
Mixing probability-weighted representations preserves representation when each coordinate set is convex. No nonemptiness premise is needed here.
```
theorem convex_finiteMixtures (B : ι → Set E) (hB : ∀ i, Convex ℝ (B i)) :
    Convex ℝ (finiteMixtures B) := by
…
```
Mentions: OAI.Tingley.finiteMixtures

theorem OAI.Tingley.convexHull_cover_representation line 60

Source documentation

Regroup a point of a convex hull along an arbitrary finite cover by nonempty sets. Cover members may be infinite, overlapping, or nonclosed.

theorem convexHull_cover_representation
    (H : Set E) (A : ι → Set E)
    (hne : ∀ i, (A i).Nonempty)
    (hcover : ∀ x ∈ H, ∃ i, x ∈ A i)
    {x : E} (hx : x ∈ convexHull ℝ H) :
    ∃ (w : ι → ℝ) (z : ι → E),
      (∀ i, 0 ≤ w i) ∧ (∑ i, w i) = 1 ∧
      (∀ i, z i ∈ convexHull ℝ (A i)) ∧
      (∑ i, w i • z i) = x := by
…