Ehrhart volume inequality: Foundations

Foundational convex, lattice, Bergman, and variational constructions.

@[reducible, inline]

abbrev Ehrhart.Space (n : ℕ) : Type

The ambient real vector space in dimension n.

Equations

• Ehrhart.Space n = (Fin n → ℝ)

def Ehrhart.integerPoint (n : ℕ) (z : Fin n → ℤ) : Space n

The real point associated to an integer lattice vector.

Equations

• Ehrhart.integerPoint n z i = ↑(z i)

def Ehrhart.standardSimplex (n : ℕ) : Set (Space n)

The standard closed simplex.

Equations

• Ehrhart.standardSimplex n = {x : Ehrhart.Space n | (∀ (i : Fin n), 0 ≤ x i) ∧ ∑ i : Fin n, x i ≤ 1}

def Ehrhart.simplexDilation (n : ℕ) (x : Space n) : Space n

The affine dilation taking the standard simplex to its centered extremal form.

Equations

• Ehrhart.simplexDilation n x i = (↑n + 1) * x i - 1

def Ehrhart.centeredSimplex (n : ℕ) : Set (Space n)

The centered simplex that attains the sharp Ehrhart volume bound.

Equations

• Ehrhart.centeredSimplex n = Ehrhart.simplexDilation n '' Ehrhart.standardSimplex n

noncomputable def Ehrhart.normalizedVolume {n : ℕ} (K : Set (Space n)) : ℝ

Euclidean volume, converted from ℝ≥0∞ to ℝ.

Equations

• Ehrhart.normalizedVolume K = (MeasureTheory.volume K).toReal

noncomputable def Ehrhart.barycenter {n : ℕ} (K : Set (Space n)) : Space n

The volume-normalized barycenter of a measurable body.

Equations

• Ehrhart.barycenter K = (Ehrhart.normalizedVolume K)⁻¹ • ∫ (x : Ehrhart.Space n) in K, x

def Ehrhart.interiorLatticePoints {n : ℕ} (K : Set (Space n)) : Set (Fin n → ℤ)

The integer lattice points lying in the interior of a body.

Equations

• Ehrhart.interiorLatticePoints K = {z : Fin n → ℤ | Ehrhart.integerPoint n z ∈ interior K}

structure Ehrhart.CenteredBody (n : ℕ) : Type

A compact full-dimensional convex body centered at its unique interior lattice point.

• carrier : Set (Space n)

  The underlying point set.

• convex : Convex ℝ self.carrier

  Convexity of the body.

• compact : IsCompact self.carrier

  Compactness of the body.

• fullDimensional : (interior self.carrier).Nonempty

  Nonempty interior.

• centered : barycenter self.carrier = 0

  The body has barycenter zero.

• uniqueInteriorLatticePoint : interiorLatticePoints self.carrier = {0}

  The origin is the unique interior lattice point.

noncomputable def Ehrhart.sharpConstant (n : ℕ) : ℝ

The sharp volume constant in dimension n.

Equations

• Ehrhart.sharpConstant n = (↑n + 1) ^ n / ↑n.factorial

theorem Ehrhart.SimplexVolume.normalizedVolume_centeredSimplex (n : ℕ) : normalizedVolume (centeredSimplex n) = sharpConstant n

The centered simplex has exactly the sharp normalized volume.

theorem Ehrhart.SimplexVolume.barycenter_centeredSimplex (n : ℕ) : barycenter (centeredSimplex n) = 0

The centered simplex has barycenter zero.

theorem Ehrhart.SimplexVolume.exists_centeredBody_sharp (n : ℕ) (hn : 0 < n) : ∃ (K : CenteredBody n), normalizedVolume K.carrier = sharpConstant n

A centered body attaining the sharp volume bound exists in every positive dimension.

Normalising a function at a minimiser: x ↦ g (x + z) - g z. Both the smooth source potential of MomentCoercivityCompactness and the target geodesic of MomentTargetGeodesicVariation are normalised this way at their minimum points, and the facts below are shared by the two.