Convex closure for flag convex hulls

The flag convex hull is defined through finite relational convex combinations. This file proves the expected structural API, including the flattening of a convex combination of convex combinations. Strictly positive supports are used throughout, so the least-upper-bound base is preserved by flattening.

theorem EGZ.ConvexFlag.ConvexCombination.reindex {F : ConvexFlag} {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] {points : I → F.Point} {weight : I → ℝ} {result : F.Point} (c : ConvexCombination points weight result) (e : J ≃ I) : ConvexCombination (points ∘ ⇑e) (weight ∘ ⇑e) result

Reindex a convex combination along an equivalence of finite index types.

theorem EGZ.ConvexFlag.ConvexCombination.singleton {F : ConvexFlag} (q : F.Point) : ConvexCombination (fun (x : Fin 1) => q) (fun (x : Fin 1) => 1) q

The one-point convex combination.

theorem EGZ.ConvexFlag.subset_convexHull (F : ConvexFlag) (S : Set F.Point) : S ⊆ F.convexHull S

Every point of a set belongs to its flag convex hull.

theorem EGZ.ConvexFlag.convexHull_mono {F : ConvexFlag} {S T : Set F.Point} (hST : S ⊆ T) : F.convexHull S ⊆ F.convexHull T

Flag convex hull is monotone.

theorem EGZ.ConvexFlag.convexHull_convex_closed (F : ConvexFlag) (S : Set F.Point) : F.convexHull (F.convexHull S) ⊆ F.convexHull S

A convex combination of points which are themselves convex combinations can be flattened to one convex combination. The flattened index contains only pairs on which both coefficients are strictly positive; this makes its base exactly the iterated least upper bound.

theorem EGZ.ConvexFlag.convexHull_idempotent (F : ConvexFlag) (S : Set F.Point) : F.convexHull (F.convexHull S) = F.convexHull S

Flag convex hull is idempotent.