Ehrhart volume inequality: Variation

Variational envelopes and torus analytic estimates.

theorem Ehrhart.MomentTargetDanskin.abs_exp_sub_one_le_mul_exp_abs (z : ℝ) : |Real.exp z - 1| ≤ |z| * Real.exp |z|

A first-order bound on the error of the real exponential.