Functional equation for $\mu$: $\mu(\sigma)=\mu(1-\sigma)-\sigma+\tfrac12$

For every real $\sigma$,

where $\mu(\sigma)=\inf\{a\in\mathbb R:\zeta(\sigma+iT)=O(T^{a})\}$ (as an extended real number).

This reflects the functional equation of $\zeta$ to the growth exponent; together with $\mu(\sigma)=0$ for $\sigma>1$ and convexity it determines $\mu$ outside the critical strip.

Formalization Note $\mu$ is LindelofHypothesis.mu, valued in the extended reals. The identity is stated in the extended reals; $-\sigma+\tfrac12$ is a finite real shift.