Products of nearby reals #
If x and y are each within e of a nonnegative q, their product is within
e (2q + e) of q²: the quantitative form of continuity of multiplication used when a measure is
compared with its own square. Stated for any linearly ordered commutative ring.
theorem
TauCeti.abs_mul_sub_mul_self_le
{R : Type u_1}
[CommRing R]
[LinearOrder R]
[IsStrictOrderedRing R]
{x y q e : R}
(hx : |x - q| ≤ e)
(hy : |y - q| ≤ e)
(hq0 : 0 ≤ q)
:
|x y - q²| ≤ e (2q + e) when x and y are each within e of q ≥ 0; neither x nor
y need be nonnegative.