Average Grover success for a uniform integer iteration count

Since $0<a\le 1\mathrm{/}2$, [F7] gives a nonnegative root and [F11] gives $0<\sqrt{a}<1$. By [F4], $\sin \theta =\sqrt{a}$. Since $\sin 0=0$ by [F8] and sine is strictly increasing by [F10], $\theta >0$. Also $\sin (\pi \mathrm{/}2)=1$ by [F9], so strict increase and $\sin \theta <1$ give $\theta <\pi \mathrm{/}2$; hence $\cos \theta >0$ by [F10]. The Pythagorean identity [F5] gives $\cos \theta =\sqrt{1-a}$.

Using [F1] and the identity ${\sin }^{2}x=(1-\cos 2x)\mathrm{/}2$ from [F3], the average is $\frac{1}{2}-\frac{1}{2K}{\sum }_{j=0}^{K-1}\cos ((4j+2)\theta )$.

For each $j$, [F2] gives $2\sin (2\theta )\cos ((4j+2)\theta )=\sin ((4j+4)\theta )-\sin (4j\theta )$. Summing from $j=0$ to $K-1$ telescopes to ${\sum }_{j=0}^{K-1}\cos ((4j+2)\theta )=\sin (4K\theta )\mathrm{/}(2\sin (2\theta ))$. Substitution in step 1.2 proves the displayed identity.

Since $1-a\ge 1\mathrm{/}2$, [F11] gives $\sqrt{1-a}\ge 1\mathrm{/}\sqrt{2}$. By [F3] and step 1.1, $\sin (2\theta )=2\sqrt{a}\sqrt{1-a}\ge \sqrt{2a}$. Hence $K\sin (2\theta )\ge \sqrt{2}$ by [F6]. The absolute value of the correction term in step 2.1 is at most $1\mathrm{/}(4\sqrt{2})<1\mathrm{/}4$, so the average is at least $1\mathrm{/}4$.