A fourth-power bound for clipping

For M > 0, clipping an element of a linearly ordered field to [-M, M] has squared error at most its fourth power divided by 16 M². The constant 1/16 is sharp, with equality at x = 2M. Integrating this pointwise estimate gives the fourth-moment clipping bound used in the Gaussian truncation proof of Grothendieck's inequality.

References

• F. Albiac and N. J. Kalton, Topics in Banach Space Theory, §8.1.

theorem TauCeti.sq_sub_max_min_le_pow_four_div {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {M : α} (hM : 0 < M) (x : α) : (x - max (-M) (min M x)) ^ 2 ≤ x ^ 4 / (16 * M ^ 2)

The pointwise fourth-moment estimate for clipping, with the sharp constant 1/16.