Upper bound for the irrationality measure of π

The irrationality measure of $\pi$ is at most the numeric bound in the formal statement. For every real $\varepsilon>0$, there is a natural threshold $Q$, uniform in the integer numerator $p$ and positive natural denominator $q\ge Q$, such that $1/q^{B+\varepsilon}<|\pi-p/q|$, where $B$ is that bound. Replace the formal placeholder with the entry value and give the theorem a unique Lean name.