Harmonic Analysis

Motivation

For a set $E\subset\mathbb R^d$ the distance set is $\Delta(E)=\{|x-y|:x,y\in E\}$. Falconer (1985) asked how large a set must be, measured by Hausdorff dimension, to force $\Delta(E)$ to have positive length. Examples built from lattices show that dimension $d/2$ is not enough in general, and Falconer conjectured that any compact set of dimension strictly greater than $d/2$ suffices. The question is the continuous analogue of Erdős's distinct-distances problem and has been a driving problem for geometric measure theory and Fourier restriction theory: progress on it has repeatedly come from, and fed back into, spherical averages, restriction estimates, decoupling and radial projections.

Background

• 1985. Falconer proves the threshold $(d+1)/2$ and introduces the conjecture (doi:10.1112/S0025579300010998).
• 1987. Mattila's spherical-average criterion makes Fourier $L^2$ estimates the central approach (doi:10.1112/S0025579300013462).
• 1994. Bourgain connects improvements in dimensions two and three to restriction phenomena (doi:10.1007/BF02772994).
• 1999, 2005. Wolff reaches $4/3$ in the plane; Erdoğan reaches $d/2+1/3$ for $d\ge3$ (doi:10.1155/S1073792899000288, doi:10.1155/imrn.2005.1411).
• 2019–2021. Du, Guth, Ou, Wang, Wilson and Zhang reach $9/5$ in $\mathbb R^3$; Du and Zhang reach $d/2+1/4+1/(8d-4)$; Guth, Iosevich, Ou and Wang reach $5/4$ in the plane, with a pinned conclusion (arXiv:1802.10186, doi:10.4007/annals.2019.189.3.4, doi:10.1007/s00222-019-00917-x).
• 2019. Keleti and Shmerkin develop multiscale profile methods for planar distance sets (doi:10.1007/s00039-019-00500-9).
• 2023–2024. Orponen and Shmerkin prove the planar Furstenberg-set/projection estimates; Orponen, Shmerkin and Wang prove radial projection theorems; Du, Ou, Ren and Zhang improve higher-dimensional thresholds (arXiv:2106.03338, doi:10.1007/s00039-024-00660-3, arXiv:2309.04103).
• 2025. Shmerkin and Wang show $\dim_H\Delta(E)=1$ when the Hausdorff and packing dimensions both equal $d/2$ (doi:10.1007/s00039-024-00696-5).
• 2026. Liu proves the planar conclusion for sets with equal Hausdorff and packing dimension above one (arXiv:2603.15328).

The source of this mission is an OpenAI preprint dated September 23, 2026.

Setting

• $\mathbb R^d$ carries the Euclidean distance $|x-y|$.
• For $E\subset\mathbb R^d$, the Hausdorff dimension $\dim_HE$ is the infimum of $s\ge0$ for which the $s$-dimensional Hausdorff measure of $E$ vanishes.
• $\Delta(E)=\{|x-y|:x,y\in E\}\subset[0,\infty)$, and $\mathcal L^1$ is Lebesgue measure on $\mathbb R$.

Formalization targets

Milestone: the planar case

$$E\subset\mathbb R^2\ \text{compact},\ \dim_HE>1\ \Longrightarrow\ \mathcal L^1(\Delta(E))>0.$$

Goal: Theorem 1.1

$$d\ge2,\ E\subset\mathbb R^d\ \text{compact},\ \dim_HE>\tfrac d2\ \Longrightarrow\ \mathcal L^1(\Delta(E))>0.$$

The goal OAI.Falconer.falconer_distance_conjecture is open on the platform.

Significance

Theorem 1.1 resolves Falconer's distance conjecture in every dimension, with no regularity assumption beyond the strict dimension bound: no equality of Hausdorff and packing dimension, no Ahlfors regularity, no product structure. The threshold $d/2$ is sharp by Falconer's lattice examples, and no endpoint assertion is made. The result is unpinned: it does not assert that a single point $y\in E$ has $\mathcal L^1(\{|x-y|:x\in E\})>0$ at the threshold. Positive measure is stronger than $\dim_H\Delta(E)=1$.

The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists.

Difficulty

