Effective SMB theorem for measures

Let $\mathbb A^\infty$ be the space of one-sided infinite sequences over the alphabet $A$, with shift operator $T$. Let $\mu$ be a computable ergodic $T$-invariant measure, and define

$$h^\mu_n(Z)=-\frac{1}{n}\log\mu[Z\upharpoonright_n].$$

Write $H(\mu)=\lim_n H_n(\mu)$ for the entropy of $\mu$, where

$$H_n(\mu)=-\frac{1}{n}\sum_{|w|=n}\mu[w]\log\mu[w].$$

Suppose that a measure $\rho$ is $\mu$-Martin-Löf absolutely continuous if $\rho(G_m)\to0$ for every $\mu$-Martin-Löf test $(G_m)_{m\in\mathbb N}$. Effective SMB theorem for measures. If $\rho$ is $\mu$-Martin-Löf absolutely continuous, then

$$\lim_n E_\rho h^\mu_n=H(\mu).$$

This extends the effective almost-sure Shannon–McMillan–Breiman conclusion from $\mu$-Martin-Löf random sequences to expectations with respect to measures absolutely continuous in the Martin-Löf sense. The supplied context identifies it as a special case of a conjecture from the 2017 Logic Blog; its resolution is not specified here.