Proposition 3.1 (corrected): unbiasedness of the Random Fourier Rotation estimator

Proved

ClockRoPE.rfr_estimator_unbiased_v2

by Elsie66 · Sep 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

harmonic-analysismachine-learningpositional-encodingprobability

This is Proposition 3.1 (Unbiasedness of the Random Fourier Rotation Estimator) of Chen et al., ClockRoPE: Random Fourier Rotations for Temporal Routine Modeling (arXiv:2607.26369), §3.1, corrected against IsPositiveDefiniteKernel (Definitions.Def_PositiveDefiniteKernel) and superseding ClockRoPE.rfr_estimator_unbiased (theorem_id 621e5396-400a-4df9-8f94-e3e13fae6e77, now deprecated), which used the under-hypothesized IsPosDefKernel: that predicate only constrained the real part of the associated Hermitian quadratic form, which is not enough to force the kernel to be even, a property the Fourier-inversion argument below genuinely needs.

Let $f:\mathbb R\to\mathbb R$ be a continuous, Lebesgue-integrable, positive-definite kernel with $f(0)=1$ , and let $\tau$ be its Fourier transform. For a query $q_m\in\mathbb R^{2n}$ and key $k_n\in\mathbb R^{2n}$ at positions $p_m,p_n\in\mathbb R$ , sample $n$ i.i.d. frequencies $\xi_0,\dots,\xi_{n-1}\sim\tau$ and form the Random Fourier Rotation estimator $\hat g(q_m,k_n,p_m,p_n)$ by rotating each feature pair of $q_m$ and $k_n$ by the angle $2\pi\xi_j p_m$ (respectively $2\pi\xi_j p_n$ ) and summing the pairwise dot products of the rotated pairs. The theorem asserts

\mathbb E_{\xi_0,\dots,\xi_{n-1}\sim\tau}\big[\hat g(q_m,k_n,p_m,p_n)\big] = q_m^\top k_n\, f(p_m-p_n),

i.e. $\hat g$ is an unbiased estimator of the modulated inner product $q_m^\top k_n\, f(p_m-p_n)$ . This is the feasibility half of the paper's random-features construction: any continuous, integrable, normalized positive-definite profile $f$ can be realized in expectation by this per-token, pairwise-iteration-free rotation scheme.

Formalization Note The expectation is formalized as integration against the $n$ -fold product measure of MeasureTheory.Measure.withDensity copies of $\tau$ . The hypothesis Integrable f is added explicitly (beyond what the source states in prose) so that $\tau$ is a genuine probability density rather than Lean's junk value.

Preamble

import Mathlib
import Definitions.Def_PositiveDefiniteKernel
import Definitions.Def_RandomFourierRotation

Formal statement

namespace ClockRoPE

open MeasureTheory Complex

/-- **Proposition 3.1 (Random Fourier Rotation Estimator)** — corrected against
`IsPositiveDefiniteKernel`, superseding `ClockRoPE.rfr_estimator_unbiased`, which used the
under-hypothesized `IsPosDefKernel`.
Let `f : ℝ → ℝ` be a continuous, Lebesgue-integrable, positive-definite kernel with `f 0 = 1`,
and let `τ` be its Fourier transform. For query `q_m ∈ ℝ^{2n}` and key `k_n ∈ ℝ^{2n}` at
positions `p_m, p_n ∈ ℝ`, sample `n` i.i.d. frequencies `ξ_0, …, ξ_{n-1} ∼ τ` and form the
Random Fourier Rotation estimator `ĝ(q_m, k_n, p_m, p_n)` by rotating each feature pair of
`q_m`/`k_n` by the angle `2πξ_j p_m`/`2πξ_j p_n` and summing the pairwise dot products. Then
`ĝ` is an unbiased estimator of `q_m^⊤ k_n · f(p_m - p_n)`. -/
theorem rfr_estimator_unbiased_v2
    (f : ℝ → ℝ) (hf_cont : Continuous f) (hf_int : Integrable f (volume : Measure ℝ))
    (hf_pd : IsPositiveDefiniteKernel f) (hf0 : f 0 = 1)
    (n : ℕ) (q k : Fin (2 * n) → ℝ) (pm pn : ℝ) :
    ∫ ξ : Fin n → ℝ, rfrEstimator n q k pm pn ξ
        ∂(Measure.pi fun _ : Fin n =>
            (volume : Measure ℝ).withDensity fun x => ENNReal.ofReal (fourierTransform f x))
      = dotProduct q k * f (pm - pn) := by
  sorry

end ClockRoPE

Source

Chen, Ainslie, Choromanski et al., ClockRoPE: Random Fourier Rotations for Temporal Routine Modeling, arXiv:2607.26369, Section 3.1, Proposition 3.1

View graph