Read-back: Def_IntMul_HvdH_Resampling.lean

All declarations live in the namespace IntMul.HvdH. Only Mathlib is imported. Throughout, $\pi$ is the real number $\pi$, $i$ is the imaginary unit, $\exp$ is the real exponential unless it is applied to a complex argument.

Conventions used by every declaration

Index sets. For a natural number $n$, the index set is $\mathbb{Z}/n\mathbb{Z}$ (Mathlib's ZMod n). When $n \ge 1$ this is the finite ring of residues mod $n$; when $n = 0$ it is $\mathbb{Z}$ itself. A "vector in $\mathbb{C}^n$" is a function $u : \mathbb{Z}/n\mathbb{Z} \to \mathbb{C}$; indices are residues, so $u_j$ for any integer $j$ means $u_{j \bmod n}$. For a residue $x \in \mathbb{Z}/n\mathbb{Z}$ with $n \ge 1$, $\bar x \in \{0, 1, \dots, n-1\}$ denotes its canonical representative (Mathlib's ZMod.val). (For $n = 0$, val is the absolute value of the integer.) Whenever a formula below uses an index as a number, it is this canonical representative $\bar x$ that is used, not an arbitrary lift.

Norms. On $\mathbb{C}^n = (\mathbb{Z}/n\mathbb{Z} \to \mathbb{C})$ (with $n \ge 1$) Mathlib's norm is the supremum norm

$$\|u\| = \max_{j \in \mathbb{Z}/n\mathbb{Z}} |u_j|.$$

On continuous linear maps $L : \mathbb{C}^s \to \mathbb{C}^t$ the norm is the operator norm with respect to these sup norms,

$$\|L\| = \inf\{C \ge 0 : \|Lu\| \le C\|u\| \text{ for all } u\} = \sup_{\|u\| \le 1} \|Lu\|,$$

which for a matrix map equals the maximum over rows of the sum of absolute values of the row's entries. None of the declarations in this file mention a norm; this is only the structure the types carry.

Infinite sums. $\sum'$ denotes Mathlib's unconditional sum over $\mathbb{Z}$. For real-valued terms, it equals the usual sum when the series is absolutely summable, and it is defined to be $0$ when the series is not summable (no error is raised).

---

1. toCLM — the linear map of a matrix

Given natural numbers $s, t$ with $s \neq 0$ and $t \neq 0$ (both are required as hypotheses), and a complex $t \times s$ matrix $A$ whose rows are indexed by $\mathbb{Z}/t\mathbb{Z}$ and columns by $\mathbb{Z}/s\mathbb{Z}$, $\mathrm{toCLM}(A)$ is the continuous $\mathbb{C}$-linear map $\mathbb{C}^s \to \mathbb{C}^t$ given by matrix–vector multiplication:

$$\big(\mathrm{toCLM}(A)\,u\big)_k = \sum_{r \in \mathbb{Z}/s\mathbb{Z}} A_{k,r}\, u_r, \qquad k \in \mathbb{Z}/t\mathbb{Z}.$$

(The linear map is promoted to a continuous linear map using finite-dimensionality; nothing else changes.)

2. dft — the discrete Fourier transform

For $n \ge 1$, $\mathrm{dft}_n : \mathbb{C}^n \to \mathbb{C}^n$ is $\mathrm{toCLM}$ of the $n \times n$ matrix with entries

$$F_{j,k} = \frac{1}{n}\exp\!\Big(\frac{-2\pi i\, \bar j\, \bar k}{n}\Big), \qquad j, k \in \mathbb{Z}/n\mathbb{Z},$$

so

$$(\mathrm{dft}_n u)_j = \frac{1}{n}\sum_{k=0}^{n-1} e^{-2\pi i \bar j k / n}\, u_k.$$

Note the normalisation factor is $1/n$ (not $1/\sqrt n$) and the exponent has a minus sign. Because $e^{-2\pi i \bar j \bar k/n}$ only depends on $j, k$ mod $n$, using the canonical representatives does not matter here.

3. latticeMatrix — periodised kernel matrix

Inputs: natural numbers $s, t$ (no non-zero hypothesis) and a real-valued function $g : \mathbb{N} \times \mathbb{Z} \to \mathbb{R}$. Output: a complex matrix with rows indexed by $\mathbb{Z}/t\mathbb{Z}$ and columns by $\mathbb{Z}/s\mathbb{Z}$, with entries

$$L^{s,t}_g[k, r] = \sum'_{m \in \mathbb{Z}} g\big(\bar k,\ \bar r + m s\big) \in \mathbb{R} \subset \mathbb{C}.$$

The first argument of $g$ is the canonical representative $\bar k \in \{0,\dots,t-1\}$ of the row index; the second runs over the integers congruent to $\bar r$ mod $s$. Edge cases:

