Prefix sums of the lifted sequence: the first $L$ entries sum to $(L \bmod m_1) + M\lfloor L/m_1 \rfloor$

This lemma computes the prefix sums of the lifted sequence exactly.

Let $m_1 \ge 1$, $m_2$ and $M \ge m_1$ be natural numbers, and let $x_L = (L \bmod m_1) + M \lfloor L/m_1 \rfloor$ for $L \in \mathbb{N}$. Let $A = (a_1, \dots, a_{m_1 m_2 - 1})$ be the lifted sequence of the Lift bundle, with $a_i = x_i - x_{i-1}$; it is the sequence of jumps of the grid $X = \{u + Mj : 0 \le u \le m_1 - 1,\ 0 \le j \le m_2 - 1\}$. Then for every $L$ with $0 \le L \le m_1 m_2 - 1$, the sum of the first $L$ entries of $A$ is

For $L = 0$ both sides are $0$.

The formula identifies the prefix sums of $A$ with the elements of the grid $X$. It is the fourth part of the lift lemma, and it gives the bound on the prefix averages of $A$ that the lower bound $L(n) \ge m_1 m_2$ needs.

Formalization Note "The first $L$ entries" is List.take L, and $m_1 m_2 - 1$ is truncated subtraction on $\mathbb{N}$. There is no hypothesis on $m_2$; for $m_2 = 0$ only $L = 0$ is allowed.