Positive-definite kernel and its Fourier transform

Definition

PosDefKernel

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

fourier-analysisharmonic-analysispositive-definite-kernels

This bundle establishes two notions used throughout the mission: positive-definiteness of a real kernel, and the (real-valued) Fourier transform of such a kernel.

A function $f : \mathbb{R} \to \mathbb{R}$ is positive definite (IsPosDefKernel f) if for every $n \in \mathbb{N}$ , every finite family of points $x_1, \dots, x_n \in \mathbb{R}$ , and every family of complex coefficients $c_1, \dots, c_n \in \mathbb{C}$ ,

\mathrm{Re}\left(\sum_{i=1}^n \sum_{j=1}^n \overline{c_i}\, c_j\, f(x_i - x_j)\right) \ge 0.

This is the classical hypothesis of Bochner's theorem, which characterizes positive-definite continuous functions as Fourier transforms of finite positive measures.

The Fourier transform of $f$ (fourierTransform f) is the real-valued function

\tau(\xi) = \mathrm{Re}\int_{\mathbb{R}} f(x)\, e^{-i2\pi\xi x}\, dx.

When $f$ is continuous, Lebesgue-integrable, positive definite, and normalized ( $f(0)=1$ ), Bochner's theorem guarantees $\tau$ is nonnegative and integrates to $1$ , i.e. it is a genuine probability density on $\mathbb{R}$ — this is the density from which the mission's random rotation frequencies are sampled.

Formalization Note The real part is taken explicitly because a general integral of a complex-valued integrand is complex; for a real, even kernel the imaginary part vanishes, but that fact is not assumed here and is left for the theorems that use fourierTransform to establish.

Definition code

import Mathlib

namespace ClockRoPE

/-- A real-valued kernel `f : ℝ → ℝ` is *positive definite* if, for every finite family of
points `x : Fin n → ℝ` and complex coefficients `c : Fin n → ℂ`, the Hermitian quadratic form
`∑ i, ∑ j, conj (c i) * c j * f (x i - x j)` has nonnegative real part. This is the standard
positive-definiteness hypothesis of Bochner's theorem. -/
def IsPosDefKernel (f : ℝ → ℝ) : Prop :=
  ∀ (n : ℕ) (x : Fin n → ℝ) (c : Fin n → ℂ),
    0 ≤ (∑ i : Fin n, ∑ j : Fin n,
          starRingEnd ℂ (c i) * c j * (f (x i - x j) : ℂ)).re

/-- The Fourier transform `τ(ξ) = ∫_ℝ f(x) e^{-i2πξx} dx` of a real kernel `f`, taken as a real
number via its real part. For a continuous, Lebesgue-integrable, positive-definite kernel with
`f 0 = 1`, this coincides with the (real-valued) probability density furnished by Bochner's
theorem. -/
noncomputable def fourierTransform (f : ℝ → ℝ) (ξ : ℝ) : ℝ :=
  (∫ x : ℝ, Complex.exp (-(2 * Real.pi * Complex.I * ξ * x)) * (f x : ℂ)).re

end ClockRoPE

Source

Yiwen Chen, Joshua Ainslie, Krzysztof Choromanski, Xiang Gao, Su-Lin Wu, Yiping Yuan, Qian Sun, ClockRoPE: Random Fourier Rotations for Temporal Routine Modeling, arXiv:2607.26369, p.3, §3.2, Eq. (1) and the footnote/proof invoking Bochner's theorem before Proposition 3.1

Read-back

What the Lean code literally says, in plain math · claude-sonnet-5

Positive-definiteness of a real kernel. For a function $f : \mathbb{R} \to \mathbb{R}$ , IsPosDefKernel f asserts: for every natural number $n$ (including $n = 0$ ), every finite family of points $x_1, \dots, x_n \in \mathbb{R}$ (indexed by $\mathrm{Fin}\ n$ ), and every finite family of complex coefficients $c_1, \dots, c_n \in \mathbb{C}$ (also indexed by $\mathrm{Fin}\ n$ ), the real part of the double sum

\sum_{i=1}^{n} \sum_{j=1}^{n} \overline{c_i}\, c_j \, f(x_i - x_j)

is nonnegative, where $f(x_i-x_j)$ is treated as a complex number (its real value embedded into $\mathbb{C}$ with zero imaginary part) before being multiplied into the sum. There is no continuity, integrability, symmetry, or normalization hypothesis on $f$ anywhere in this definition — it is purely this quadratic-form condition, required to hold for all $n$ , all point-tuples, and all coefficient-tuples simultaneously. In particular the case $n = 0$ makes both sums empty, so the condition $0 \le 0$ holds trivially for every $f$ regardless of any other property of $f$ ; the substantive content resides entirely in the $n \ge 1$ cases.

Fourier transform of a real kernel. For $f : \mathbb{R} \to \mathbb{R}$ and $\xi \in \mathbb{R}$ , fourierTransform f ξ is defined as

\tau(\xi) \;=\; \operatorname{Re}\!\left(\int_{\mathbb{R}} e^{-i 2\pi \xi x}\, f(x)\, dx\right),

where the integral is taken with respect to Lebesgue measure on $\mathbb{R}$ (Mathlib's default volume measure, since no measure is specified), the integrand is the complex-valued function $x \mapsto e^{-i2\pi\xi x} \cdot f(x)$ (with $f(x)$ again coerced from $\mathbb{R}$ into $\mathbb{C}$ ), and only the real part of the resulting complex integral is retained as the output — any imaginary part the integral might have is silently discarded. Critically, this definition carries no hypothesis whatsoever that $f$ is integrable, continuous, or that the integral converges in any sense, for the given $\xi$ or for any $\xi$ . In Mathlib's convention, ∫ is a total function: whenever the integrand $x \mapsto e^{-i2\pi\xi x} f(x)$ fails to be Bochner-integrable with respect to Lebesgue measure, the integral is defined to equal $0$ by fiat (the "junk value" convention), and consequently fourierTransform f ξ evaluates to $0$ in that case — a value indistinguishable, at the level of this definition, from a genuine Fourier coefficient of $0$ . Nothing in the two declarations shown ties IsPosDefKernel to fourierTransform, nor asserts that a positive-definite $f$ has an integrable Fourier transform, nor states any version of Bochner's theorem itself (e.g., that $\tau$ is a nonnegative or probability-density function, or that $\tau(0)=1$ , or that $f(0)=1$ ); the file's docstrings describe such a connection informally, but no theorem enforcing it appears in the code given.

Human review

Endorsed by Shuze Chen · Sep 6, 2026

View graph