The classical route bounds the $L^2$ norm of a distance measure via spherical averages of Fourier transforms (Mattila), and every improvement so far has come from finer restriction or decoupling estimates, which stall above $d/2$. In higher dimensions there is a structural obstacle: radial projections of an $s$-dimensional source cannot gain dimension above $s$, so for $d/2<s<d-1$ one cannot assume radial projections have densities, and the angular input the Fourier argument needs must be built as cap bounds on directional fibres with arbitrarily small losses. Converting such fractal angular laws into a distance estimate requires a belt (rather than cap) estimate whose annular power is exactly balanced at $S=d/2$, and a recursive multiscale accounting whose costs must be paid by a potential across two separated depths.

Formalization scope

• Points live in EuclideanSpace ℝ (Fin d), so dist is the Euclidean distance.
• dimH E : ℝ≥0∞ is Mathlib's Hausdorff dimension; the hypothesis is (d : ℝ≥0∞) / 2 < dimH E, strict.
• The conclusion is 0 < volume {r : ℝ | ∃ x ∈ E, ∃ y ∈ E, dist x y = r} with Lebesgue volume on ℝ; compactness of $E$ makes this set compact.
• The planar milestone uses PlanarFalconer.distanceSet on EuclideanSpace ℝ (Fin 2) with 1 < dimH E.

A complete development needs Frostman's lemma, energy and Fourier characterizations of dimension, Mattila's spherical-average criterion, stationary phase for spherical oscillatory integrals, and the Orponen–Shmerkin planar incidence theorem (used as an external input). Contributions formalizing Lemma 5.5 (the classical distance threshold $(d+1)/2$), Theorem 4.1 (linear projection gain), Theorem 4.2 (planar discretized Furstenberg estimate), Proposition 5.10 (starting pair measures), Proposition 8.1 (graph estimate) and Theorem 10.4 (single-profile angular bound) are welcome.

Selected references

• OpenAI, The Falconer distance conjecture in all dimensions, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Falconer-distance-conjecture-in-all-dimensions-September-23-2026/paper.pdf
• K. J. Falconer, On the Hausdorff dimensions of distance sets, Mathematika, 1985. https://doi.org/10.1112/S0025579300010998
• P. Mattila, Spherical averages of Fourier transforms of measures with finite energy; dimensions of intersections and distance sets, Mathematika, 1987. https://doi.org/10.1112/S0025579300013462
• T. Wolff, Decay of circular means of Fourier transforms of measures, IMRN, 1999. https://doi.org/10.1155/S1073792899000288
• L. Guth, A. Iosevich, Y. Ou, H. Wang, On Falconer's distance set problem in the plane, Invent. Math., 2020. https://doi.org/10.1007/s00222-019-00917-x
• X. Du, L. Guth, Y. Ou, H. Wang, B. Wilson, R. Zhang, Weighted restriction estimates and application to Falconer distance set problem, Amer. J. Math., 2021. https://doi.org/10.1353/ajm.2021.0005
• T. Orponen, P. Shmerkin, On the Hausdorff dimension of Furstenberg sets and orthogonal projections in the plane, Duke Math. J., 2023. https://arxiv.org/abs/2106.03338
• T. Orponen, P. Shmerkin, H. Wang, Kaufman and Falconer estimates for radial projections and a continuum version of Beck's theorem, Geom. Funct. Anal., 2024. https://doi.org/10.1007/s00039-024-00660-3
• P. Shmerkin, H. Wang, On the distance sets spanned by sets of dimension d/2 in $\mathbb R^d$, Geom. Funct. Anal., 2025. https://doi.org/10.1007/s00039-024-00696-5
• X. Du, Y. Ou, K. Ren, R. Zhang, New improvement to Falconer distance set problem in higher dimensions, preprint, 2024. https://arxiv.org/abs/2309.04103

Motivation

Reaction–diffusion equations $u_t = \Delta u + f(u)$ are the standard model for the interplay of diffusion with local growth or decay: chemical kinetics, population dynamics, and the bifurcation of equilibria of partial differential equations. The special case

$$u_t = \Delta u + \lambda u - \gamma u^m$$

