Ehrhart volume inequality: Convergence #
The final concentration argument and Ehrhart volume inequality.
theorem
Ehrhart.Volume.ehrhart_volume_inequality_for_sets
{n : ℕ}
(hn : 0 < n)
(S : Set (Space n))
(hconvex : Convex ℝ S)
(hcompact : IsCompact S)
(hinterior : (interior S).Nonempty)
(hcentered : barycenter S = 0)
(hlattice : interiorLatticePoints S = {0})
:
Ehrhart's sharp volume inequality for a centered convex body with one interior lattice point.