Exact power and least sample size for a known-variance normal z-test

By [A1], countable choice is available for the Borel-measurability supplier in [F5]. The affine statistic $x\mapsto \sqrt{n}(x-{\mu }_0)\mathrm{/}\sigma$ is continuous, so the strict upper-level rejection set is Borel and its indicator is measurable. [F5] therefore makes ${\phi }_n$ a randomized-test function in the sample-mean experiment described by [F3]; [F1] gives its statistic the stated shifted normal law.

Write ${\lambda }_{\mu }=\sqrt{n}(\mu -{\mu }_0)\mathrm{/}\sigma$. Under parameter $\mu$, the rejection probability is $1-\mathrm{\Phi }(z_{1-\alpha }-{\lambda }_{\mu })=\mathrm{\Phi }({\lambda }_{\mu }-z_{1-\alpha })$ by the symmetry in [F2]. This is the stated power function.

On $H_0$, ${\lambda }_{\mu }\le 0$. Since $\mathrm{\Phi }$ is strictly increasing, the power in step 2.1 is increasing in $\mu$, so its supremum over $\mu \le {\mu }_0$ occurs at ${\mu }_0$. There it equals $\mathrm{\Phi }(-z_{1-\alpha })=\mathrm{\Phi }(z_{\alpha })=\alpha$ by [F2]; hence the test size is $\alpha$.

At ${\mu }_1={\mu }_0+\delta$, target power is attained exactly when $\mathrm{\Phi }(\delta \sqrt{n}\mathrm{/}\sigma -z_{1-\alpha })\ge \mathrm{\Phi }(z_{1-{\beta }_{\mathrm{I}\mathrm{I}}})$. Strict increase of $\mathrm{\Phi }$ makes this equivalent to $\delta \sqrt{n}\mathrm{/}\sigma \ge q$, where $q=z_{1-\alpha }+z_{1-{\beta }_{\mathrm{I}\mathrm{I}}}$. If $q\le 0$, the left side is positive for every $n\ge 1$, so all positive sizes qualify. If $q>0$, the condition is $n\ge (\sigma \mathrm{/}\delta {)}^2{q}^2$.

For $q\le 0$, the least positive size is $1$, which agrees with the displayed formula. For $q>0$, [F8] makes the least integer at least $(\sigma \mathrm{/}\delta {)}^2{q}^2$ its ceiling, already positive. The cases in step 3.2 make the target-feasible set nonempty; step 3.1 shows that every candidate size satisfies the size constraint $s_n=\alpha$. Thus the target-feasible sizes are exactly the plans meeting the test request, and [F7] identifies their least size with the planning rule's output. The unified expression is the stated $n_{\ast }$.