(the Chafee–Infante equation on bounded domains, Chafee and Infante 1974) is the model equation for loss of stability: $u = 0$ is linearly stable for $\lambda < 0$ and unstable for $\lambda > 0$, and for $m = 3$, $\gamma > 0$ the reaction term produces a supercritical pitchfork bifurcation. Before any of that dynamics can be studied, one needs solutions to exist. §5.5 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis, revised 6/18/2014) proves local existence by rewriting the equation as an integral equation and applying the contraction mapping theorem. This argument, the "mild solution" method of Kato and Segal, is the template for local well-posedness of semilinear parabolic and dispersive equations (Pazy 1983, Henry 1981).

Setting

Write $\mathbb{R}^n$ for Euclidean space with Lebesgue measure. For $f \in L^2(\mathbb{R}^n)$ the Fourier transform is $\hat f(k) = (2\pi)^{-n}\int f(x)e^{-ik\cdot x}\,dx$, defined by this formula on Schwartz functions and extended to $L^2$ by Plancherel's theorem. For $s \ge 0$, the Sobolev space $H^s(\mathbb{R}^n)$ consists of the $f \in L^2$ with finite norm

$$\|f\|_{H^s} = \Big((2\pi)^n \int_{\mathbb{R}^n} (1+|k|^2)^{s}\,|\hat f(k)|^2\,dk\Big)^{1/2}.$$

The heat semigroup $e^{-tA}$, $A = -\Delta$, is the Fourier multiplier $\widehat{e^{-tA}h}(k) = e^{-t|k|^2}\hat h(k)$. For $t > 0$ it is convolution with the heat kernel $\Gamma_t(x) = (4\pi t)^{-n/2}e^{-|x|^2/4t}$.

Fix $\lambda, \gamma \in \mathbb{R}$ and an integer $m \ge 1$, and let $F(h) = \lambda h - \gamma h^m$ act pointwise on functions. The initial value problem is

$$u_t = \Delta u + \lambda u - \gamma u^m, \qquad u(x,0) = g(x). \tag{5.34}$$

Write $C([0,T];H^s)$ for the curves $t \mapsto u(t) \in H^s$ that are continuous on $[0,T]$ in the $H^s$ norm, normed by $\sup_{0\le t\le T}\|u(t)\|_{H^s}$. A mild solution on $[0,T]$ with values in $H^{2\alpha}$ is a curve $u \in C([0,T];H^{2\alpha})$ satisfying the Duhamel formula

$$u(t) = e^{-tA}g + \int_0^t e^{-(t-s)A}F(u(s))\,ds \qquad (0 \le t \le T).$$

The right-hand side, viewed as a function of $u$, is the map $\Phi(u)$.

Formalization targets

Goal: local existence and uniqueness (Theorem 5.49)

Let $1 \le n \le 3$ and $n/4 < \alpha < 1$. For every $R > 0$ there is $T > 0$, depending only on $\alpha, n, R, \lambda, \gamma, m$, such that for every $g$ with $\|g\|_{H^{2\alpha}} \le R$, (5.34) has a mild solution $u \in C([0,T];H^{2\alpha})$, and any two mild solutions on $[0,T]$ coincide.

Milestones

• Smoothing (Lemma 5.50). For $\alpha > 0$ there is $C = C(\alpha,n)$ with

$$\|e^{-tA}h\|_{H^{2\alpha}} \le \frac{Ce^t}{t^\alpha}\|h\|_{L^2} \qquad (t > 0,\ h \in L^2).$$

• Fractional Sobolev embedding (Theorem 5.79). If $0 < s < n/2$ and $1/q = 1/2 - s/n$, then $\|f\|_{L^q} \le C\|f\|_{H^s}$. If $s > n/2$, then every $f \in H^s$ is a.e. equal to a continuous function vanishing at infinity, and $\|f\|_{L^\infty} \le C\|f\|_{H^s}$.
• Local Lipschitz bound for $\Phi$ (Lemma 5.51). For $n/4 < \alpha < 1$, $\Phi$ maps $C([0,T];H^{2\alpha})$ to itself, and for $0 < T \le T_0$

$$\|\Phi(u)-\Phi(v)\| \le C T^{1-\alpha}\big(1 + \|u\|^{m-1} + \|v\|^{m-1}\big)\|u - v\|,$$

where all norms are in $C([0,T];H^{2\alpha})$ and $C$ depends on $\alpha, m, n, \lambda, \gamma, T_0$.

