I am dealing with the bounding of compression and decompression functions in CRYSTALS-Kyber, see the lemma in this post or the original reference KYBER, section 2.2 topic "Compression and Decompression".
I have not yet found a formal proof of the assertion and have tried to construct my own proof at this point.
As for the proof itself, I must note that I would like a correction. There are one or two places in it that might be relatively far-fetched. That is why I am asking here, hoping for constructive criticism of the proof.
Lemma: $$|x'-x \text{ mod}^{\pm} \, q| \leq \left\lceil \frac{q}{2^{d+1}} \right\rfloor,$$
where $x \in \mathbb{Z}_q$ and $x' = Decompress_q(Compress_q(x,d),d)$ and the Compression and Decompression functions are defined as:
$$Compress_q(x,d)= \lceil (2^d / q) \cdot x \rfloor \text{ mod}^+ \, 2^d$$ $$Decompress_q(x,d) = \lceil (q/2^d) \cdot x \rfloor$$
Proof:
For the proof we use the facts that $\lceil x \rfloor = x + \epsilon$, where $-\frac{1}{2} < \epsilon \leq \frac{1}{2}$ and $x$ is a rational number, together with $a \text{ mod } b = a - b \left\lfloor \frac{a}{b} \right\rfloor$ where $a$ and $b$ are integers.
\begin{align}
&|x'-x \text{ mod}^{\pm} \, q| \\
&=\left| \left\lceil \frac{q}{2^d} \left( \left\lceil \frac{2^d}{q}x \text{ mod}^{+} \, 2^d \right\rfloor \right) \right\rfloor - x \text{ mod}^{\pm} \, q \right| \\
&=\left| \left\lceil \frac{q}{2^d} \left( \frac{2^d}{q}x + \epsilon_1 \text{ mod}^{+} \, 2^d \right) \right\rfloor -x \text{ mod}^{\pm} \, q \right| \\
&=\left| \left\lceil \frac{q}{2^d} \left( \frac{2^d}{q}x - 2^d \left\lfloor \frac{x}{q} \right\rfloor + \epsilon_1 \right) \right\rfloor -x \text{ mod}^{\pm} \, q\right| \\
&=\left| \left\lceil x - q \left\lfloor \frac{x}{q} \right\rfloor + \frac{q}{2^d}\epsilon_1 \right\rfloor - x \text{ mod}^{\pm} \, q \right| \\
&=\left| x - q \left\lfloor \frac{x}{q} \right\rfloor + \frac{q}{2^d}\epsilon_1 + \epsilon_2 - x \text{ mod}^{\pm} \, q \right| \\
&=\left| - q \left\lfloor \frac{x}{q} \right\rfloor + \frac{q}{2^d}\epsilon_1 + \epsilon_2 \text{ mod}^{\pm} \, q \right| \\
&=\left| \frac{q}{2^d}\epsilon_1 + \epsilon_2 \text{ mod}^{\pm} \, q \right| \\
&=\left| \frac{q}{2^d}\epsilon_1 + \epsilon_2 \right| \\
&= \left\lceil \frac{q}{2^d} \epsilon_1 \right\rfloor \\
&\leq \left\lceil \frac{q}{2^{d+1}} \right\rfloor
\end{align}
For the inequality the fact that the absolute value of $\epsilon_1$ is at most $\frac{1}{2}$ was used.
