Vinogradov-type lemma with coprimality (source Lemma 3.4, interval form)

Lemma 3.4 in the form the Type I argument consumes, with the coprimality hypothesis restored.

Let $q\ge1$, let $A'\ge0$ and $B\ge0$, let $a'$ be an integer coprime to $q$, and let $\alpha'=\frac{a'}{q}+\beta'$ with $|\beta'|\le q^{-2}$. Then for all real $\theta'$ and all $u<v$,

with $\mathrm{vmin}(A',t)=A'$ at a vanishing phase and $\min(A',t)$ elsewhere.

This is the source's Lemma 3.4, stated over the integer interval $(\lfloor u\rfloor,\lfloor v\rfloor]$. It differs from the platform's TaoFivePrimes.vinogradov_lemma_if_form (which is false as stated — see the Accepted disproof) only by the added hypothesis $\gcd(|a'|,q)=1$; that hypothesis is part of the classical statement, since the source writes $\alpha=a/q$ with $a/q$ a reduced fraction, and it is exactly what prevents the phase from being constant modulo $\pi$.

The proof is the source's: subdivide the range into $\lfloor\frac{v-u}{q}\rfloor+1$ consecutive blocks of length $q$ and apply the block estimate on each. The subdivision half is already formalised and proved as TaoFivePrimes.vinogradov_lemma_if_form_from_block; this node is the assembly of that with the corrected block estimate TaoFivePrimes.vinogradov_block_coprime.

Formalization note. The hypotheses $A'\ge0$ and $B\ge0$ are needed: for $A'<0$ the left side has one term per integer in the interval while the right side only counts blocks of length $q$. The convention at the zeros of the sine is made explicit by an if, since Lean's real division returns $0$ there.