Significance

The theorem is the base case of the semigroup approach to nonlinear evolution equations. The existence time depends only on the size of the data, so an a priori bound on $\|u(t)\|_{H^{2\alpha}}$ upgrades local existence to global existence. The same scheme, with $X = \mathcal D(A^\alpha)$ for a sectorial operator $A$, covers general semilinear parabolic problems. The smoothing estimate and the fractional Sobolev embedding are also used separately, in parabolic regularity theory and in the analysis of dispersive equations.

The results are classical and proved in the notes. None of them has a machine-checked proof on this platform. Mathlib has the $L^2$ Fourier transform and Plancherel's theorem, tempered distributions, and a Bessel-potential definition of Sobolev spaces, but no fractional Sobolev embedding on $\mathbb{R}^n$ and no mild-solution theory for semilinear heat equations. The mission asks for complete formal proofs of the three milestones and the goal, stated for the concrete objects above.

Difficulty

The obvious fixed-point argument needs three separate analytic inputs. The first is that the $L^2 \to H^{2\alpha}$ operator norm of $e^{-tA}$ blows up like $t^{-\alpha}$, which is integrable only because $\alpha < 1$. The second is that $F$ is locally Lipschitz from $H^{2\alpha}$ to $L^2$, which needs the embedding $H^{2\alpha} \hookrightarrow L^\infty$ and fails for $\alpha \le n/4$. The third is that the Duhamel integral defines a continuous $H^{2\alpha}$-valued curve even though its integrand is singular at $s = t$. With these in hand, the contraction must be run on a ball whose radius is fixed by the data, with $T$ chosen uniformly over that ball. Uniqueness is claimed in all of $C([0,T];H^{2\alpha})$, not only in the ball where the contraction runs, so an extra argument is needed to exclude solutions that leave the ball.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) with volume. The solution and the data are real-valued. Theorem 5.79 and Lemma 5.50 are stated for complex-valued functions. A curve is a map ℝ → (ℝⁿ → ℝ), and only its values on $[0,T]$ matter.
• Fourier normalization. The book's $\hat f(k) = (2\pi)^{-n}\int f e^{-ik\cdot x}$ is obtained from Mathlib's $L^2$ transform Lp.fourierTransformₗᵢ (kernel $e^{-2\pi i\langle x,\xi\rangle}$, no prefactor) as $\hat f(k) = (2\pi)^{-n}\mathcal F f(k/2\pi)$. Mathlib's constants are never used for the book's.
• $H^s$ norm. hsNorm is valued in $[0,\infty]$ and is $\infty$ off $L^2$, so $f \in H^s$ means hsNorm n s f < ⊤. The factor $(2\pi)^n$ is inside the square root, as in the book's inner product and in its proof of Lemma 5.50. Definition 5.74 prints it outside, which is inconsistent with both. With this choice $\|f\|_{H^0} = \|f\|_{L^2}$.
• Semigroup. $e^{-tA}$ is convolution with the heat kernel for $t > 0$, which agrees with the multiplier (5.37) on $L^2$, and the identity at $t = 0$. No abstract semigroup theory is used.
• Duhamel integral. It is taken pointwise in $x$, and (5.39) is required for almost every $x$ at each $t \in [0,T]$. For curves in $C([0,T];H^{2\alpha})$ with $\alpha > n/4$, the integrand is bounded, so this is the book's $L^2$-valued integral.
• Constants and corrections. The data dependence of $T$ is read as uniform over the ball $\|g\|_{H^{2\alpha}} \le R$. In Lemma 5.51 the constant, announced as $C(\alpha,m,n)$, is allowed to depend on $\lambda, \gamma$ and on an upper bound $T_0$ for $T$. The hypothesis $\alpha < 1$ is added. Both corrections are used by the notes' own proof, and without them the printed inequality fails for large $T$. Theorem 5.79 prints its inequalities without the constant $C$ it announces, and the constant is restored. Throughout, $m \ge 1$.
• Trivializing readings excluded. The norms are $[0,\infty]$-valued and $\infty$ off $L^2$, so no bound holds through a junk value $0$. A mild solution must satisfy the Duhamel identity and be continuous in $H^{2\alpha}$, so existence cannot be met by an unconstrained curve. Uniqueness is stated over all mild solutions on $[0,T]$, not over a ball.
• Infrastructure. A complete development needs Plancherel in the book's normalization, the heat-kernel/multiplier identity on $L^2$, Bochner or pointwise integration of $L^2$-valued curves, the Banach fixed-point theorem on a closed ball of $C([0,T];H^{2\alpha})$, and the fractional Sobolev embedding. The embedding and the smoothing estimate can be reused beyond this mission. Contributions of the $H^s$ theory as a normed space are welcome.

