User:IssaRice/Formalizing adjustment of epsilons

I want to elaborate on a thing that shows up when proving part (a) of https://taoanalysis.wordpress.com/2020/05/24/exercise-5-6-1/

Actually, a similar thing appears in Tao's original proof (Proposition 5.5.12) and the situation is simpler there (fewer variables to deal with), so let's start there.

Tao's proof

In the first part of the proof, we suppose $x^2<2$, and let $0<\epsilon <1$. Then we show the bound $(x+\epsilon {)}^2\le x^2+5\epsilon$.