Lemma 29 — with prob. 1 − δ, |log posterior odds| ≤ 15τ√(2n log(2/δ))

Let $\theta$ be uniform on $\{-1,+1\}$ and let $(x_1,y_1),\dots,(x_n,y_n)$ be drawn independently from the one-dimensional $(\theta,\tau)$-Bernoulli model ($y_k$ uniform, $x_k=y_k\theta$ with probability $\tfrac12+\tau$, else $x_k=-y_k\theta$). Suppose $0<\tau\le\tfrac14$, $n\le 1/\tau^2$ and $\delta>0$. Then, with probability at least $1-\delta$ over the joint draw of $\theta$ and the samples $S$,

The lemma quantifies how little $n\le1/\tau^2$ samples reveal about a single sign $\theta$: the posterior stays close to uniform. Applied to each coordinate of $\theta^\star$ it controls the posterior means in the proof of Theorem 31.

Formalization Note The probability is a finite sum of the joint weights $\tfrac12\prod_k P_{\theta,\tau}(x_k,y_k)$ over $\theta$ and $S$. The hypothesis $\delta>0$ is added: at $\delta=0$ Lean's conventions $2/0=0$ and $\log 0=0$ would collapse the interval to $\{0\}$ and make the statement false. For $\delta\ge1$ the statement is trivially true, so no upper bound on $\delta$ is imposed.