Selected references

• J. K. Hunter, Notes on Partial Differential Equations, UC Davis lecture notes, revised 6/18/2014, §5.5 and Appendices 5.C–5.D. https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf
• N. Chafee and E. F. Infante, A bifurcation problem for a nonlinear partial differential equation of parabolic type, Applicable Analysis 4 (1974), 17–37. https://doi.org/10.1080/00036817408839081
• A. Pazy, Semigroups of Linear Operators and Applications to Partial Differential Equations, Springer, 1983. https://doi.org/10.1007/978-1-4612-5561-1
• D. Henry, Geometric Theory of Semilinear Parabolic Equations, Lecture Notes in Mathematics 840, Springer, 1981. https://doi.org/10.1007/BFb0089647

Why trace class representations matter

A strongly continuous unitary representation turns each group element into a unitary operator on a Hilbert space. Averaging those operators against a smooth, compactly supported function gives a bounded operator. When every such average is trace class, its trace defines a distribution character. The trace condition is therefore a bridge from an operator representation to a scalar distribution that can be studied by harmonic analysis. Van Dijk, Neeb, Salmasian and Zellner collect and extend characterizations of this condition for finite-dimensional Lie groups in their 2015 preprint. Their Theorem 1.3 is the target here.

The authors identify one of the equivalences, between the trace class property and a trace class negative power of the Nelson Laplacian, with an earlier statement of Cartier that had appeared without a proof or reference. Their further conclusion that one finite degree of differentiability suffices is presented as a new result; it gives finite order for the distribution character. These are claims about the cited preprint, not claims of prior machine verification. Source: introduction and Theorem 1.3, pp. 2–5.

The representation and its test functions

Let $G$ be a finite-dimensional real Lie group, let $H$ be a complex Hilbert space, and let $\pi:G\to\mathrm U(H)$ be a strongly continuous unitary representation. Fix a left Haar measure $\mu$. For a compactly supported continuous function $f:G\to\mathbb C$, the integrated operator is $\pi(f)v=\int_G f(g)\pi(g)v\,d\mu(g)$ for each $v\in H$. Write $C^m_c(G)$ for compactly supported functions with $m$ continuous derivatives and $C^\infty_c(G)$ for smooth compactly supported functions. Write $B_1(H)$ and $B_2(H)$ for the trace class and Hilbert–Schmidt ideals of bounded operators on $H$.

Choose a basis $X_1,\ldots,X_n$ of the Lie algebra $\mathfrak g$. The Nelson Laplacian is $\Delta=\sum_{j=1}^n X_j^2$ in the enveloping algebra. The derived representation applies $d\pi(\Delta)$ on smooth vectors. Its closure $D=\overline{d\pi(\Delta)}$ is a non-positive self-adjoint operator, and $(1-D)^{-1}$ is bounded. The choice of basis determines $D$, while the theorem holds for an arbitrary fixed basis. Source: §1 and proof of Theorem 1.3, pp. 3–4.

Formalization targets

Five equivalent conditions

The mission goal is the complete five-way equivalence in Theorem 1.3:

$$\begin{aligned} \text{(i)}\;&\exists m\ge1:\ \pi(C^m_c(G))\subseteq B_1(H) \text{ and }\pi:C^m_c(G)\to B_1(H)\text{ is continuous};\\ \text{(ii)}\;&\pi(C^\infty_c(G))\subseteq B_1(H) \text{ and }\pi:C^\infty_c(G)\to B_1(H)\text{ is continuous};\\ \text{(iii)}\;&\pi(C^\infty_c(G))\subseteq B_1(H);\\ \text{(iv)}\;&\pi(C^\infty_c(G))\subseteq B_2(H);\\ \text{(v)}\;&\exists k\ge1:\ (1-D)^{-k}\in B_1(H). \end{aligned}$$

