Square-root bounds for error estimates

Small reusable inequalities for square roots of nonnegative error terms.

theorem MIPStarRE.LDT.sqrt_add_le_add_sqrt {x y : Error} (hx : 0 ≤ x) (hy : 0 ≤ y) : √(x + y) ≤ √x + √y

Subadditivity of the square root on nonnegative error terms.

theorem MIPStarRE.LDT.sqrt_add3_le_add3_sqrt {x y z : Error} (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : 0 ≤ z) : √(x + y + z) ≤ √x + √y + √z

Three-term subadditivity of the square root on nonnegative error terms.