Ehrhart volume inequality: Resolvent

Mollification, Green operator, and resolvent estimates.

theorem Ehrhart.TorusNoncompactBochner.complex_norm_sub_sq_le_two_mul_add (z w : ℂ) : ‖z - w‖ ^ 2 ≤ 2 * (‖z‖ ^ 2 + ‖w‖ ^ 2)

A quadratic bound for the norm of a difference of complex numbers.