The continuity clauses are part of the target; they cannot be inferred merely from the displayed inclusions. The milestone list includes the four nontrivial implications named in the paper's proof, its finite-order claim and the two displayed identities needed to connect the function and operator Laplacians. Source: Theorem 1.3 and proof, pp. 3–5.

What the equivalence gives

Condition (iii) is formulated using every smooth compactly supported function. Condition (i) replaces smoothness by one finite differentiability order that works uniformly for the representation, while retaining continuity into the trace class ideal. This is the form needed to conclude that the distribution character has finite order. Condition (v) tests the same property with one operator associated with the Lie algebra basis. These consequences are stated by the authors in the introduction and derived in §1. Source: pp. 2–5.

A formal proof would connect Lie-group differentiation, Bochner integration, Schatten ideals and the topology of compactly supported function spaces in one reusable development. The target and milestones here are open Lean statements: compilation checks their types, not their proofs. The previously posed Lemmas 1.1 and 1.2 of the same paper remain separate open platform items, and can be used by solvers without being re-posed here.

Where the difficulty lies

Showing that each $\pi(f)$ is trace class does not immediately give continuity of $f\mapsto\pi(f)$ in trace norm: operator-norm convergence alone does not control trace norm. The paper also needs to pass from trace class images of smooth functions to an operator statement about $(1-D)^{-k}$, and then back to functions with only finitely many derivatives. The obvious shortcut of treating $d\pi(\Delta)$ as a bounded operator fails because its natural domain is the smooth-vector space and its closure is generally unbounded. The proof therefore has substantial analytic content beyond elementary ideal inclusions. Source: proof of Theorem 1.3, pp. 4–5.

Formalization scope

Lean represents $G$ as a Hausdorff finite-dimensional Lie group modelled on a finite-dimensional real normed space $E$, equipped with a regular left Haar measure. It represents $H$ as a complete complex inner-product space, without a separability assumption, and the representation by a strongly continuous monoid homomorphism into unitary continuous linear equivalences. The Lie algebra is the tangent space $E$ at the identity, and the basis is an arbitrary finite basis of $E$. The quantifiers for $m$ and $k$ include explicit lower bounds $1\le m$ and $1\le k$, matching the paper's convention $\mathbb N_0=\mathbb N\cup\{0\}$.

Smooth vectors are exactly those whose orbit maps are smooth. The derived action is the manifold derivative of that orbit map at the identity, used only on smooth vectors. The function-side Laplacian uses right-invariant directional derivatives; its second-order sign agrees with the paper's action. A bounded operator $R$ is characterized by $R(w-d\pi(\Delta)w)=w$ on every smooth vector. The paper's essential self-adjointness and density statement identifies this $R$ uniquely with $(1-D)^{-1}$; the theorem carries that characterization as a hypothesis. The hypothesis must be satisfiable, and the interpretation must remain the paper's resolvent.

Continuity on $C^m_c(G)$ is encoded by a bound on the Schatten $1$-norm for every compact support set, with one constant for all functions supported there. For $C^\infty_c(G)$, the derivative order may depend on the compact set. The Schatten norms and classes are reused published definitions, with norm values in $[0,\infty]$; no alternate trace norm is introduced. Equation (1) is an identity of distributions tested against smooth compactly supported functions. A complete proof needs the smooth-vector integration lemma, Lie-group test-function approximation, the function-side parametrix and operator ideal estimates. These components are useful beyond this mission.

Selected references

• G. van Dijk, K.-H. Neeb, H. Salmasian and C. Zellner, On the characterization of trace class representations and Schwartz operators, arXiv preprint, 2015, arXiv:1512.02451v1.

Motivation

Integrals of polynomial functions of the matrix entries of a random element of a compact group appear across mathematical physics and probability: in random matrix theory (moments of Haar-distributed unitary, orthogonal and symplectic matrices), in lattice gauge theory (the link integrals of $U(N)$ gauge fields), and in quantum information (averages of quantum channels over random unitaries, twirling, unitary designs). Weingarten first computed asymptotics of such integrals for $U(N)$ in 1978 (Weingarten, J. Math. Phys. 19 (1978)); Collins (IMRN 2003) and Collins–Śniady (CMP 2006) gave exact formulas for the unitary, orthogonal and symplectic groups in terms of what is now called the Weingarten function.

