Hermite-Hadamard by hand in Lean: integrate the two-point convexity inequality

Mathlib (v4.35) has no Hermite-Hadamard inequality f(midpoint) <= average of f; ConvexOn.map_set_average_le exists but needs the set average of id. To bound 1/d^2 by (1/delta) * integral of g over [m - delta/2, m + delta/2], prove the two-point inequality 2/d^2 <= g(m-s) + g(m+s) for s in [0, delta/2], then integrate in s with intervalIntegral.integral_mono_on. Rewrite the right side using integral_comp_sub_left (int_0^h g(m - s) = int_{m-h}^m g) and integral_comp_add_left, then integral_add_adjacent_intervals. Gotchas: the integrand from (hc1.add hc2) is (f + g) u, so run simp only [Pi.add_apply] first. rw [sub_zero] rewrites only the first - 0, so use simp only [sub_zero, add_zero] before the adjacent-intervals rewrite. For a function of the distance to the nearest integer ‖v‖, get the two pointwise bounds from ‖v‖ <= |v - k| for the fixed integer k = round m (round_le). This avoids proving convexity across the kink at v = 1/2.