Weak convex hulls of flag points

This is Definition 3.10 and the elementary closure API around equation wcabsorb. Proposition 3.11, the finite weak-hull/projection characterization, is stated as the geometric proof target.

def EGZ.ConvexFlag.weakConvexHull (F : ConvexFlag) (S : Set F.Point) : Set F.Point

The weak convex hull of S: every flag functional defined at q has a defined point of S on the same or higher side.

Equations

• F.weakConvexHull S = {q : F.Point | ∀ (xi : F.LinearFunction) (hq : xi.EvaluableAt q), ∃ s ∈ S, ∃ (hs : xi.EvaluableAt s), xi.eval q hq ≤ xi.eval s hs}

theorem EGZ.ConvexFlag.mem_weakConvexHull_iff {F : ConvexFlag} {S : Set F.Point} {q : F.Point} : q ∈ F.weakConvexHull S ↔ ∀ (xi : F.LinearFunction) (hq : xi.EvaluableAt q), ∃ s ∈ S, ∃ (hs : xi.EvaluableAt s), xi.eval q hq ≤ xi.eval s hs

theorem EGZ.ConvexFlag.subset_weakConvexHull (F : ConvexFlag) (S : Set F.Point) : S ⊆ F.weakConvexHull S

Weak convex hull is extensive.

theorem EGZ.ConvexFlag.weakConvexHull_mono {F : ConvexFlag} {A B : Set F.Point} (hAB : A ⊆ B) : F.weakConvexHull A ⊆ F.weakConvexHull B

Monotonicity of weak convex hull.

theorem EGZ.ConvexFlag.weakConvexHull_absorb {F : ConvexFlag} {A B : Set F.Point} (hAB : A ⊆ F.weakConvexHull B) : F.weakConvexHull A ⊆ F.weakConvexHull B

Absorption, equation wcabsorb in the paper.

theorem EGZ.ConvexFlag.weakConvexHull_idempotent (F : ConvexFlag) (S : Set F.Point) : F.weakConvexHull (F.weakConvexHull S) = F.weakConvexHull S

Weak convex hull is idempotent.

theorem EGZ.ConvexFlag.LinearFunction.eval_eq_of_projection {F : ConvexFlag} (xi : F.LinearFunction) (q q' : F.Point) (hbase : q'.base ≤ q.base) (hval : q.val = q'.coord hbase) (hq : xi.EvaluableAt q) : xi.eval q hq = xi.eval q' ⋯

Evaluation is unchanged by projection. This packages the cocycle calculation used throughout the proof of Flag Helly.

theorem EGZ.ConvexFlag.ConvexCombination.eval_eq {F : ConvexFlag} {I : Type u_1} [Fintype I] {points : I → F.Point} {weight : I → ℝ} {result : F.Point} (c : ConvexCombination points weight result) (xi : F.LinearFunction) (hxi : xi.EvaluableAt result) : xi.eval result hxi = ∑ i : { i : I // 0 < weight i }, weight ↑i * xi.eval (points ↑i) ⋯

An affine functional takes a flag-convex combination to the weighted average of its values on the positive support.

theorem EGZ.ConvexFlag.mem_weakConvexHull_iff_exists_projection {F : ConvexFlag} {S : Set F.Point} (hS : S.Finite) (q : F.Point) : q ∈ F.weakConvexHull S ↔ ∃ q' ∈ F.convexHull S, q.IsProjectionOf q'

Proposition 3.11 (pf1): for finite input, weak hull means projection of an ordinary flag-convex combination.

def EGZ.ConvexFlag.WeaklyConvexPosition (F : ConvexFlag) (S : Set F.Point) : Prop

No member of S lies in the weak hull of the remaining members.

Equations

• F.WeaklyConvexPosition S = ∀ q ∈ S, q ∉ F.weakConvexHull (S \ {q})