• If for some $(k, r)$ the series over $m$ is not (absolutely) summable, that entry is $0$.
• If $s = 0$ then $\bar r + m s = \bar r$ for all $m$, so each series is a constant series over $\mathbb{Z}$; it is summable only if the constant is $0$, hence every entry is $0$.
• Consequently, applying $\mathrm{toCLM}$ of this matrix to $u$ gives $\sum_{r} \big(\sum'_m g(\bar k, \bar r + ms)\big) u_r$; this coincides with "$\sum_{j \in \mathbb{Z}} g(\bar k, j)\, u_{j \bmod s}$" only when the per-residue series are summable.

4. resS — the Gaussian resampling map $\mathcal S$

For $s, t \ge 1$ and a real parameter $\alpha$ (no sign or non-zero hypothesis), $\mathcal{S}_{s,t,\alpha} : \mathbb{C}^s \to \mathbb{C}^t$ is $\mathrm{toCLM}$ of $\mathrm{latticeMatrix}$ with kernel

$$g(k, j) = \alpha^{-1}\exp\!\Big(-\pi\, \alpha^{-2}\, s^2 \Big(\frac{k}{t} - \frac{j}{s}\Big)^2\Big),$$

so the entry in row $k \in \mathbb{Z}/t\mathbb{Z}$, column $r \in \mathbb{Z}/s\mathbb{Z}$ is

$$\mathcal{S}[k,r] = \sum'_{m\in\mathbb{Z}} \alpha^{-1}\exp\!\Big(-\pi \alpha^{-2} s^2\Big(\frac{\bar k}{t} - \frac{\bar r + ms}{s}\Big)^2\Big) = \alpha^{-1}\sum_{m\in\mathbb{Z}} \exp\!\Big(-\pi \alpha^{-2} s^2\Big(\frac{\bar k}{t} - \frac{\bar r}{s} - m\Big)^2\Big),$$

and $(\mathcal S u)_k = \sum_{r \in \mathbb{Z}/s\mathbb{Z}} \mathcal S[k,r]\, u_r$. Divisions by $s$ and $t$ are real divisions by non-zero numbers. Edge cases:

• For $\alpha \neq 0$ the Gaussian series is summable, so the sum is a genuine sum.
• For $\alpha = 0$, Mathlib's convention $0^{-1} = 0$ makes $g \equiv 0$, so $\mathcal S$ is the zero map.
• For $\alpha < 0$ the prefactor $\alpha^{-1}$ is negative while $\alpha^{-2} > 0$; thus $\mathcal S_{s,t,\alpha} = -\mathcal S_{s,t,-\alpha}$.
• $s = t$ is allowed.

5. resT — the Gaussian resampling map $\mathcal T$

For $s, t \ge 1$ and real $\alpha$ (no hypothesis), $\mathcal{T}_{s,t,\alpha} : \mathbb{C}^s \to \mathbb{C}^t$ is $\mathrm{toCLM}$ of $\mathrm{latticeMatrix}$ with kernel

$$g(k, j) = \exp\!\Big(-\pi\, \alpha^{2}\, t^2 \Big(\frac{k}{t} - \frac{j}{s}\Big)^2\Big),$$

i.e. entries

$$\mathcal{T}[k,r] = \sum'_{m\in\mathbb{Z}} \exp\!\Big(-\pi \alpha^{2} t^2\Big(\frac{\bar k}{t} - \frac{\bar r}{s} - m\Big)^2\Big), \qquad k \in \mathbb{Z}/t\mathbb{Z},\ r \in \mathbb{Z}/s\mathbb{Z}.$$

There is no $\alpha$ prefactor. Edge cases:

• For $\alpha \neq 0$ the series is summable.
• For $\alpha = 0$ every term equals $1$, the series over $\mathbb{Z}$ is not summable, so every entry is $0$ and $\mathcal T$ is the zero map.
• $\mathcal T$ depends on $\alpha$ only through $\alpha^2$, so $\mathcal T_{\alpha} = \mathcal T_{-\alpha}$.
• Since shifting $\bar k$ by $t$ is absorbed by re-indexing $m$, the entry formula would give the same value for any integer lift of $k$.

6. permS — the map $\mathcal P_s$

For $s \ge 1$ and any natural number $t$ (no hypothesis on $t$), $\mathcal P_s : \mathbb{C}^s \to \mathbb{C}^s$ is precomposition with multiplication by $t$ in $\mathbb{Z}/s\mathbb{Z}$:

$$(\mathcal P_s u)_j = u_{t j \bmod s}, \qquad j \in \mathbb{Z}/s\mathbb{Z}.$$

It is linear for every $t$; it is a permutation of coordinates exactly when multiplication by $t$ is a bijection of $\mathbb{Z}/s\mathbb{Z}$, i.e. when $\gcd(s,t) = 1$. No coprimality is assumed. If $t \equiv 0 \pmod s$ (e.g. $t = 0$ or $t = s$), $(\mathcal P_s u)_j = u_0$ for all $j$.

7. permT — the map $\mathcal P_t$

For $t \ge 1$ and any natural number $s$ (no hypothesis on $s$), $\mathcal P_t : \mathbb{C}^t \to \mathbb{C}^t$ is

$$(\mathcal P_t u)_k = u_{-s k \bmod t}, \qquad k \in \mathbb{Z}/t\mathbb{Z}.$$

Again no coprimality is assumed; it is a coordinate permutation exactly when $\gcd(s,t)=1$, and if $s \equiv 0 \pmod t$ it sends $u$ to the constant vector $u_0$.

8. nearest — nearest integer

For real $x$,

$$[x] = \lfloor x + \tfrac12 \rfloor \in \mathbb{Z}.$$

Ties round up: $[\tfrac12] = 1$, $[-\tfrac12] = 0$, $[n + \tfrac12] = n+1$. It satisfies $x - \tfrac12 < [x] \le x + \tfrac12$.

9. beta

For natural numbers $s, t$ (no hypotheses) and an integer $\ell$,

$$\beta_\ell = \frac{t\ell}{s} - \Big[\frac{t\ell}{s}\Big],$$

computed in the reals as $(t \cdot \ell)/s$. Its value always lies in $[-\tfrac12, \tfrac12)$. Edge case: if $s = 0$, real division by zero returns $0$, so $\beta_\ell = 0 - [0] = 0$ for every $\ell$.

10. rowDel — the row-deleting map $\mathcal C$

For $s, t \ge 1$, $\mathcal C : \mathbb{C}^t \to \mathbb{C}^s$ is $\mathrm{toCLM}$ of the $s \times t$ $0/1$ matrix (rows $\ell \in \mathbb{Z}/s\mathbb{Z}$, columns $k \in \mathbb{Z}/t\mathbb{Z}$)

$$C[\ell, k] = \begin{cases} 1 & \text{if } k \equiv \big[t \bar\ell / s\big] \pmod t,\\ 0 & \text{otherwise,}\end{cases}$$

so

$$(\mathcal C u)_\ell = u_{\,[t\bar\ell/s] \bmod t}, \qquad \bar\ell \in \{0, \dots, s-1\}.$$

Each row has exactly one $1$. The nearest-integer value $[t\bar\ell/s]$ lies in $\{0, \dots, t\}$; it can equal $t$ (when $\bar\ell = s-1$ and $t/s \le 1/2$), in which case it is reduced to the index $0$. No relation between $s$ and $t$ is assumed; if $t < s$, distinct $\ell$ may pick the same coordinate.

11. diagD — the diagonal map $\mathcal D$

For $s \ge 1$, any natural $t$, and real $\alpha$, $\mathcal D : \mathbb{C}^s \to \mathbb{C}^s$ is $\mathrm{toCLM}$ of the diagonal matrix

$$\mathcal D = \operatorname{diag}(d_\ell)_{\ell \in \mathbb{Z}/s\mathbb{Z}}, \qquad d_\ell = \exp\!\big(\pi \alpha^2 \beta_{\bar\ell}^{\,2}\big),$$

where $\beta_{\bar\ell}$ is item 9 with the same $s, t$ evaluated at the canonical representative $\bar\ell \in \{0,\dots,s-1\}$. So $(\mathcal D u)_\ell = d_\ell u_\ell$. The real numbers $d_\ell$ satisfy $1 \le d_\ell \le e^{\pi\alpha^2/4}$. If $\alpha = 0$, $\mathcal D$ is the identity. (The toCLM call carries the hypothesis that $s \ne 0$ for both index sets, which holds.)

12. normN — the map $\mathcal N$

For $s, t \ge 1$ and real $\alpha$,

$$\mathcal N = \mathcal C \circ \mathcal T_{s,t,\alpha} \circ \mathcal D : \mathbb{C}^s \to \mathbb{C}^s,$$

with $\mathcal C$ from item 10, $\mathcal T$ from item 5 and $\mathcal D$ from item 11 (all with the same $s, t, \alpha$). Explicitly, writing $\kappa_\ell \in \{0,\dots,t-1\}$ for the canonical representative of $[t\bar\ell/s] \bmod t$,

$$(\mathcal N u)_\ell = \sum_{r \in \mathbb{Z}/s\mathbb{Z}} \Big(\sum'_{m \in \mathbb{Z}} \exp\!\Big(-\pi\alpha^2 t^2\Big(\frac{\kappa_\ell}{t} - \frac{\bar r}{s} - m\Big)^2\Big)\Big)\, e^{\pi\alpha^2\beta_{\bar r}^2}\, u_r.$$

Edge case: for $\alpha = 0$, $\mathcal T = 0$ (item 5), hence $\mathcal N = 0$.

13. errE — the map $\mathcal E$

For $s, t \ge 1$ and real $\alpha$,

$$\mathcal E = \mathcal N - \mathcal I : \mathbb{C}^s \to \mathbb{C}^s,$$

where $\mathcal I$ is the identity map of $\mathbb{C}^s$; i.e. $\mathcal E u = \mathcal N u - u$. For $\alpha = 0$, $\mathcal E = -\mathcal I$.

14. theta

For natural numbers $s, t$ (no hypotheses),

$$\theta = \frac{t}{s} - 1 \in \mathbb{R}.$$

Edge case: if $s = 0$, real division by zero gives $t/0 = 0$, so $\theta = -1$. If $s = t \ge 1$, $\theta = 0$; no sign of $\theta$ is assumed.