Intrinsic integer points and the polytope centerpoint statement

This file records the convex-geometric definitions from the introduction and the corrected formal statement of Theorem 1.12. The paper writes P ⊆ ℚ^d while simultaneously taking real convex combinations. We use the real realization and explicitly require the finite support of the weight to be rational. Without that requirement a finite set such as {0, 1, sqrt 2} need not lie in any discrete affine lattice, so the phrase "the lattice spanned by the support" would be undefined.

def EGZ.affineIntSpan {n : ℕ} (S : Set (RealCoord n)) : Set (RealCoord n)

The affine integer span of a set: finite integer affine combinations.

Equations

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

def EGZ.RationalPolytope.IsMinimalFaceAt {n : ℕ} (P : RationalPolytope n) (q : RealCoord n) (F : P.Face) : Prop

F is the minimal face of P containing q, expressed by the standard equivalent characterization that q lies in the relative interior of F. The order-theoretic characterization (every containing face also contains F) belongs in the finite-face API.

Equations

• P.IsMinimalFaceAt q F = (q ∈ F.relInterior)

def EGZ.RationalPolytope.IsIntrinsicInteger {n : ℕ} (P : RationalPolytope n) (q : RealCoord n) : Prop

Definition 1.7 (intpt): integrality is measured in the affine integer span of the vertices of the minimal face, not in an ambient fixed lattice.

Equations

• P.IsIntrinsicInteger q = ∃ (F : P.Face), P.IsMinimalFaceAt q F ∧ q ∈ EGZ.affineIntSpan (P.vertexSet ∩ F.carrier)

def EGZ.RationalPolytope.IsHollow {n : ℕ} (P : RationalPolytope n) : Prop

A hollow polytope has no intrinsic integer points other than vertices.

Equations

• P.IsHollow = ∀ q ∈ P.carrier, P.IsIntrinsicInteger q → q ∈ P.vertexSet

def EGZ.AdmitsHollowPolytopeVertexCount (d n : ℕ) : Prop

There is a hollow rational d-polytope with exactly n vertices.

Equations

• EGZ.AdmitsHollowPolytopeVertexCount d n = ∃ (P : EGZ.RationalPolytope d), P.IsHollow ∧ P.vertexSet.ncard = n

noncomputable def EGZ.hollowPolytopeNumber (d : ℕ) : ℕ

The paper's convex-geometric constant L(d), defined as a supremum. Finiteness/attainment will be supplied by the hollow-polytope theory.

Equations

• EGZ.hollowPolytopeNumber d = sSup {n : ℕ | EGZ.AdmitsHollowPolytopeVertexCount d n}

noncomputable def EGZ.totalWeight {n : ℕ} (w : RealCoord n → NNReal) : NNReal

Total mass of a finitely supported nonnegative weight.

Equations

• EGZ.totalWeight w = ∑ᶠ (q : EGZ.RealCoord n), w q

noncomputable def EGZ.upperHalfspaceWeight {n : ℕ} (w : RealCoord n → NNReal) (q : RealCoord n) (xi : RealCoord n →ᵃ[ℝ] ℝ) : NNReal

Weight on the closed affine halfspace through q selected by xi.

Equations

• EGZ.upperHalfspaceWeight w q xi = ∑ᶠ (x : EGZ.RealCoord n), if xi q ≤ xi x then w x else 0

def EGZ.IsCentral {n : ℕ} (w : RealCoord n → NNReal) (theta : NNReal) (q : RealCoord n) : Prop

A point is theta-central if every closed halfspace containing it has at least a theta fraction of the total weight. It suffices to test supporting halfspaces whose boundary passes through the point.

Equations

• EGZ.IsCentral w theta q = ∀ (xi : EGZ.RealCoord n →ᵃ[ℝ] ℝ), theta * EGZ.totalWeight w ≤ EGZ.upperHalfspaceWeight w q xi

def EGZ.PolytopeCenterpointConclusion {d : ℕ} (P : RationalPolytope d) (w : RealCoord d → NNReal) : Prop

The exact conclusion of Theorem 1.12.

Equations

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