Random Fourier Rotation estimator

rotation2

For a real number $\theta$, rotation2 θ is the $2\times 2$ real matrix

$$R(\theta) = \begin{pmatrix} \cos\theta & -\sin\theta \\ \sin\theta & \cos\theta \end{pmatrix},$$

with rows and columns indexed by Fin 2 (i.e. by $\{0,1\}$). No hypothesis is placed on $\theta$: it ranges over all of $\mathbb{R}$, with no restriction to an interval such as $[0,2\pi)$.

featurePair

Fix a natural number $n$ and a vector $v : \mathrm{Fin}(2n) \to \mathbb{R}$, thought of as a function assigning a real value to each index $0,1,\dots,2n-1$. For $j$ ranging over Fin n (i.e. $j \in \{0,1,\dots,n-1\}$), featurePair n v j is the 2-element vector

$$\big(v(2j),\, v(2j+1)\big),$$

indexed by Fin 2. This is defined for every $j < n$; the Lean proof obligation attached to the definition merely certifies that $2j$ and $2j+1$ are valid indices into $v$ (both are $< 2n$) and carries no further mathematical content. When $n = 0$, Fin n is empty, so there is no valid $j$ and the function has no inputs to apply to; correspondingly $v$ itself has type $\mathrm{Fin}(0) \to \mathbb{R}$, the empty (zero-dimensional) domain, carrying no data.

pairNorm

For an arbitrary vector $v : \mathrm{Fin}(2) \to \mathbb{R}$ (not required to arise from featurePair, or from any other construction — any pair of reals), pairNorm v is the ordinary Euclidean norm

$$\|v\| = \sqrt{v(0)^2 + v(1)^2}.$$

This definition is stated on its own and is not invoked anywhere inside rfrEstimator below; nothing in the file connects pairNorm to the estimator.

rfrEstimator

Fix $n \in \mathbb{N}$; two vectors $q, k : \mathrm{Fin}(2n) \to \mathbb{R}$ (the "query" and "key," each with $2n$ real coordinates, indexed $0,\dots,2n-1$, with no constraint such as boundedness or normalization); two real numbers $p_m, p_n \in \mathbb{R}$ (arbitrary reals, not restricted to be nonnegative, integer-valued, or distinct from one another); and a function $\xi : \mathrm{Fin}(n) \to \mathbb{R}$ assigning a real number $\xi_j$ to each $j \in \{0,\dots,n-1\}$. No hypothesis whatsoever is imposed on $\xi$ — the $\xi_j$ are arbitrary reals, with no assumption of positivity, distinctness, boundedness, or of being drawn from any probability distribution.

For each $j$, write $q_j = \big(q(2j), q(2j+1)\big)$ and $k_j = \big(k(2j), k(2j+1)\big)$ for the $j$-th feature pairs of $q$ and $k$ (as produced by featurePair), and set

$$\theta^{(m)}_j = 2\pi\,\xi_j\, p_m, \qquad \theta^{(n)}_j = 2\pi\,\xi_j\, p_n .$$

The quantity rfrEstimator n q k pm pn ξ is defined as

$$\hat g(q,k,p_m,p_n) \;=\; \sum_{j=0}^{n-1} \Big\langle\, R(\theta^{(m)}_j)\, q_j,\; R(\theta^{(n)}_j)\, k_j \,\Big\rangle,$$

where $R(\cdot)$ is the matrix from rotation2, matrix–vector multiplication is the standard one, and $\langle\cdot,\cdot\rangle$ is the componentwise dot product on $\mathbb{R}^2$ (Mathlib's generic dotProduct: sum of the products of corresponding entries), i.e. writing $q_j=(q_{j,0},q_{j,1})$ and $k_j=(k_{j,0},k_{j,1})$,

$$\big\langle R(\theta^{(m)}_j) q_j,\ R(\theta^{(n)}_j) k_j\big\rangle = \big(\cos\theta^{(m)}_j\, q_{j,0} - \sin\theta^{(m)}_j\, q_{j,1}\big)\big(\cos\theta^{(n)}_j\, k_{j,0} - \sin\theta^{(n)}_j\, k_{j,1}\big)$$ $${}+ \big(\sin\theta^{(m)}_j\, q_{j,0} + \cos\theta^{(m)}_j\, q_{j,1}\big)\big(\sin\theta^{(n)}_j\, k_{j,0} + \cos\theta^{(n)}_j\, k_{j,1}\big).$$

When $n = 0$, Fin n is empty, so the sum defining $\hat g$ is a sum over the empty index set and hence equals $0$ identically — regardless of the values of $q$, $k$, $p_m$, $p_n$, and $\xi$ (all of which are then either the empty function $\mathrm{Fin}(0)\to\mathbb{R}$, in the case of $q,k,\xi$, or unconstrained reals, in the case of $p_m,p_n$). For $n \geq 1$, the value of $\hat g$ is exactly the finite sum above, with no further normalization (e.g. no division by $n$) and no claim of any relationship to an expectation, an inner product of the un-rotated vectors, or any other target quantity — the statement asserts only the equality of $\hat g$ with this explicit finite sum of rotated dot products.