The survey of Collins, Matsumoto and Novak, The Weingarten Calculus (arXiv:2109.14890), isolates the single statement underneath all these formulas, valid for every compact group and every finite-dimensional unitary representation. This mission formalizes that statement, Theorem 2.1 of the survey, together with the steps of its proof as written in Section 2.

Setting

Let $G$ be a compact Hausdorff topological group and $\mu$ its Haar probability measure, the unique Borel probability measure on $G$ invariant under left translation. Let $H=\mathbb{C}^N$ with its standard orthonormal basis $e_1,\dots,e_N$, and let $U:G\to\mathrm U(N)$ be a continuous group homomorphism into the unitary $N\times N$ matrices. Its matrix elements are $U_{xy}(g)=\langle e_x,U(g)e_y\rangle$, the $(x,y)$ entry of $U(g)$.

Fix $d\in\mathbb N$. A multi-index is a function $i:[d]\to[N]$; the set of them is $\mathrm{Fun}(d,N)$. The Weingarten integrals of degree $d$ are

$$I_{ij}=\int_G\prod_{x=1}^d U_{i(x)j(x)}(g)\,d\mu(g),\qquad i,j\in\mathrm{Fun}(d,N).$$

The tensor power $H^{\otimes d}$ has the orthonormal basis $e_i=e_{i(1)}\otimes\cdots\otimes e_{i(d)}$, and the tensor-power matrix $U^{\otimes d}(g)$ has entries $U^{\otimes d}_{ij}(g)=\prod_{x=1}^dU_{i(x)j(x)}(g)$. The invariant tensors are

$$(H^{\otimes d})^G=\{t\in H^{\otimes d}: U^{\otimes d}(g)\,t=t\ \text{for all }g\in G\},$$

and the Haar average is the matrix $P=\int_GU^{\otimes d}(g)\,d\mu(g)$. Given vectors $a_1,\dots,a_m\in H^{\otimes d}$, let $A=[\langle e_i,a_x\rangle]$ be the $N^d\times m$ matrix whose columns are their coordinates, $A^*$ its conjugate transpose, $A^*A=[\langle a_x,a_y\rangle]$ their Gram matrix, and, when it is invertible, $W=(A^*A)^{-1}$ the Weingarten matrix of $a_1,\dots,a_m$.

Formalization targets

Goal: Theorem 2.1 (p. 4)

If $a_1,\dots,a_m$ is a basis of $(H^{\otimes d})^G$, then for all $i,j\in\mathrm{Fun}(d,N)$

$$I_{ij}=\sum_{x,y=1}^mA_{ix}\,W_{xy}\,A^*_{yj}.$$

The identity is exact and holds for every compact group, every continuous unitary representation, every degree $d$ and every choice of basis; nothing is fixed beyond the data.

Milestones (Section 2, pp. 3–4)

1. $I_{ij}=P_{ij}$: the Weingarten integrals are the matrix elements of the Haar average.
2. $P^*=P$, $P^2=P$, and $\operatorname{im}P=(H^{\otimes d})^G$: $P$ is the orthogonal projection onto the invariant tensors (the existing platform theorem that a Haar average of a compact group representation is an idempotent fixing exactly the invariant vectors is included as a supporting reference item).
3. For linearly independent columns, the selfadjoint idempotent with image $\operatorname{span}\{a_x\}$ is $A(A^*A)^{-1}A^*$.

Significance

Theorem 2.1 reduces a family of analytic problems — Haar integrals of polynomials in matrix entries — to two algebraic ones: find a basis of the invariant tensors of $G$ in $H^{\otimes d}$ (classical invariant theory), and invert its Gram matrix. For $U(N)$ the invariants come from Schur–Weyl duality and the Weingarten matrix becomes the Weingarten function on permutations; for $O(N)$ and $Sp(N)$ the invariants are indexed by pair partitions; for the symmetric group $S(N)$ acting by permutation matrices the invariants are indicators of set partitions. Each of these case-specific formulas, surveyed in Sections 3–5 of the paper, is an instance of Theorem 2.1, so a formal proof of the theorem is the common entry point for formalizing any of them.

