Helly number of a convex flag

This file formalizes Definition 3.7 and states Theorem 3.13 (Helly's theorem for convex flags). The maximum in hellyConstant is an actual bounded maximum: the cutoff is the number of integral points in all fibre polytopes, which is finite by local finiteness of the fibre lattices.

def EGZ.ConvexFlag.IntegralFiber (F : ConvexFlag) (x : F.Node) : Type

Integral points in one fibre polytope, before attaching the fibre as the base of a flag point.

Equations

• F.IntegralFiber x = { q : EGZ.RealCoord (F.rank x) // q ∈ (F.polytope x).carrier ∧ q ∈ F.lattice x }

@[instance_reducible]

noncomputable instance EGZ.ConvexFlag.integralFiberFintype (F : ConvexFlag) (x : F.Node) : Fintype (F.IntegralFiber x)

Equations

• F.integralFiberFintype x = ⋯.fintype

def EGZ.ConvexFlag.IntegralPointCode (F : ConvexFlag) : Type u_1

A finite code for all integral flag points.

Equations

• F.IntegralPointCode = ((x : F.Node) × F.IntegralFiber x)

@[instance_reducible]

noncomputable instance EGZ.ConvexFlag.integralPointCodeFintype (F : ConvexFlag) : Fintype F.IntegralPointCode

Equations

• F.integralPointCodeFintype = id inferInstance

def EGZ.ConvexFlag.integralPointEquiv (F : ConvexFlag) : { q : F.Point // q.IsIntegral } ≃ F.IntegralPointCode

Integral flag points are equivalent to their base together with their integral coordinate in that fibre.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance EGZ.ConvexFlag.integralPointFintype (F : ConvexFlag) : Fintype { q : F.Point // q.IsIntegral }

Equations

• F.integralPointFintype = Fintype.ofEquiv F.IntegralPointCode F.integralPointEquiv.symm

noncomputable def EGZ.ConvexFlag.integralPointCount (F : ConvexFlag) : ℕ

The number of integral points in all fibre polytopes. This counts the same real coordinate separately at different bases, as required for flag points.

Equations

• F.integralPointCount = Fintype.card { q : F.Point // q.IsIntegral }

structure EGZ.ConvexFlag.HellyIndependent {F : ConvexFlag} (Ω : F.ProperPointSet) {n : ℕ} (points : Fin n → F.Point) : Prop

A finite indexed family has the extremal property from Definition 3.7: its points are pairwise distinct proper integer points, and an integral convex combination of them must put coefficient one on one of the inputs.

The conclusion is deliberately about the coefficient, rather than merely about equality of the resulting flag point with an input; these conditions are not equivalent for flags.

• injective : Function.Injective points
• proper (i : Fin n) : points i ∈ Ω
• integral (i : Fin n) : (points i).IsIntegral
• only_trivial (weight : Fin n → ℝ) (result : F.Point) : ConvexCombination points weight result → result.IsIntegral → ∃ (i : Fin n), weight i = 1

theorem EGZ.ConvexFlag.HellyIndependent.card_le_integralPointCount {F : ConvexFlag} {Ω : F.ProperPointSet} {n : ℕ} {points : Fin n → F.Point} (h : HellyIndependent Ω points) : n ≤ F.integralPointCount

A Helly-independent family cannot have more members than there are integral flag points.

theorem EGZ.ConvexFlag.HellyIndependent.empty (F : ConvexFlag) (Ω : F.ProperPointSet) : HellyIndependent Ω fun (i : Fin 0) => i.elim0

The empty indexed family has the extremal property vacuously: no convex combination on an empty index type can have total weight one.

theorem EGZ.ConvexFlag.HellyIndependent.singleton {F : ConvexFlag} {Ω : F.ProperPointSet} {q : F.Point} (hqΩ : q ∈ Ω) (hqint : q.IsIntegral) : HellyIndependent Ω fun (x : Fin 1) => q

Every proper integral singleton is Helly-independent.

noncomputable def EGZ.ConvexFlag.hellyConstant {F : ConvexFlag} (Ω : F.ProperPointSet) : ℕ

Definition 3.7: the Helly constant of a convex flag with designated proper points.

Equations

• EGZ.ConvexFlag.hellyConstant Ω = Nat.findGreatest (fun (n : ℕ) => ∃ (points : Fin n → F.Point), EGZ.ConvexFlag.HellyIndependent Ω points) F.integralPointCount

theorem EGZ.ConvexFlag.hellyConstant_spec {F : ConvexFlag} (Ω : F.ProperPointSet) : ∃ (points : Fin (hellyConstant Ω) → F.Point), HellyIndependent Ω points

The defining maximum is attained.

theorem EGZ.ConvexFlag.HellyIndependent.card_le_hellyConstant {F : ConvexFlag} {Ω : F.ProperPointSet} {n : ℕ} {points : Fin n → F.Point} (h : HellyIndependent Ω points) : n ≤ hellyConstant Ω

Maximality of the Helly constant.

theorem EGZ.ConvexFlag.hellyConstant_le_integralPointCount {F : ConvexFlag} (Ω : F.ProperPointSet) : hellyConstant Ω ≤ F.integralPointCount

The Helly constant is bounded by the finite population of integral flag points.

theorem EGZ.ConvexFlag.hellyConstant_pos {F : ConvexFlag} {Ω : F.ProperPointSet} {q : F.Point} (hqΩ : q ∈ Ω) (hqint : q.IsIntegral) : 0 < hellyConstant Ω

A proper integral point forces the Helly constant to be positive.

def EGZ.ConvexFlag.HasCommonWeakHullPoint {F : ConvexFlag} (Ω : F.ProperPointSet) (ℱ : Set (Set F.Point)) : Prop

A proper integral point common to the weak hulls of a family of sets.

Equations

• EGZ.ConvexFlag.HasCommonWeakHullPoint Ω ℱ = ∃ q ∈ Ω, q.IsIntegral ∧ ∀ S ∈ ℱ, q ∈ F.weakConvexHull S

theorem EGZ.ConvexFlag.flagHelly {F : ConvexFlag} (Ω : F.ProperPointSet) (hnonempty : ∃ q ∈ Ω, q.IsIntegral) (ℱ : Set (Set F.Point)) (hlocal : ∀ (G : Finset (Set F.Point)), ↑G ⊆ ℱ → G.Nonempty → G.card ≤ hellyConstant Ω → HasCommonWeakHullPoint Ω ↑G) : HasCommonWeakHullPoint Ω ℱ

Theorem 3.13 (Helly): Helly's theorem for convex flags.

The family may be infinite. Only nonempty finite subfamilies of cardinality at most the Helly constant occur in the hypothesis; the separate existence assumption supplies the conclusion for an empty family.

theorem EGZ.ConvexFlag.theorem_3_13 {F : ConvexFlag} (Ω : F.ProperPointSet) (hnonempty : ∃ q ∈ Ω, q.IsIntegral) (ℱ : Set (Set F.Point)) (hlocal : ∀ (G : Finset (Set F.Point)), ↑G ⊆ ℱ → G.Nonempty → G.card ≤ hellyConstant Ω → HasCommonWeakHullPoint Ω ↑G) : HasCommonWeakHullPoint Ω ℱ

Numbered alias for Theorem 3.13.