Proposition 3.2 (corrected): convergence of the Random Fourier Rotation estimator

Proved

ClockRoPE.rfr_estimator_concentration_v2

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

harmonic-analysismachine-learningpositional-encodingprobability

This is Proposition 3.2 (Convergence of the Random Fourier Rotation Estimator) of Chen et al., ClockRoPE: Random Fourier Rotations for Temporal Routine Modeling (arXiv:2607.26369), §3.2, corrected against IsPositiveDefiniteKernel (Definitions.Def_PositiveDefiniteKernel) and superseding ClockRoPE.rfr_estimator_concentration (theorem_id 64647d10-141e-40a5-a8c5-b9acdc7ad56c, now deprecated), which used the under-hypothesized IsPosDefKernel (see ClockRoPE.rfr_estimator_unbiased_v2 for why that predicate is insufficient).

Under the same setting as Proposition 3.1 (ClockRoPE.rfr_estimator_unbiased_v2) — a continuous, Lebesgue-integrable, positive-definite kernel $f$ with $f(0)=1$ , its Fourier transform $\tau$ , $n$ i.i.d. frequencies $\xi_0,\dots,\xi_{n-1}\sim\tau$ , and a query $q_m\in\mathbb R^{2n}$ , key $k_n\in\mathbb R^{2n}$ at positions $p_m,p_n\in\mathbb R$ — the theorem gives a quantitative concentration bound for the averaged estimator around its mean. For every $\epsilon>0$ :

P\!\left(\left|\frac1n\hat g(q_m,k_n,p_m,p_n) - \frac1n\,q_m^\top k_n\,f(p_m-p_n)\right| \ge \epsilon\right) \le 2\exp\!\left(-\frac{\epsilon^2(2n)^2}{8\sum_{j=0}^{n-1}\big(\lVert q_m^{(j)}\rVert\,\lVert k_n^{(j)}\rVert\big)^2}\right),

where $q_m^{(j)},k_n^{(j)}\in\mathbb R^2$ are the $j$ -th feature pairs of $q_m,k_n$ and $\lVert\cdot\rVert$ is the Euclidean norm on $\mathbb R^2$ . The probability is taken over the same product measure as in Proposition 3.1.

This is the quantitative counterpart to the unbiasedness of Proposition 3.1: it shows the deviation of the sampled estimator from its target value decays exponentially as the embedding dimension $d=2n$ grows, at a rate controlled by the magnitudes of the feature pairs.

Formalization Note The probability is represented as the measure, under the $n$ -fold product measure of MeasureTheory.Measure.withDensity copies of $\tau$ , of the set of frequency vectors $\xi$ for which the deviation exceeds $\epsilon$ ; the right-hand side is compared as an extended nonnegative real via ENNReal.ofReal.

Preamble

import Mathlib
import Definitions.Def_PositiveDefiniteKernel
import Definitions.Def_RandomFourierRotation

Formal statement

namespace ClockRoPE

open MeasureTheory

/-- **Proposition 3.2 (Convergence of Random Fourier Rotation Estimator)** — corrected against
`IsPositiveDefiniteKernel`, superseding `ClockRoPE.rfr_estimator_concentration`, which used the
under-hypothesized `IsPosDefKernel`.
Under the same setting as `rfr_estimator_unbiased_v2` (a continuous, integrable, positive-definite
kernel `f` with `f 0 = 1`, its Fourier transform `τ`, `n` i.i.d. frequencies `ξ_0, …, ξ_{n-1} ∼
τ`, and query/key vectors `q_m, k_n ∈ ℝ^{2n}` at positions `p_m, p_n`), the averaged estimator
`(1/n) · ĝ(q_m, k_n, p_m, p_n)` concentrates around `(1/n) · q_m^⊤ k_n · f(p_m - p_n)` at a rate
governed by a McDiarmid-type exponential tail bound. -/
theorem rfr_estimator_concentration_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 : ℝ) (ε : ℝ) (hε : 0 < ε) :
    (Measure.pi fun _ : Fin n =>
        (volume : Measure ℝ).withDensity fun x => ENNReal.ofReal (fourierTransform f x))
        {ξ : Fin n → ℝ |
          ε ≤ |(1 / (n : ℝ)) * rfrEstimator n q k pm pn ξ
                - (1 / (n : ℝ)) * (dotProduct q k * f (pm - pn))|}
      ≤ ENNReal.ofReal
          (2 * Real.exp (-(ε ^ 2 * (2 * (n : ℝ)) ^ 2 /
            (8 * ∑ j : Fin n,
              (pairNorm (featurePair n q j) * pairNorm (featurePair n k j)) ^ 2)))) := by
  sorry

end ClockRoPE

Source

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

View graph