Positive-definite kernel (Bochner-correct) and its Fourier transform

Definition

PositiveDefiniteKernel

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

fourier-analysisharmonic-analysispositive-definite-kernels

This bundle corrects and supersedes ClockRoPE.IsPosDefKernel (Definitions.Def_PosDefKernel), which turned out to be under-hypothesized: it only required the Hermitian quadratic form's real part to be nonnegative, whereas the standard definition needed for Bochner's theorem requires the whole quadratic form to be a real, nonnegative number.

A function $f : \mathbb{R} \to \mathbb{R}$ is positive definite (IsPositiveDefiniteKernel 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}$ , the quantity

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

is real (i.e. $\operatorname{Im}(S) = 0$ ) and nonnegative ( $\operatorname{Re}(S) \ge 0$ ).

IsPositiveDefiniteKernel.even: a positive-definite kernel (in this corrected sense) is automatically even: $f(-x) = f(x)$ for every $x$ . This follows from a single instance of the definition with two points $\{0, x\}$ and coefficients $\{1, i\}$ : the realness constraint forces the imaginary part of the resulting $2\times 2$ Hermitian sum, which works out to $f(-x) - f(x)$ , to vanish. Evenness is exactly what is needed for the Fourier-inversion argument used in Propositions 3.1/3.2 of the source paper: the real-valued Fourier transform fourierTransform f (defined via Re of the complex Fourier integral) can only recover $f$ through Fourier inversion when the complex Fourier transform of $f$ is already real-valued, which holds precisely when $f$ is even.

The Fourier transform fourierTransform f is unchanged from the earlier bundle: $\tau(\xi) = \operatorname{Re}\int_{\mathbb{R}} f(x)\, e^{-i2\pi\xi x}\, dx$ .

Formalization Note ClockRoPE.IsPosDefKernel and the theorems built on it (rfr_estimator_unbiased, rfr_estimator_concentration, periodic_posdef_fourier_coeffs_pmf, fourierTransform_nonneg_and_integral_eq_one) predate this fix and should be treated as superseded; corrected versions built on IsPositiveDefiniteKernel are forthcoming.

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)` is a real number and is nonnegative. Requiring the
sum to be real (not merely its real part) is the standard positive-definiteness hypothesis of
Bochner's theorem; it is what forces a positive-definite kernel to be even
(`f (-x) = f x`, see `IsPositiveDefiniteKernel.even`), which the Fourier-inversion argument for
Propositions 3.1/3.2 depends on. This supersedes `ClockRoPE.IsPosDefKernel`
(`Definitions.Def_PosDefKernel`), which only constrained the real part and is too weak to force
evenness. -/
def IsPositiveDefiniteKernel (f : ℝ → ℝ) : Prop :=
  ∀ (n : ℕ) (x : Fin n → ℝ) (c : Fin n → ℂ),
    (∑ i : Fin n, ∑ j : Fin n, starRingEnd ℂ (c i) * c j * (f (x i - x j) : ℂ)).im = 0 ∧
    0 ≤ (∑ i : Fin n, ∑ j : Fin n, starRingEnd ℂ (c i) * c j * (f (x i - x j) : ℂ)).re

/-- A positive-definite real kernel is even: `f (-x) = f x` for every `x`. -/
theorem IsPositiveDefiniteKernel.even {f : ℝ → ℝ} (hf : IsPositiveDefiniteKernel f) (x : ℝ) :
    f (-x) = f x := by
  have h := (hf 2 ![0, x] ![1, Complex.I]).1
  simp [Fin.sum_univ_two, sub_eq_add_neg] at h
  linarith [h]

/-- 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

Corrects Chen et al., ClockRoPE: Random Fourier Rotations for Temporal Routine Modeling, arXiv:2607.26369, p.3, Eq. (1) (the positive-definite kernel hypothesis); the standard definition of a positive-definite function, as required by Bochner's theorem (Bochner 1933)

View graph