4.3 Rozier–Terracol Lemma 2.3

Lemma 130

✓

Lean declarations:

X_T_iter_shift

For any \(j, m \in \mathbb {N}\), the parity of the iterates at \(m\) and \(m + 2^j\) are opposite:

\begin{equation} X(T^j(m)) + X(T^j(m + 2^j)) = 1. \end{equation}

Proof ▶

By the linear decomposition \(2^j T^j(n) = 3^{q} n + \mathcal{Q}_j(n)\), and the fact that \(V_j(m + 2^j) = V_j(m)\), we have \(T^j(m + 2^j) = T^j(m) + 3^q\). Since \(3^q\) is always odd, \(T^j(m + 2^j)\) and \(T^j(m)\) have opposite parity.

Lemma 131

✓

Lean declarations:

E_shift

The correction ratio \(E_j(n)\) is periodic with period \(2^j\):

\begin{equation} E_j(m + 2^j) = E_j(m). \end{equation}

Proof ▶

Since \(E_j(n)\) depends only on the parity vector \(V_j(n)\), and \(V_j(n)\) is periodic with period \(2^j\), the result follows.

Lemma 132

✓

Lean declarations:

E_succ_pair_sum

For any \(j, m \in \mathbb {N}\), we have the identity:

\begin{equation} E_{j+1}(m) + E_{j+1}(m + 2^j) = 2 E_j(m) + \frac{1}{2}. \end{equation}

Proof ▶

Using the recurrence \(E_{j+1}(n) = \frac{3^{X(T^j(n))}}{2} E_j(n) + \frac{X(T^j(n))}{2}\) and the shift properties:

\begin{align*} E_{j+1}(m) + E_{j+1}(m + 2^j) & = \frac{3^{X(T^j(m))} + 3^{X(T^j(m + 2^j))}}{2} E_j(m) + \frac{X(T^j(m)) + X(T^j(m + 2^j))}{2} \\ & = \frac{3^0 + 3^1}{2} E_j(m) + \frac{1}{2} \\ & = 2 E_j(m) + \frac{1}{2}. \end{align*}

Theorem 133 Rozier–Terracol Lemma 2.3

✓

Lean declarations:

CRoz_lemma_23

For every positive integer \(j\), the average value of the correction ratio \(E_j(n)\) over a full period is \(j/4\):

\begin{equation} \frac{1}{2^j} \sum _{n=1}^{2^j} E_j(n) = \frac{j}{4}. \end{equation}

Proof ▶

By induction on \(j\). For \(j=1\), the average is \((E_1(1) + E_1(2))/2 = (1/2 + 0)/2 = 1/4\). For the inductive step \(j+1\), we split the sum over \(\{ 1, \dots , 2^{j+1}\} \) into two halves and use Lemma 132:

\begin{align*} \sum _{n=1}^{2^{j+1}} E_{j+1}(n) & = \sum _{n=1}^{2^j} (E_{j+1}(n) + E_{j+1}(n + 2^j)) \\ & = \sum _{n=1}^{2^j} \left( 2 E_j(n) + \frac{1}{2} \right) \\ & = 2 \left( \frac{j}{4} \cdot 2^j \right) + \frac{2^j}{2} \\ & = \frac{j \cdot 2^j + 2^j}{2} = \frac{(j+1) 2^{j+1}}{4}. \end{align*}

Dividing by \(2^{j+1}\) yields \((j+1)/4\).