Formal Conjectures Portfolio: Bateman-Horn and CompanionsOpen Problem
## 1. Motivation
Wikipedia's pages on open problems are, for many mathematicians, the first contact with a
conjecture: a one-paragraph statement, a short history, a list of partial results. The
[Formal Conjectures](https://github.com/google-deepmind/formal-conjectures) library (Google
DeepMind, Apache-2.0) turned a large part of that material into Lean 4 statements, so that the
conjectures can be attacked — and, just as importantly, *stated unambiguously* — by machine.
This mission ports a coherent slice of that material to Prove2Me. It is deliberately a
**portfolio mission**: the goal theorem is the Bateman–Horn conjecture, the strongest single
statement in the collection, and the milestone list gathers the other conjectures and the
landmark theorems that surround them. Some milestones are genuine steps toward the goal (the
Bunyakovsky conjecture is literally the one-polynomial case); most are independent open problems
from other fields, grouped here because they share a source, a level of difficulty, and a need
for faithful formal statements. **A reader should not assume that proving a milestone advances
the goal theorem.** The mission's value is that every statement in it has been written against
the same Mathlib revision, checked to compile, and documented well enough to be attacked.
A rough timeline of the collection's landmarks:
- 1947 — Mills: a real $A>1$ with $\lfloor A^{3^n}\rfloor$ always prime.
- 1962 — Radó: the busy beaver function outgrows every computable function.
- 1971 — Davies: planar Kakeya sets have Hausdorff dimension $2$.
- 1978 — Apéry: $\zeta(3)$ is irrational.
- 1985 — Read (after Enflo, 1981): an operator on $\ell^1$ with no nontrivial closed invariant
subspace.
- 2001 — Zudilin: one of $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational.
- 2002 — Mihăilescu: $8$ and $9$ are the only consecutive perfect powers (Catalan's conjecture).
- 2009 / 2021 — Dvir; Bukh–Chao: the finite-field Kakeya bound and its sharp density constant.
- 2021 — Gardam: Kaplansky's *unit* conjecture is false (its zero-divisor and idempotent
companions remain open).
- 2024 — Saito: Mills' constant is irrational; bbchallenge: $\mathrm{BB}(5)=47\,176\,870$.
- 2025 — Wang–Zahl: the Kakeya set conjecture in $\mathbb{R}^3$.
## 2. Setting
The goal theorem concerns prime values of polynomials. Fix a finite set
$S=\{f_1,\dots,f_k\}\subseteq\mathbb{Z}[X]$ of distinct polynomials. Say that $f$ satisfies the
**Bunyakovsky condition** if its leading coefficient is positive, $\deg f\ge 1$, and $f$ is
irreducible over $\mathbb{Z}$; say that $S$ satisfies the **Schinzel condition** if for every
prime $p$ there is an integer $n$ with $p\nmid f_1(n)\cdots f_k(n)$ — i.e. no fixed prime divides
the product at every argument.
For a prime $p$ let $\omega_p(S)$ be the number of residue classes $n \bmod p$ at which some
$f_i$ vanishes, let $D=\prod_i \deg f_i$, and let
$$\pi_S(x)=\#\{\,n\le x : |f_i(n)| \text{ is prime for every } i\,\}.$$
The **Bateman–Horn constant** is the (conditionally convergent) Euler product
$$C=\lim_{N\to\infty}\ \prod_{p<N}\Big(1-\tfrac1p\Big)^{-k}\Big(1-\tfrac{\omega_p(S)}{p}\Big).$$
The other groups use their own vocabulary, each fixed in a definition item of this mission:
Kakeya sets in $\mathbb{R}^n$ and over $\mathbb{F}_q$; Mills' property
$\lfloor A^{3^n}\rfloor \in \mathbb{P}$; Wagstaff primes and Catalan–Mersenne numbers; polynomial
self-maps and their Jacobian matrix; nontrivial closed invariant subspaces; linear extensions of
a finite poset; Catalan's constant; and an explicit two-symbol Turing machine model with its
maximum-shifts function $\mathrm{BB}$.
## 3. Target
The goal theorem is the Bateman–Horn asymptotic: under the Bunyakovsky and Schinzel hypotheses,
$C$ exists and is positive and
$$\pi_S(x)\ \sim\ \frac{C}{D}\,\frac{x}{(\log x)^{k}}\qquad (x\to\infty).$$
Weaker statements in the same direction appear as milestones, first of all Bunyakovsky's
conjecture: under the same hypotheses with $k=1$, $f$ takes prime values infinitely often. The
remaining milestones are listed in the milestone panel and are grouped by subject: Diophantine
equations (Brocard, Pillai, Lebesgue–Nagell, Catalan/Mihăilescu), Mersenne-type primality
(New Mersenne, infinitude of Mersenne primes, Catalan–Mersenne), prime-representing constants
(Mills), geometric measure theory (Kakeya in $\mathbb{R}^n$, Kakeya over $\mathbb{F}_q$,
Falconer), operator theory (invariant subspace problem and Read's $\ell^1$ counterexample),
group algebras (Kaplansky's zero-divisor and idempotent conjectures), affine algebraic geometry
(the two-variable Jacobian conjecture), irrationality and transcendence ($\zeta(5)$, all odd zeta
values, Zudilin's theorem, $e+\pi$, $e\pi$, $\gamma$, Catalan's constant), order theory (the
$1/3$–$2/3$ conjecture), and computability (Radó's theorem).
## 4. Significance
*The results themselves.* Bateman–Horn is the quantitative form of Schinzel's hypothesis H: it
contains the twin prime conjecture, the infinitude of primes of the form $n^2+1$, and Bunyakovsky
as special cases, and it is the standard heuristic behind prime-counting predictions. The other
targets are each the headline question of their area: whether every bounded Hilbert-space
operator has an invariant subspace; whether group algebras of torsion-free groups are domains;
whether Kakeya sets must have full dimension. The solved milestones (Mihăilescu, Davies, Dvir,
Zudilin, Read, Saito, Radó) are landmarks whose formal proofs would be significant library
contributions in their own right.
*Formalizing them.* None of the open statements is expected to fall here; the concrete deliverable
is a set of faithful, compiling, reusable statements plus formal proofs of the solved milestones,
most of which are not in Mathlib today. Several are realistically in reach: the finite-field
Kakeya bound (Dvir's polynomial method is short), the elementary fact that $\pi+e$ and $\pi e$
cannot both be algebraic, and Radó's diagonal argument.
## 5. Difficulty
For Bateman–Horn, the obstruction is visible already for $k=1$, $\deg f = 2$: sieve methods bound
$\pi_S(x)$ from above by a constant times the conjectured main term and produce almost-primes,
but the parity problem blocks every known sieve from producing a single prime value of an
irreducible quadratic. The conditional convergence of the Euler product is a second, smaller
trap: the product over $p<N$ must be taken in order, so any reformulation as an unordered
infinite product changes the statement.
Each other group has its own obstruction, and they do not transfer: the parity problem says
nothing about Kakeya, where the difficulty is that dimension is not stable under the natural
compactness arguments, nor about the invariant subspace problem, where the known counterexamples
on $\ell^1$ show that no soft argument can work.
## 6. Formalization scope
Conventions this mission commits to, all fixed in the definition items:
- Polynomials are elements of `ℤ[X]`; primality of a polynomial value is primality of its
absolute value, and the counting function ranges over natural numbers $n \le \lfloor x\rfloor$.
- The Bateman–Horn constant is the limit of the *ordered* partial products over $p<N$, not an
unordered infinite product.
- Kakeya sets carry no compactness or measurability hypothesis, matching the source; the
conjecture is stated as an equality of Hausdorff dimensions in $[0,\infty]$.
- Falconer's hypothesis is written $d < 2\dim_H E$ to avoid division in $[0,\infty]$.
- Torsion-freeness of a group is spelled out as "every element of finite order is the identity",
which is the hypothesis the source intends (it is weaker than Mathlib's `IsMulTorsionFree`).
- Linear extensions are order-preserving bijections onto $\{0,\dots,|P|-1\}$, and probabilities
are quotients of set cardinalities in $\mathbb{Q}$.
- The busy beaver model is an explicit $n$-state, $2$-symbol machine with a bi-infinite Boolean
tape; $\mathrm{BB}$ counts transitions performed (maximum shifts), the halting transition
included, and $\mathrm{BB}(0)=0$.
- Several source statements are phrased as "is $X$ true?" with an unknown answer. Prove2Me
statements must be definite, so each such question is recorded in its **affirmative** form
(e.g. "$e+\pi$ is irrational"); a solver who can refute one should submit a disproof. The one
question with no statable answer, "what is $\mathrm{BB}(6)$?", is replaced by Radó's growth
theorem rather than guessed at.
- Nothing here is vacuous: each hypothesis set is satisfiable (e.g. closed unit balls are Kakeya
sets, and $X^2+1$ satisfies the Bunyakovsky and Schinzel conditions).
Contributions welcome: proofs of the solved milestones; sharper variants; and additional faithful
statements from the same source library, which contains far more than fits in one mission.
## 7. Selected references
- P. T. Bateman and R. A. Horn, *A heuristic asymptotic formula concerning the distribution of
prime numbers*, Math. Comp. 16 (1962), 363–367.
[DOI](https://doi.org/10.1090/S0025-5718-1962-0148632-7)
- T. Radó, *On non-computable functions*, Bell System Tech. J. 41 (1962), 877–884.
[DOI](https://doi.org/10.1002/j.1538-7305.1962.tb00480.x)
- R. O. Davies, *Some remarks on the Kakeya problem*, Math. Proc. Cambridge Philos. Soc. 69
(1971), 417–421. [DOI](https://doi.org/10.1017/S0305004100046867)
- C. J. Read, *A solution to the invariant subspace problem on the space $\ell_1$*, Bull. London
Math. Soc. 17 (1985), 305–317. [DOI](https://doi.org/10.1112/blms/17.4.305)
- K. Falconer, *On the Hausdorff dimensions of distance sets*, Mathematika 32 (1985), 206–212.
[DOI](https://doi.org/10.1112/S0025579300010998)
- W. Zudilin, *One of the numbers $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational*, Russian
Math. Surveys 56 (2001), 774–776. [DOI](https://doi.org/10.1070/RM2001v056n04ABEH000427)
- P. Mihăilescu, *Primary cyclotomic units and a proof of Catalan's conjecture*, J. reine angew.
Math. 572 (2004), 167–195. [DOI](https://doi.org/10.1515/crll.2004.048)
- Z. Dvir, *On the size of Kakeya sets in finite fields*, J. Amer. Math. Soc. 22 (2009),
1093–1097. [DOI](https://doi.org/10.1090/S0894-0347-08-00607-3)
- B. Bukh and T.-W. Chao, *Sharp density bounds on the finite field Kakeya problem*, Discrete
Analysis 26 (2021). [DOI](https://doi.org/10.19086/da.30071)
- G. Gardam, *A counterexample to the unit conjecture for group rings*, Ann. of Math. 194 (2021),
967–979. [DOI](https://doi.org/10.4007/annals.2021.194.3.9)
- K. Saito, *Mills' constant is irrational*, Mathematika 71 (2025), e70027.
[arXiv:2404.19461](https://arxiv.org/abs/2404.19461)
- H. Wang and J. Zahl, *Volume estimates for unions of convex sets, and the Kakeya set conjecture
in three dimensions*, [arXiv:2502.17655](https://arxiv.org/abs/2502.17655)
- Google DeepMind, *Formal Conjectures*, Apache-2.0,
[github.com/google-deepmind/formal-conjectures](https://github.com/google-deepmind/formal-conjectures)
---
*Provenance note.* The Lean statements in this mission are adaptations of the Formal Conjectures
library (Apache-2.0), rewritten to depend only on Mathlib and on this mission's own definition
items, and checked to compile against the platform's Mathlib revision. Each draft item carries a
read-back; **those read-backs are non-blind** — they were written by the same agent that drafted
the statements, and each says so in its first line. They are documentation, not independent
testimony.
42 thms2 active usersReviewed
🏆Completed
Captain: Elsie66
ClockRoPE: Random Fourier RotationsResearch Paper
## 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
Captain: Lucas
Gelbart's Langlands Survey I: Hecke's Correspondence between Automorphic Forms and Dirichlet SeriesResearch Paper
## Motivation
The Langlands program proposes that the arithmetic of number fields is encoded in the
representation theory of reductive groups over their adele rings. Its conjectures — reciprocity
and functoriality — are stated in the survey this mission formalizes,
[Gelbart 1984](https://doi.org/10.1090/S0273-0979-1984-15237-6), only after a long preparatory
part on the classical results they generalize, and it is that classical part (Part II of the
survey) that admits precise formal statements today.
The classical engine is a theorem of **Hecke** (1936): a holomorphic function on the upper
half-plane, given by a Fourier expansion in $e^{2\pi i n z/h}$, transforms in a prescribed way
under $z \mapsto -1/z$ **exactly when** the Dirichlet series built from its Fourier coefficients
continues analytically and satisfies a functional equation. One side of the equivalence is a
symmetry of an analytic object on the upper half-plane; the other is an analytic property of a
series assembled from arithmetic data. Gelbart presents this as the prototype of the
"reciprocity" that the Langlands conjectures extend to $GL_n$ and beyond.
Timeline of the material covered here.
- 1859: Riemann derives the functional equation of $\zeta(s)$ from the transformation law of the
Jacobi theta function, via the Mellin transform (Gelbart, §II.B.2, p. 187).
- 1920s: Hasse and Minkowski establish the local-global principle for rational quadratic forms
(Gelbart, §II.A, p. 186).
- 1936: Hecke proves the equivalence that is this mission's goal, and characterizes Euler
products among Dirichlet series of automorphic forms (Gelbart, §II.B.2, Theorems 1 and 2).
- 1967: Weil extends Hecke's theorem to congruence subgroups; Langlands formulates functoriality.
## Setting
Fix a sequence of complex numbers $a_0, a_1, a_2, \dots$ subject to the growth condition
$a_n = O(n^c)$ for some $c > 0$, a period $h > 0$, a weight $k > 0$, and a sign $C = \pm 1$.
Three objects are attached to this data.
- The **form**: $\displaystyle f(z) = \sum_{n \ge 0} a_n e^{2\pi i n z/h}$, holomorphic on the
upper half-plane $\{z : \operatorname{Im} z > 0\}$.
- The **Dirichlet series**: $\displaystyle \varphi(s) = \sum_{n \ge 1} \frac{a_n}{n^s}$,
absolutely convergent for $\operatorname{Re} s > c+1$.
- The **completed series**:
$\displaystyle \Phi(s) = \left(\frac{2\pi}{h}\right)^{-s} \Gamma(s)\, \varphi(s)$.
Two conditions on this data are compared.
$$\textbf{(A)}\quad \Phi(s) + \frac{a_0}{s} + \frac{C a_0}{k-s} \ \text{extends to an entire
function, bounded in every vertical strip, and}\ \Phi(k-s) = C\,\Phi(s).$$
$$\textbf{(B)}\quad f(-1/z) = C\left(\frac{z}{i}\right)^{k} f(z) \qquad (\operatorname{Im} z > 0).$$
Condition (B) says that $f$ is automorphic of weight $k$ for the group of transformations
generated by $z \mapsto z + h$ and $z \mapsto -1/z$; invariance under $z \mapsto z+h$ is built
into the Fourier expansion.
## Formalization targets
### Goal — Theorem 1 (Hecke), p. 188
$$\textbf{(A)} \iff \textbf{(B)}$$
for every coefficient sequence of polynomial growth and all $h, k > 0$, $C = \pm 1$. The goal
fixes no particular group, no level and no arithmetic input: it is the general equivalence, from
which the classical examples follow by specialization.
### Milestones
The milestone list follows the survey: the local-global principle of §II.A, the Riemann–theta
computation that motivates Hecke's proof (§II.B.2, p. 187), the Mellin representation of $\Phi$,
the two implications of Theorem 1 separately, and the Euler-product criterion of Theorem 2
(p. 189).
## Significance
Hecke's theorem is what makes "this $L$-function is automorphic" a checkable assertion: it
converts a statement about analytic continuation and a functional equation — often the only
handle one has on an arithmetically defined Dirichlet series — into the existence of an
automorphic form with prescribed Fourier coefficients. Weil's converse theorem, the modularity of
elliptic curves, and the automorphy criteria used throughout the Langlands program are
descendants of this statement. Downstream of it sit the classical applications listed in the
survey: the functional equations of $\zeta$ and of Dirichlet $L$-functions, and the
identification of theta series of quadratic forms with modular forms.
Status. Hecke's theorem is a classical, fully proved result (Hecke 1936; a textbook treatment is
Ogg, *Modular forms and Dirichlet series*, Ch. 1). Hasse–Minkowski is likewise classical. Neither
has a formalization in Mathlib at the pinned revision: Mathlib supplies the completed Riemann
zeta function and its functional equation, the Jacobi theta transformation law, `LSeries` and its
abscissa theory, the Gamma function and the Mellin transform, and modular forms with
`SlashAction`, but no converse theorem and no local-global principle for quadratic forms. What
this mission produces is therefore new formal mathematics on top of an old result, not a
re-derivation of something already machine-checked.
## Difficulty
The forward implication (B) $\Rightarrow$ (A) is Riemann's argument: split
$\int_0^\infty (f(iy) - a_0) y^{s-1}\,dy$ at $y = 1$, substitute $y \mapsto 1/y$ in the lower
piece, and use (B). The obstacle is not the algebra but the analysis that licenses it: exchanging
the sum defining $f$ with the integral, controlling $f(iy) - a_0$ as $y \to 0^{+}$, where the
naive termwise bound diverges, and showing the result is entire *and* bounded on vertical strips
rather than merely holomorphic on a half-plane.
The reverse implication (A) $\Rightarrow$ (B) is harder, and it is where the first idea fails: one
cannot simply run the computation backwards, because the Mellin inversion integral
$\frac{1}{2\pi i}\int_{(\sigma)} \Phi(s) y^{-s}\,ds$ converges only once boundedness in vertical
strips is combined with Stirling decay of $\Gamma$, and the contour shift that produces the $a_0$
terms needs both. Mathlib has the Mellin transform and an inversion theorem, under hypotheses that
are not met verbatim here; supplying that bridge is the main work.
## Formalization scope
Conventions committed to in Lean, all of them invisible in the prose.
- $f$ is defined as an unconditional `tsum` over $n \ge 0$, so it takes the junk value $0$ where
the series fails to converge; every statement about $f$ is guarded by $\operatorname{Im} z > 0$,
and a separate item asserts summability there.
- $\varphi$ is Mathlib's `LSeries`, whose $n = 0$ term is $0$ by definition, so $a_0$ never enters
the Dirichlet series — only the correction terms $a_0/s$ and $C a_0/(k-s)$.
- "Entire" is rendered as differentiability on all of $\mathbb{C}$; "bounded in every vertical
strip" as: for all reals $\sigma_1, \sigma_2$ there is an $M$ bounding the function on
$\sigma_1 \le \operatorname{Re} s \le \sigma_2$.
- The functional equation is imposed on the *continued* function $F$ as $F(k-s) = C\,F(s)$; for
$C = \pm 1$ this is equivalent to $\Phi(k-s) = C\,\Phi(s)$ on the half-plane of convergence.
- Complex powers $(2\pi/h)^{-s}$, $(z/i)^{k}$ and $y^{s-1}$ are principal-branch `cpow`; on the
upper half-plane $z/i$ has positive real part, so no branch ambiguity arises.
- The growth hypothesis is $\lVert a_n \rVert \le K n^{c}$ for $n \ge 1$ with $c > 0$, and the
abscissa used throughout is $\sigma = c+1$.
- The printed source reads $\Phi(s) + a_0/s + C/(k-s)$; the term $C a_0/(k-s)$ used here is the
standard form of the correction (see Ogg, Ch. 1), and the two agree when $a_0 = 0$.
No trivializing reading is available: condition (A) requires the entire function to *agree with*
$\Phi(s) + a_0/s + C a_0/(k-s)$ on $\operatorname{Re} s > c+1$, where $\Phi$ is genuinely defined,
so it is not satisfied by an arbitrary entire function; and the hypotheses of the goal are
satisfiable — the Jacobi theta coefficients with $h = 2$, $k = 1/2$, $C = 1$ are an instance,
recorded as its own item.
A complete development needs: summability and holomorphy of $q$-expansions of polynomial growth;
the Mellin transform of an exponentially decaying series; entirety and strip-boundedness of the
continued $\Phi$; Mellin inversion with Stirling control of $\Gamma$; and, for the Euler-product
item, the passage from multiplicativity to an Euler product for `LSeries`. All of these are
reusable beyond this mission. Contributions to any single item are welcome; the two implications
of the goal are independently valuable and are listed as separate milestones for that reason.
## Selected references
- S. Gelbart, *An elementary introduction to the Langlands program*, Bull. Amer. Math. Soc. (N.S.)
**10** (1984), 177–219. https://doi.org/10.1090/S0273-0979-1984-15237-6
- E. Hecke, *Über die Bestimmung Dirichletscher Reihen durch ihre Funktionalgleichung*, Math. Ann.
**112** (1936), 664–699. https://doi.org/10.1007/BF01565437
- A. Ogg, *Modular forms and Dirichlet series*, W. A. Benjamin, 1969.
- R. P. Langlands, *Problems in the theory of automorphic forms*, Lectures in Modern Analysis and
Applications III, Lecture Notes in Math. **170** (1970), 18–61.
https://doi.org/10.1007/BFb0079065
- J.-P. Serre, *A course in arithmetic*, Springer GTM 7, 1973 (Ch. IV: Hasse–Minkowski).
12 thms2 active usersReviewed
🏆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.