The theorem is classical and its proof is elementary once stated; it is not open. No machine-checked proof is known to exist in Mathlib or on this platform: Mathlib has Haar measure, unitary groups and Gram matrices (including the equivalence of linear independence with invertibility of the Gram matrix), but not the averaging projection of a representation in matrix form nor the formula $A(A^*A)^{-1}A^*$ for orthogonal projections. The mission produces both as reusable lemmas and the Fundamental Theorem itself.

Difficulty

The argument is short on paper; the formal work sits in three places. First, selfadjointness of $P$ needs $\int_GF(g^{-1})\,d\mu=\int_GF(g)\,d\mu$, i.e. unimodularity of a compact group, which Mathlib does not provide as an instance for non-commutative groups. Second, identifying the image of $P$ with the invariant tensors needs both directions: invariant vectors are fixed by $P$, and every vector $Pt$ is invariant, which uses left invariance of $\mu$ inside a matrix-valued Bochner integral. Third, the projection formula needs invertibility of $A^*A$ from linear independence and an argument that a selfadjoint idempotent is determined by its image. Commuting the integral with matrix entries and products is routine but must be done with care for the matrix norm chosen.

Formalization scope

• $H$ is $\mathbb C^N$ with its standard basis (a finite-dimensional Hilbert space with a specified orthonormal basis is the same thing after identification); $U$ is a monoid homomorphism G →* Matrix.unitaryGroup (Fin N) ℂ, assumed continuous. Indices are 0-based: $[N]$ is Fin N, multi-indices are Fin d → Fin N, tensors are (Fin d → Fin N) → ℂ.
• $G$ carries [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [BorelSpace G], and $\mu$ is a Haar measure that is a probability measure. Right invariance is not assumed; it is a consequence that solvers must prove.
• $d$ ranges over all of $\mathbb N$, including $d=0$, where both sides equal $1$; the paper takes $d$ positive.
• The inner product is conjugate-linear in the first slot, so $A^*_{yj}=\overline{A_{jy}}$ and $A^*$ is Mathlib's conjugate transpose.
• $P$ is a Bochner integral of matrices, taken with the entrywise sup norm; in finite dimension the integral is independent of the norm.
• The basis hypothesis is two hypotheses: LinearIndependent ℂ a and span (range a) = invariants U d, with the invariant subspace defined from the representation. Without independence Mathlib's matrix inverse returns $0$ on a singular Gram matrix, and the statement would be false; it is therefore not a trivializing gap but a necessary hypothesis.
• Correction. The paper says "a basis $a_1,\dots,a_m$ of $(H)^{\otimes d}$"; the same paragraph calls the $a_x$ "the basic invariants", and with a basis of all of $H^{\otimes d}$ the right-hand side would be the identity. The formal statement uses a basis of $(H^{\otimes d})^G$.
• A trivializing formalization — defining the Weingarten integral as $AWA^*$, defining the invariant space as the image of $P$, or assuming that $P$ projects onto the span of the $a_x$ — is excluded: the left side is the Haar integral of the product of matrix elements written out, and the invariant space is defined by $U^{\otimes d}(g)t=t$.

Needed infrastructure: matrix-valued Bochner integrals commuting with entries and with matrix multiplication; unimodularity of compact groups; the orthogonal-projection formula. All three are reusable well beyond this mission, and contributions of these general lemmas are welcome.

Selected references

• B. Collins, S. Matsumoto, J. Novak, The Weingarten Calculus, arXiv preprint, 2021. https://arxiv.org/abs/2109.14890
• D. Weingarten, Asymptotic behavior of group integrals in the limit of infinite rank, J. Math. Phys. 19 (1978), 999–1001. https://doi.org/10.1063/1.523807
• B. Collins, Moments and cumulants of polynomial random variables on unitary groups, the Itzykson–Zuber integral, and free probability, Int. Math. Res. Not. 2003, no. 17, 953–982. https://doi.org/10.1155/S107379280320917X
• B. Collins, P. Śniady, Integration with respect to the Haar measure on unitary, orthogonal and symplectic group, Comm. Math. Phys. 264 (2006), 773–795. https://doi.org/10.1007/s00220-006-1554-3