## Motivation
Transformer sequence models modulate attention scores by a function of the relative
position between a query and a key: the attention logit between token $m$ and token
$n$ is scaled by a fixed profile $f(p_m - p_n)$. Realizing this modulation the naive
way means evaluating $f$ once per pair $(m,n)$ and materializing an $L\times L$
adjustment over the whole sequence — quadratic in the sequence length $L$. Rotary
Position Embedding (RoPE) [Su et al. 2021](https://arxiv.org/abs/2104.09864) avoids
this entirely: it rotates the query at position $p_m$ and the key at position $p_n$
*independently*, each by an angle depending only on its own position, so that the
pairwise quantity $f(p_m-p_n)$ falls out of the dot product of the two separately
rotated vectors — $f$ is never evaluated pairwise, and no $L\times L$ matrix is ever
built. This is what lets RoPE stay a linear, per-token preprocessing step compatible
with efficient (sub-quadratic) attention implementations, rather than an $O(L^2)$
modulation. The catch is that RoPE's specific log-linear frequency schedule bakes in
one particular profile: a monotone, decaying $f$. That schedule is a poor fit
whenever the correlation structure of the data is not monotonically decaying with
distance — the leading example being **periodicity**: in sequential recommendation,
interactions separated by exactly one day or one week are more correlated than
interactions separated by, say, half a day, and a decaying profile cannot express
that "attention comes back" at the period.
Chen, Ainslie, Choromanski et al., *ClockRoPE: Random Fourier Rotations for Temporal
Routine Modeling* ([arXiv:2607.26369](https://arxiv.org/abs/2607.26369)), ask a more
general question first: which attention-modulation profiles $f$ can be realized *at
all* by this same per-token, pairwise-iteration-free rotation trick — rotate each
token once, on its own, and let the pairwise profile emerge from the dot product —
and by what rotation-frequency schedule? Their answer is a random-features
construction — sample the rotation frequencies from the kernel's own Fourier
transform, rather than fixing them log-linearly — that realizes *any* continuous,
normalized, positive-definite profile in expectation, with a quantified concentration
rate, all while keeping the exact same per-token rotate-then-dot-product computation
RoPE already uses. ClockRoPE is the periodic instance of this general theory, later
deployed in a production-scale generative-retrieval system.
## Setting
Fix an embedding dimension $d = 2n$ and group a vector $v \in \mathbb{R}^d$ into $n$
consecutive **feature pairs** $v^{(j)} = (v_{2j}, v_{2j+1}) \in \mathbb{R}^2$ for
$j = 0, \dots, n-1$. For an angle $\theta$, let
$$
R(\theta) = \begin{pmatrix} \cos\theta & -\sin\theta \\ \sin\theta & \cos\theta \end{pmatrix}
$$
be the $2\times 2$ (Givens) rotation matrix. A real kernel $f : \mathbb{R} \to
\mathbb{R}$ is **positive definite** if for every finite family of points
$x_1,\dots,x_N \in \mathbb{R}$ and complex coefficients $c_1,\dots,c_N$,
$\sum_{i,j} \overline{c_i} c_j f(x_i - x_j)$ has nonnegative real part; it is
**normalized** if $f(0) = 1$. When $f$ is also continuous and Lebesgue-integrable,
its Fourier transform
$$
\tau(\xi) = \int_{\mathbb{R}} f(x) e^{-i2\pi\xi x}\,dx
$$
is (by Bochner's theorem) a genuine probability density on $\mathbb{R}$: this is the
distribution the mission's rotation frequencies are sampled from.
Given a query $q_m \in \mathbb{R}^{2n}$ at position $p_m$, a key $k_n \in
\mathbb{R}^{2n}$ at position $p_n$, and $n$ i.i.d. frequencies $\xi_0, \dots,
\xi_{n-1} \sim \tau$, the **Random Fourier Rotation (RFR) estimator** is
$$
\hat g(q_m, k_n, p_m, p_n) = \sum_{j=0}^{n-1} \big(R(2\pi\xi_j p_m)\, q_m^{(j)}\big)^\top \big(R(2\pi\xi_j p_n)\, k_n^{(j)}\big).
$$
$\hat g$ is exactly the modulated attention logit computed by rotating query/key
feature pairs with per-pair, sampled RoPE frequencies — the same operation standard
RoPE performs, but with $\xi_j$ drawn from $\tau$ instead of fixed by a log-linear
schedule.
## Formalization targets
### Goal — convergence of the RFR estimator (Proposition 3.2)
$$
P\!\left(\left|\tfrac1n \hat g(q_m,k_n,p_m,p_n) - \tfrac1n\, 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)
$$
for every $\epsilon > 0$. This is the mission's central target: it upgrades the mean
identity below into a quantitative, non-asymptotic guarantee that the sampled
estimator is close to the target profile with high probability, at a rate that is
exponential in the embedding dimension $d = 2n$.
### Milestone — unbiasedness of the RFR estimator (Proposition 3.1)
$$
\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).
$$
The expectation identity that the concentration bound above sharpens; it is the
feasibility half of the claim ("this construction is correct on average") that the
convergence half needs as its starting point.
### Milestone — periodic case via Herglotz's theorem (Corollary 3.3)
For a continuous, positive-definite, $T$-periodic $f$ with $f(0)=1$ and Fourier
coefficients $\alpha_k = \frac1T \int_0^T f(x) e^{-i2\pi kx/T}\,dx$,
$$
\alpha_k \ge 0 \text{ for all } k \in \mathbb{Z}, \qquad \sum_{k=-\infty}^{\infty} \alpha_k = f(0) = 1.
$$
The periodic specialization needed to apply the goal and first milestone with a
*discrete* frequency distribution over harmonics $k/T$ — the regime ClockRoPE
actually deploys, since daily/weekly routines are periodic rather than merely
decaying.
## Significance
The result gives a general recipe — sample, don't hand-design — for turning *any*
admissible attention-modulation profile into a RoPE-compatible rotation schedule,
with a concentration guarantee that says how many feature pairs are needed before the
sampled schedule reliably approximates the target profile. Crucially, the recipe
changes only *which frequencies* the per-token rotation uses — it never touches the
computational shape of RoPE itself: each query and key is still rotated once,
independently, by an angle depending only on its own position, and the target
pairwise profile $f(p_m-p_n)$ is still recovered purely from the dot product of the
two rotated vectors. So realizing an arbitrary positive-definite $f$ this way costs
exactly what realizing RoPE's own log-linear profile costs — linear in the sequence
length, with no pairwise evaluation of $f$ and no $L\times L$ matrix ever
materialized — rather than the quadratic cost a direct, per-pair implementation of
an arbitrary modulation function would require. This subsumes standard RoPE's
log-linear schedule as one instance and explains, via the periodic corollary, why a
schedule built from the kernel's own spectrum (rather than an arbitrary log-linear
one) is the right way to encode periodicity: nothing about the construction, or its
efficiency, is specific to decay. The paper reports this translated into measured
gains in a production-scale generative-retrieval system, which is unusual weight of
practical evidence behind a Bochner/Herglotz-style spectral argument.
At the time of writing, none of these three results have a machine-checked proof;
this mission asks for the first formalization of all three, together with the shared
scaffolding (feature-pair extraction, the rotation estimator, and the notion of a
positive-definite kernel) they are stated over.
## Difficulty
The natural first attempt at the concentration bound is a direct union bound or a
naive variance argument, but the estimator $\hat g$ is a sum of $n$ terms that are
each *bounded* (each rotated pair lies on a fixed-radius circle) rather than governed
by a variance bound that shrinks with $n$ under a fixed frequency; the source proof
instead applies McDiarmid's bounded-differences inequality, treating each sampled
frequency $\xi_j$ as one coordinate of the input and bounding the one-coordinate
change in $\hat g$ by $2\lVert q_m^{(j)}\rVert\lVert k_n^{(j)}\rVert$ via the
maximal distance between two points on the unit circle — not by directly bounding a
variance term. Establishing Proposition 3.1 itself already requires care: it
requires justifying that $\tau$, defined purely as an integral transform of $f$, is
in fact a legitimate probability density (Bochner's theorem), and then a real/complex
bookkeeping argument identifying the real inner product of rotated pairs with the
real part of a product of complex exponentials.
## Formalization scope
The mission works over the reals and represents feature pairs as functions
`Fin (2 * n) → ℝ` sliced into `Fin n`-indexed pairs, matching the "$n$ feature pairs,
dimension $d = 2n$" convention used throughout; $2\times2$ rotations are ordinary
`Matrix (Fin 2) (Fin 2) ℝ` values built with `Matrix.mulVec`/`Matrix.dotProduct`, and
expectation over i.i.d. $\tau$-distributed frequencies is formalized as integration
against the product measure `MeasureTheory.Measure.pi` of `n` independent copies of
the measure with density $\tau$ (`MeasureTheory.Measure.withDensity`) — this is
mathematically equivalent to, and more directly usable in Lean than, introducing an
abstract probability space with named i.i.d. random variables.
Since a general continuous positive-definite kernel need not have an
*integrable* Fourier transform (the periodic case in Corollary 3.3 is exactly the
counterexample: its "Fourier transform" is a discrete measure, not a density) — the
goal and first milestone add `Integrable f` as an explicit hypothesis beyond what the
paper states in prose, so that $\tau$ is genuinely a density rather than a junk value.
This is not a strengthening of the target profiles the paper cares about in practice
(Gaussian, Laplace, and the cosine/Gaussian priors used by ClockRoPE itself are all
integrable) and mirrors the paper's own split between the density case (Propositions
3.1–3.2) and the discrete, purely-periodic case (Corollary 3.3). A formalization that
dropped this hypothesis and instead let the Fourier integral silently evaluate to
Lean's junk value (`0` for non-integrable integrands) would make the goal statement
possible to "prove" vacuously and must be avoided.
Definitions needed: a positive-definite-kernel predicate, the real-valued Fourier
transform of a kernel, feature-pair extraction, the $2\times2$ rotation matrix, and
the RFR estimator itself — all reusable by any future mission formalizing RoPE-family
positional encodings (e.g. STRING, nD-RoPE) or other random-Fourier-feature results.
McDiarmid's inequality, if not already in Mathlib in the needed form, is itself a
independently reusable contribution.
## Selected references
- Yiwen Chen, Joshua Ainslie, Krzysztof Choromanski, Xiang Gao, Su-Lin Wu, Yiping Yuan, Qian Sun, *ClockRoPE: Random Fourier Rotations for Temporal Routine Modeling*, 2026. [arXiv:2607.26369](https://arxiv.org/abs/2607.26369)
- Jianlin Su, Yu Lu, Shengfeng Pan, Ahmed Murtadha, Bo Wen, Yunfeng Liu, *RoFormer: Enhanced Transformer with Rotary Position Embedding*, arXiv, 2021. [arXiv:2104.09864](https://arxiv.org/abs/2104.09864)
- Ali Rahimi, Benjamin Recht, *Random Features for Large-Scale Kernel Machines*, NeurIPS, 2007.
- Salomon Bochner, *Monotone Funktionen, Stieltjessche Integrale und harmonische Analyse*, Springer, 1933.
- Gustav Herglotz, *Über Potenzreihen mit positivem, reellem Teil im Einheitskreis*, Berichte über die Verhandlungen der Königlich Sächsischen Gesellschaft der Wissenschaften zu Leipzig, 1911.
5 thms1 active userReviewed
🏆Completed
Captain: lisamegawatts
Finite Reflection Positivity Methods I: Split Weights and Infrared ModesTextbook
### Motivation
Reflection positivity and infrared bounds form a standard finite-volume route
from the geometry of a lattice reflection to quantitative control of long
wavelength fluctuations. In the classical argument, reflection positivity
supplies a Cauchy--Schwarz inequality for reflected observables, while Fourier
diagonalization of the lattice Laplacian identifies the free covariance used
in the infrared comparison. These ingredients underlie rigorous results on
continuous-symmetry lattice systems in Fröhlich, Simon, and Spencer's
development of infrared bounds and spontaneous symmetry breaking
([1976](https://doi.org/10.1007/bf01608557)), and the general theory of
reflection positivity developed by Fröhlich, Israel, Lieb, and Simon
([1978](https://doi.org/10.1007/bf01940327)). Related technology appears in
Fröhlich and Spencer's treatment of the two-dimensional Abelian spin systems
and Coulomb gas ([1981](https://doi.org/10.1007/bf01208273)).
The analytic and model-specific theorems are substantial, but their finite
algebraic interface is sharply separable. This mission isolates that interface
so later clock, XY, and Gaussian-domination developments can share one checked
notion of reflection, one spectral covariance convention, and one treatment of
the constant mode.
### Setting
Let $X$ be a finite set of configurations on one side of a reflection plane.
A full split configuration is a pair $(x,y)\in X\times X$, and reflection
exchanges its two entries. A plus-half observable is a function $F:X\to
\mathbb R$ lifted to $X\times X$ through the first coordinate. Its reflected
copy therefore depends on the second coordinate.
A split weight is specified by a finite feature index $A$, real coefficients
$c_a$, and features $\phi_a:X\to\mathbb R$:
$$
W(x,y)=\sum_{a\in A}c_a\phi_a(x)\phi_a(y).
$$
For a finite family of plus-half observables $F_i$, the reflected kernel is
$$
K_{ij}=\sum_{(x,y)\in X\times X}
W(x,y)F_i(x)F_j(y).
$$
A real matrix is positive semidefinite here when it is symmetric and its
quadratic form is nonnegative on every real coordinate vector.
The spectral side uses a finite mode set $I$ with a distinguished zero mode
$0$. An infrared spectrum consists of a function $\lambda:I\to\mathbb R$
that is nonnegative and vanishes exactly at $0$. For $\beta>0$, the free
mode covariance is diagonal, equals zero at the constant mode, and has entry
$$
G_{kk}=\frac{1}{\beta\lambda_k}
$$
away from zero. Covariance domination is tested only on source vectors whose
zero-mode coordinate vanishes. The concrete spectral fixture is the
$4\times4$ periodic square lattice, with tensor-product discrete Fourier modes
and the nearest-neighbor graph Laplacian.
### Formalization targets
#### Finite reflection positivity
The first target identifies the split reflection pairing with the explicit
double sum over the two halves. Under $c_a\ge0$, the resulting reflected
kernel must be positive semidefinite:
$$
\sum_{i,j}u_iK_{ij}u_j\ge0.
$$
Every such kernel must satisfy the two-observable chessboard inequality
$$
K_{ij}^{2}\le K_{ii}K_{jj}.
$$
#### Typed finite spectrum
For every Torus-4 frequency $k$ and site $x$, the registered Fourier mode
$\psi_k$ must satisfy the pointwise eigenvalue equation
$$
(\Delta_{\mathrm{T4}}\psi_k)(x)=\lambda_k\psi_k(x).
$$
The eigenvalues must be nonnegative and vanish exactly at the constant mode,
and these laws must be packaged as the same spectrum type consumed by the
infrared definitions.
#### Zero-mode-restricted infrared bound
The diagonal free covariance must be positive semidefinite for $\beta>0$.
If an interacting covariance $C$ is quadratically dominated by $G$ on sources
with $u_0=0$, then every nonzero Fourier mode must satisfy
$$
C_{kk}\le\frac{1}{\beta\lambda_k}\qquad(k\ne0).
$$
Two finite counterfixtures are part of the target. They assert that an
arbitrary full-vertex reflected two-point matrix need not be positive
semidefinite, and that domination restricted away from the zero mode need not
extend to full-matrix domination.
### Significance
The resulting interface prevents three substitutions that otherwise look
notational but change the theorem. Reflection positivity is tested on
observables supported on one half rather than on an arbitrary matrix indexed
by all vertices. The infrared comparison excludes the constant mode rather
than forcing a fluctuating zero mode below a covariance with zero diagonal.
The graph-Laplacian eigenvalue is connected to the Fourier mode by an explicit
pointwise theorem rather than by assigning a function the name
`laplacianEigenvalue`.
Several ingredients already have machine-checked Lean proofs in the
LeanProofs repository: the finite matrix Cauchy--Schwarz theorem, the Torus-4
DFT diagonalization and zero-mode theorem, and the diagonal free-covariance
calculation. This mission reorganizes those results around a corrected
consumer boundary and adds the split-half and off-zero adapters. It does not
present the finite statements as new mathematics.
### Difficulty
The main difficulty is maintaining the correct domain at each interface. A
reflection of lattice sites does not by itself imply positive semidefiniteness
of a correlation matrix indexed by every site; the tested observables and
their support are part of the assertion. Likewise, a free covariance whose
constant-mode entry is defined to be zero cannot dominate an arbitrary
covariance on all source vectors. Finally, a Fourier multiplier used for a
pseudospectral derivative is not automatically the eigenvalue of the
nearest-neighbor graph Laplacian. The formal statements must keep these three
objects distinct.
### Formalization scope
All configuration, feature, observable, and mode types are finite. Kernels,
weights, coefficients, source vectors, and quadratic forms are real. Complex
numbers occur only in the explicit discrete Fourier modes. Reflected pairings
are unnormalized finite sums; no partition function or probability measure is
introduced. The inverse temperature satisfies $\beta>0$. The distinguished
zero mode is part of the spectrum interface, and infrared domination is
restricted to source vectors that vanish at that coordinate.
The mission does not assert reflection positivity of a clock or XY Gibbs
measure, nonnegative Fourier coefficients of a physical cross-bond weight,
Gaussian domination, a thermodynamic limit, a Kosterlitz--Thouless transition,
or a universal jump. It also does not identify the Torus-4 graph spectrum with
the Grid3 pseudospectral multiplier from the Fourier--Hodge packet. Those are
separate future missions requiring additional model and analytic input.
The reusable outputs are the split-weight RP interface, the finite
positive-semidefinite kernel API, the typed spectrum object, and the
zero-mode-restricted domination predicate. Contributions should preserve the
explicit half support and zero-mode restrictions; a proof obtained by adding
the desired conclusion as a hypothesis is outside scope.
### Selected references
- J. Fröhlich, B. Simon, and T. Spencer, *Infrared bounds, phase transitions
and continuous symmetry breaking*, Communications in Mathematical Physics
50 (1976), 79--95. https://doi.org/10.1007/bf01608557
- J. Fröhlich, R. Israel, E. H. Lieb, and B. Simon, *Phase transitions and
reflection positivity. I. General theory and long range lattice models*,
Communications in Mathematical Physics 62 (1978), 1--34.
https://doi.org/10.1007/bf01940327
- J. Fröhlich and T. Spencer, *The Kosterlitz--Thouless transition in
two-dimensional Abelian spin systems and the Coulomb gas*, Communications in
Mathematical Physics 81 (1981), 527--602.
https://doi.org/10.1007/bf01208273
- LeanProofs, `ReflectionPositivityInfraredBound.lean`, exact repository
snapshot `dbf503b2909cc17787d40a21eb75a0c9354cc6ef`.
https://github.com/MonumentalSystems/LeanProofs/blob/dbf503b2909cc17787d40a21eb75a0c9354cc6ef/LeanProofs/StatMech/ReflectionPositivityInfraredBound.lean
11 thms1 active userReviewed
🏆Completed
Captain: Elsie66
Fejér's TheoremTextbook
## Motivation
The Fourier series of a periodic function decomposes it into sinusoidal components, but the partial sums of that series need not converge to the function even when the function is continuous: du Bois-Reymond exhibited in 1873 a continuous $2\pi$-periodic function whose Fourier partial sums diverge at a point. Fejér's 1904 theorem repairs this failure by replacing the partial sums with their Cesàro (arithmetic) averages: for *every* continuous periodic function, these averages converge to the function, uniformly, with no smoothness hypothesis beyond continuity. This was the first universally valid summation method for Fourier series, and its underlying technique — averaging against a kernel whose mass concentrates at the origin — became the template for what is now called a good kernel or approximate identity, the basic device used throughout harmonic analysis (heat-kernel smoothing, Poisson summation, Fourier-inversion arguments) [Stein & Shakarchi, 2003].
**Timeline.**
- 1873 — du Bois-Reymond constructs a continuous $2\pi$-periodic function whose Fourier series diverges at a point, showing continuity alone cannot guarantee convergence of the partial sums themselves.
- 1904 — Fejér proves that the Cesàro means of the Fourier series of any continuous periodic function converge to it uniformly (Fejér, 1904).
- The good-kernel method Fejér introduced was later systematized as the general framework for approximate identities in harmonic analysis (Stein & Shakarchi, 2003, Ch. 2, §5).
## Setting
Let $f : \mathbb{R} \to \mathbb{C}$ be continuous and $2\pi$-periodic, i.e. $f(x + 2\pi) = f(x)$ for every $x \in \mathbb{R}$. Its $n$-th **Fourier coefficient**, for $n \in \mathbb{Z}$, is
$$\hat f(n) = \frac{1}{2\pi}\int_{-\pi}^{\pi} f(\theta)\, e^{-in\theta}\, d\theta.$$
Its $N$-th **partial sum** is $S_N(f)(\theta) = \sum_{n=-N}^{N} \hat f(n)\, e^{in\theta}$, and its $N$-th **Cesàro (Fejér) mean** is the arithmetic average of the first $N+1$ partial sums,
$$\sigma_N(f)(\theta) = \frac{1}{N+1}\sum_{k=0}^{N} S_k(f)(\theta).$$
## Formalization targets
### Fejér's theorem
$$\sigma_N(f) \longrightarrow f \quad \text{uniformly on } \mathbb{R} \text{ as } N \to \infty.$$
This is the full 1904 statement: no restriction to pointwise convergence, and no extra regularity assumed on $f$ beyond continuity.
## Significance
**The result itself.** Fejér's theorem gives the first universally valid summation method for the Fourier series of a continuous function, closing the gap left open by pointwise convergence tests that need extra regularity. It also yields, essentially for free, a proof of the Weierstrass approximation theorem on the circle — the trigonometric polynomials $\sigma_N(f)$ are dense in the continuous $2\pi$-periodic functions under the uniform norm — and it is the historical prototype of the good-kernel/approximate-identity method underlying Poisson summation, heat-kernel smoothing, and $L^1$ Fourier-inversion arguments.
**Formalizing it.** Mathlib currently has no infrastructure for this at all. `Mathlib.Analysis.Fourier.AddCircle` defines Fourier coefficients on the circle and proves $L^2$ convergence (Parseval's identity, via the orthonormal Fourier basis), but it has no notion of a partial sum, no Dirichlet or Fejér kernel, and no pointwise or uniform convergence result for Fourier series of any kind. This mission builds that classical convergence theory — the Fejér kernel, its closed form and positivity, the good-kernel estimates, and the uniform convergence theorem itself — from first principles.
## Difficulty
The obvious first attempt is to bound $|\sigma_N(f)(\theta) - f(\theta)|$ termwise from the individual Fourier coefficients. This fails outright: a continuous function's Fourier coefficients need not be absolutely summable, which is exactly the mechanism behind du Bois-Reymond's divergence example. The real difficulty is representing $\sigma_N(f)$ as a convolution,
$$\sigma_N(f)(\theta) = \frac{1}{2\pi}\int_{-\pi}^{\pi} f(\theta - \varphi)\, F_N(\varphi)\, d\varphi,$$
against the Fejér kernel $F_N$, and then proving $F_N$ is a *good kernel*: nonnegative, integrating to $1$ over one period, and — the genuinely quantitative step — with its mass outside any fixed neighborhood of $0$ vanishing as $N \to \infty$. That last estimate needs the closed form
$$F_N(\theta) = \frac{1}{N+1}\left(\frac{\sin((N+1)\theta/2)}{\sin(\theta/2)}\right)^2,$$
which carries a removable singularity at $\theta = 0$ that must be handled carefully, together with a genuine decay estimate — via a lower bound on $|\sin(\theta/2)|$ — valid uniformly outside any fixed $\delta$-neighborhood of the origin.
## Formalization scope
$f$ is complex-valued, and only continuity together with exact $2\pi$-periodicity is assumed — no differentiability, no bounded variation, no realness. Uniform convergence is stated with Mathlib's `TendstoUniformly`. The period is fixed at $2\pi$, matching the classical circle-group convention, rather than a general $T > 0$; the $T$-periodic statement is a routine rescaling of this one and is not separately targeted here. One route to a trivializing formalization is worth ruling out explicitly: assuming any extra regularity on $f$ (differentiability, bounded variation, Lipschitz continuity) would let the uniform-convergence conclusion follow from the much easier Dirichlet-kernel estimates, and would no longer be Fejér's theorem — the entire content of the result is that continuity alone suffices.
The needed infrastructure is the four definitions above (Fourier coefficient, partial sum, Cesàro mean, Fejér kernel) and the milestone lemmas below, culminating in the goal. The Fejér kernel's closed form, positivity, and good-kernel estimates are reusable well beyond this mission: directly for a Lean proof of the Weierstrass approximation theorem on the circle, and for any future development that needs an explicit approximate identity on the circle group. Contributions are welcome at every milestone; the concentration estimate is the analytic heart of the mission and a natural place to start.
## Selected references
- L. Fejér, "Untersuchungen über Fouriersche Reihen," *Mathematische Annalen* 58 (1904), 51–69.
- E. M. Stein and R. Shakarchi, *Fourier Analysis: An Introduction*, Princeton Lectures in Analysis I, Princeton University Press, 2003, Chapter 2, §5 ("Good Kernels") and Theorem 5.2.
- Wikipedia, "Fejér's theorem." https://en.wikipedia.org/wiki/Fej%C3%A9r%27s_theorem
## Motivation
Positive-definite functions sit at a crossroads of harmonic analysis, probability, and machine learning. A function $f:\mathbb R\to\mathbb C$ is *positive-definite* if, for every finite family of points $x_1,\dots,x_n$ and complex coefficients $c_1,\dots,c_n$, the Hermitian quadratic form $\sum_{i,j}\overline{c_i}c_j f(x_i-x_j)$ is real and nonnegative. This single algebraic condition is exactly what makes $f$ realizable as: the covariance kernel of a stationary stochastic process; the characteristic function of a random variable (up to normalization); a valid Mercer/RBF kernel in machine learning; or a valid random-features/spectral density in random-feature kernel approximation methods.
Bochner's theorem (1932) is the structural reason all of these examples work: it says positive-definiteness is not merely a *necessary* condition for such a representation, but *exactly characterizes* it. A continuous, normalized ($f(0)=1$) function is positive-definite if and only if it is the Fourier–Stieltjes transform of some probability measure $\nu$ on $\mathbb R$ — i.e. $f$ is the characteristic function of a random variable. This mission asks for a machine-checked proof of that theorem, together with its most useful corollary: the case where $f$ is additionally Lebesgue-integrable, so that $\nu$ has an explicit continuous density given directly by the ordinary Fourier transform of $f$.
## Setting
Fix `IsPositiveDefinite f` as above, for $f:\mathbb R\to\mathbb C$ (not restricted to real-valued kernels — the standard, fully general statement). A positive-definite function is automatically Hermitian-symmetric, $f(-x)=\overline{f(x)}$ (`IsPositiveDefinite.conj_neg`), which is exactly what makes a representation by a genuine (positive) probability measure possible, rather than a signed or complex one. The theorem works with `f` continuous and normalized. No further hypothesis (in particular, no integrability of `f`) is assumed for the general representation theorem: the representing measure $\nu$ need not be absolutely continuous (e.g. for a periodic $f$, $\nu$ is a discrete measure supported on the harmonics of the period — this is Herglotz's 1911 theorem, the periodic special case). Under the extra hypothesis that `f` is Lebesgue-integrable, the representing measure becomes absolutely continuous with a continuous density: this density is `fourierTransform f`, the (real part of the) Fourier transform of `f` — automatically real-valued, again by Hermitian symmetry — and Fourier inversion recovers `f` from it.
## Formalization targets
### Goal — Bochner's theorem, general case
$$
f \text{ continuous, positive-definite, } f(0)=1 \;\Longrightarrow\; \exists\, \nu \text{ a probability measure on } \mathbb R,\; \forall x,\; f(x) = \int_{\mathbb R} e^{i2\pi\xi x}\,d\nu(\xi).
$$
The central representation theorem: no integrability hypothesis on $f$, so $\nu$ may be any probability measure, not necessarily a density.
### Milestone — Bochner's theorem, `L¹` (density) case
$$
f \text{ continuous, integrable, positive-definite, } f(0)=1 \;\Longrightarrow\; \tau:=\text{fourierTransform } f \text{ is continuous}, \;\tau \ge 0,\; \int \tau = 1, \text{ and } f(x) = \int e^{i2\pi\xi x}\tau(\xi)\,d\xi.
$$
The special case where the representing measure of the goal theorem is absolutely continuous with an explicit density — the form most directly usable in applications. Provable independently of the general goal theorem via classical Fourier-inversion machinery, so it is a natural, self-contained first target.
## Significance
Bochner's theorem is one of the load-bearing structural results of 20th-century harmonic analysis: it underlies Bochner–Minlos-type theorems for random fields, the entire theory of stationary Gaussian processes, kernel methods in statistics and machine learning, and (via its periodic specialization, Herglotz's theorem) the spectral theory of stationary time series. Formalizing it gives the platform a reusable, general-purpose characterization of positive-definite functions that any future mission on kernel methods, random features, or characteristic functions can build on directly.
## Difficulty
The general representation theorem is the harder target: the standard proof (see the Wikipedia article linked below) constructs, from `f`, a strongly continuous unitary representation of $\mathbb R$ on a Hilbert space via a GNS-type construction, then invokes Stone's theorem and the spectral theorem to extract the representing measure — a substantial functional-analytic argument, since `f` need not be integrable and $\nu$ need not have a density. The `L¹` milestone is comparatively more tractable: it can be attacked directly via Mathlib's existing Fourier-transform and Fourier-inversion machinery for integrable functions, plus the elementary fact (already available for reuse: `IsPositiveDefinite.conj_neg`) that a positive-definite function is Hermitian-symmetric.
## Formalization scope
`IsPositiveDefinite` is formalized exactly as the finite Hermitian-form condition above, over `Fin n → ℝ` point families and `Fin n → ℂ` coefficients, matching the standard convention in the literature, with `f : ℝ → ℂ` — the fully general, complex-valued statement, not restricted to real-valued kernels. `fourierTransform f ξ` is defined as the real part of `∫ Complex.exp(-i2πξ x) * f(x) dx`; this is provably the exact (not merely real-part-of) Fourier transform once `f` is positive-definite, since Hermitian symmetry forces the integral to be real already.
## Selected references
- [Bochner's theorem](https://en.wikipedia.org/wiki/Bochner%27s_theorem), Wikipedia — states the general locally-compact-abelian-group form and sketches the unitary-representation proof; a good map of the territory before diving into either target.
- Salomon Bochner, *Vorlesungen über Fouriersche Integrale*, Akademische Verlagsgesellschaft, 1932.
- Gustav Herglotz, *Über Potenzreihen mit positivem, reellem Teil im Einheitskreis*, Berichte über die Verhandlungen der Königlich Sächsischen Gesellschaft der Wissenschaften zu Leipzig, 1911.
- Walter Rudin, *Fourier Analysis on Groups*, Interscience, 1962, Chapter 1.