Corollary 3.3 (corrected): periodic case via Herglotz's theorem

Proved

ClockRoPE.periodic_posdef_fourier_coeffs_pmf_v2

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

harmonic-analysismachine-learningpositional-encodingprobability

This is Corollary 3.3 (Periodic Case via Herglotz's Theorem) of Chen et al., ClockRoPE: Random Fourier Rotations for Temporal Routine Modeling (arXiv:2607.26369), §3.3, corrected against IsPositiveDefiniteKernel (Definitions.Def_PositiveDefiniteKernel) and superseding ClockRoPE.periodic_posdef_fourier_coeffs_pmf (theorem_id a94b3c99-7dfe-4514-a452-4e32134aa731, now deprecated), which used the under-hypothesized IsPosDefKernel (see ClockRoPE.rfr_estimator_unbiased_v2 for why that predicate is insufficient).

Let $f:\mathbb R\to\mathbb R$ be a continuous, positive-definite, $T$ -periodic kernel with $f(0)=1$ ( $T>0$ ), with real Fourier coefficients $\alpha_k = \frac1T\int_0^T f(x)\cos(2\pi kx/T)\,dx$ for $k\in\mathbb Z$ (the source's Eq. (14) gives this equal to the complex-exponential form $\frac1T\int_0^T f(x)e^{-i2\pi kx/T}\,dx$ ; the real cosine form is used here so that $\alpha_k$ is manifestly real). By Herglotz's theorem,

\alpha_k \ge 0 \text{ for all } k\in\mathbb Z, \qquad \sum_{k=-\infty}^{\infty} \alpha_k = f(0) = 1,

i.e. $\{\alpha_k\}$ form a valid probability mass function over the discrete harmonics $k/T$ . This is the discrete counterpart of the goal theorem's continuous frequency density, needed to apply the RFR construction to periodic attention-modulation profiles such as the cosine and periodic-Gaussian priors ClockRoPE deploys in practice.

Formalization Note The sum $\sum_k \alpha_k$ is formalized as a tsum over $\mathbb Z$ (\sum' k : \mathbb Z, \alpha k), asserting the series converges unconditionally to $1$ .

Preamble

import Mathlib
import Definitions.Def_PositiveDefiniteKernel

Formal statement

namespace ClockRoPE

/-- **Corollary 3.3 (Periodic Case via Herglotz's Theorem)** — corrected against
`IsPositiveDefiniteKernel`, superseding `ClockRoPE.periodic_posdef_fourier_coeffs_pmf`, which
used the under-hypothesized `IsPosDefKernel`.
Let `f : ℝ → ℝ` be a continuous, positive-definite, `T`-periodic kernel with `f 0 = 1`
(`T > 0`), with (real) Fourier coefficients `α_k = (1/T) ∫_0^T f(x) cos(2πkx/T) dx` for
`k ∈ ℤ` (the source's Eq. (14) gives this as equal to the complex-exponential form
`(1/T) ∫_0^T f(x) e^{-i2πkx/T} dx`; the real cosine form is used here so that `α k` is
manifestly a real number). By Herglotz's theorem, `{α_k}` are all nonnegative and sum to
`f 0 = 1`, i.e. they form a valid probability mass function over the discrete harmonics
`{k / T}`. -/
theorem periodic_posdef_fourier_coeffs_pmf_v2
    (f : ℝ → ℝ) (T : ℝ) (hT : 0 < T)
    (hf_cont : Continuous f) (hf_pd : IsPositiveDefiniteKernel f) (hf0 : f 0 = 1)
    (hf_periodic : ∀ x : ℝ, f (x + T) = f x)
    (α : ℤ → ℝ)
    (hα : ∀ k : ℤ, α k =
      (1 / T) * ∫ x in (0 : ℝ)..T, f x * Real.cos (2 * Real.pi * (k : ℝ) * x / T)) :
    (∀ k : ℤ, 0 ≤ α k) ∧ ∑' k : ℤ, α k = 1 := by
  sorry

end ClockRoPE

Source

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

View graph