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.