Harmonic Analysis

Motivation: the triangular Hilbert transform

The triangular Hilbert transform is a bilinear singular integral on the plane that couples translations in two different coordinate directions:

$$B(F,G)(x,y)=\mathrm{p.v.}\!\int_{\mathbb R}F(x+t,y)\,G(x,y+t)\,\frac{dt}{t}.$$

Paired with a third function, it becomes a trilinear form whose three inputs depend on the three pairs of variables of $(a,b,c)$. This "triangular" or entangled structure defeats the time–frequency methods that handle the one-dimensional bilinear Hilbert transform. Boundedness of this operator is a model problem for multilinear singular integrals with simplex structure, and is closely tied to norm convergence and variation of ergodic averages for two commuting transformations. Thiele listed the symmetric case ($L^3\times L^3\times L^3$) as Problem 13 in the 2017 collection Some problems in harmonic analysis.

Timeline

• 2010 — Demeter and Thiele study the two-dimensional bilinear Hilbert transform and highlight the flat triangular operator (Amer. J. Math.).
• 2012 — Kovač proves boundedness of the twisted paraproduct, a bipartite relative of the triangular form, by energy telescoping (Rev. Mat. Iberoam.).
• 2015 — Kovač, Thiele and Zorin-Kranich prove bounds for a Walsh (dyadic) model with one structurally restricted input (Forum Math. Sigma).
• 2016–2017 — Tao proves sublogarithmic cancellation for multilinear Hilbert transforms (Collect. Math.); Zorin-Kranich extends it to simplex Hilbert transforms (Math. Res. Lett.); Thiele's problem appears in Grafakos et al. (arXiv:1701.06637).
• 2019 — Durcik, Kovač, Škreb and Thiele obtain square-root cancellation across finitely many smooth scales (Ergodic Theory Dynam. Systems); Durcik, Kovač and Thiele prove power-type cancellation with hard truncations, still growing like $\sqrt{\log(R/\varepsilon)}$ at the symmetric point (J. Anal. Math.).
• 2021 — Durcik and Roos bound averages over directions (Proc. AMS); Christ, Durcik and Roos treat the curved variant along $(t,t^2)$ (Adv. Math.).
• 2026 — An OpenAI preprint, The maximal triangular Hilbert transform at the symmetric point (OpenAI Math Release, September 24, 2026), claims the scale-free $L^3\times L^3\to L^{3/2}$ bound for the maximal truncated operator. It has not been peer reviewed, and its proof is not formally verified.

Setting

For complex functions $F,G$ on $\mathbb R^2$ and $0<\varepsilon<R<\infty$, the hard truncation is

$$B_{\varepsilon,R}(F,G)(x,y)=\int_{\varepsilon<|t|<R}F(x+t,y)\,G(x,y+t)\,\frac{dt}{t},$$

and the maximal truncation is

$$B_*(F,G)(x,y)=\sup_{0<\varepsilon<R<\infty}\bigl|B_{\varepsilon,R}(F,G)(x,y)\bigr| .$$

For $F,G\in L^3(\mathbb R^2)$ the finite truncations converge absolutely outside a common null set, and $B_*$ is measurable (Lemma 7.1 of the source).

Formalization targets

Goal: the maximal triangular Hilbert transform is bounded at the symmetric point (Theorem 1.1)

There is an absolute constant $C$ such that, for all complex $F,G\in L^3(\mathbb R^2)$,

$$\|B_*(F,G)\|_{L^{3/2}(\mathbb R^2)}\le C\,\|F\|_{L^3(\mathbb R^2)}\|G\|_{L^3(\mathbb R^2)} .$$

The Lean goal also includes the measure-theoretic preliminaries of Lemma 7.1: almost every point is a point where all finite truncations converge absolutely, and $B_*$ is almost-everywhere measurable. The goal statement is published on the platform with status Open.

Significance

The result itself. A uniform bound for the maximal operator controls a truncation chosen independently at each point, which is stronger than a uniform bound on each $B_{\varepsilon,R}$. It yields existence of the joint principal value $B(F,G)$ almost everywhere and in $L^{3/2}$ (Theorem 7.2). By duality and a determinant-one change of variables, it gives endpoint-uniform bounds for the symmetric trilinear triangular form $\iiint G_0(a,b)G_1(b,c)G_2(c,a)\,\frac{da\,db\,dc}{a+b+c}$, which resolves Thiele's Problem 13 positively. Earlier bounds all grew with the number of scales.

Formalizing it. The estimate is a clean statement in Mathlib's $L^p$ and lower-integral language. Its proof combines matrix trace inequalities, Gaussian heat-flow energies and discretization limits, all of which would have to be built. The finite-dimensional matrix inequalities (Sections 2–3 of the source) are self-contained and reusable for other entangled multilinear forms.

Difficulty

Time–frequency analysis, which handles the one-dimensional bilinear Hilbert transform, does not adapt to the triangular form because its three inputs are entangled: each depends on a different pair of variables, so no single frequency-localization serves all three. Energy and telescoping methods (Kovač; Durcik) work for bipartite forms, but the triangular cycle is the documented obstruction. Previous cancellation estimates lose a factor depending on the number of scales $\log(R/\varepsilon)$. The maximal version adds a further difficulty: the truncation endpoints vary from point to point, so the energy argument must tolerate entries that switch on and off at independently chosen scales, without losses depending on the number of scales or on matrix dimensions.

Formalization scope

• Functions are ℝ × ℝ → ℂ with Lebesgue measure; hypotheses are MemLp F 3 and MemLp G 3 (which include a.e. strong measurability).
• truncation F G E z is the Bochner integral of $F(x+t,y)G(x,y+t)/t$ over $\{\varepsilon<|t|<R\}$, with endpoints packaged as Endpoints ($0<\varepsilon<R$).
• GoodPoint requires integrability on the annuli $1/(n+2)<|t|<n+2$ for all $n$, hence on every finite annulus. maximal is the ℝ≥0∞-valued supremum over all endpoint pairs at good points, and $0$ elsewhere. The goal asserts that almost every point is good, so this junk value cannot help.
• The norm is $\bigl(\int^- B_*^{3/2}\bigr)^{2/3}$ in ℝ≥0∞, compared with eLpNorm F 3 * eLpNorm G 3. The constant is an existential ℝ≥0, so it is finite and independent of $F,G$.
• Needed infrastructure: discretization of $L^3$ functions, finite-dimensional trace inequalities for $\operatorname{tr}((R^*R)^{3/2})$, Gaussian heat-flow monotonicity, one-dimensional Hardy–Littlewood maximal bounds, and limits of smooth truncations. Contributions on the matrix inequalities or the jump-control lemma are welcome.

Selected references

• C. Demeter and C. Thiele, On the two-dimensional bilinear Hilbert transform, Amer. J. Math. (2010). https://doi.org/10.1353/ajm.0.0101
• V. Kovač, Boundedness of the twisted paraproduct, Rev. Mat. Iberoam. https://doi.org/10.4171/RMI/707
• V. Kovač, C. Thiele and P. Zorin-Kranich, Dyadic triangular Hilbert transform of two general functions and one not too general function, Forum Math. Sigma (2015). https://doi.org/10.1017/fms.2015.25
• T. Tao, Cancellation for the multilinear Hilbert transform, Collect. Math. (2016). https://arxiv.org/abs/1505.06479v3
• P. Zorin-Kranich, Cancellation for the simplex Hilbert transform, Math. Res. Lett. (2017). https://doi.org/10.4310/MRL.2017.v24.n2.a16
• L. Grafakos, D. Oliveira e Silva, M. Pramanik, A. Seeger and B. Stovall, Some problems in harmonic analysis (2017), Section 9, Problem 13. https://arxiv.org/abs/1701.06637v1
• P. Durcik, V. Kovač, K. A. Škreb and C. Thiele, Norm-variation of ergodic averages with respect to two commuting transformations, Ergodic Theory Dynam. Systems (2019). https://doi.org/10.1017/etds.2017.48
• P. Durcik, V. Kovač and C. Thiele, Power-type cancellation for the simplex Hilbert transform, J. Anal. Math. (2019). https://doi.org/10.1007/s11854-019-0052-4
• OpenAI, The maximal triangular Hilbert transform at the symmetric point, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 2; Lemma 7.1, p. 24). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-maximal-triangular-Hilbert-transform-at-the-symmetric-point-September-24-2026/paper.pdf

Motivation

Martingale inequalities compare what a fluctuating process does along a path with how large its successive increments are. Such estimates are used in probability and harmonic analysis because a martingale can represent information revealed step by step, while its square function measures accumulated fluctuation. In his 1973 Wald Memorial Lectures, Burkholder developed distribution function inequalities that cover many choices of size measure at once, extending the power norm comparisons treated earlier in the paper. Burkholder, 1973

The target of this mission is Theorem 15.1 of that paper: a two sided comparison for every convex function of moderate growth. The paper attributes the decomposition of a martingale into small and large jumps to Davis, and cites a convex comparison lemma introduced in earlier work and subsequently treated by Garsia and Neveu. These attributions matter to the scope of the mission: the decomposition and lemma are separate, named milestones, while Burkholder's printed two sided inequality is the goal. Burkholder, 1973, §§14–16

Setting

Work on a probability space $(\Omega,\mathcal A,P)$ with an increasing sequence of sub sigma fields $\mathcal A_0,\mathcal A_1,\ldots$. A real martingale $f=(f_1,f_2,\ldots)$ is observed from time $1$ onward. Following the paper, put $f_0=0$ in the formulas for its differences: $d_1=f_1$ and $d_k=f_k-f_{k-1}$ for $k\ge2$. This convention differs from the index zero value required for a Lean martingale, which is discussed below.

The square function $S(f)$ and maximal function $f^*$ are pathwise quantities:

$$S(f)=\left(\sum_{k=1}^{\infty}d_k^2\right)^{1/2}, \qquad f^*=\sup_{k\ge1}|f_k|.$$

Either quantity can be infinite. Their finite versions stop at $n$: $S_n(f)$ sums the first $n$ squared differences, and $f_n^*$ takes the maximum through time $n$. For a positive exponent $p$, the paper writes $\|f\|_p=\sup_{n\ge1}(E|f_n|^p)^{1/p}$. The notation $E\Phi(Y)$ means the expectation of a nonnegative transform of a nonnegative random variable $Y$.

A function of moderate growth is a nondecreasing continuous $\Phi:[0,\infty]\to[0,\infty]$ with $\Phi(0)=0$ and

$$\Phi(2x)\le c_{(6.1)}\Phi(x)\qquad(x>0)$$

for some nonnegative growth constant $c_{(6.1)}$. The target adds convexity on finite nonnegative arguments. The examples $\Phi(x)=x$ and $\Phi(x)=x^p$ for $p\ge1$ satisfy these conditions. The paper sets aside $\Phi\equiv0$ as trivial; the Lean statements allow it because every displayed comparison still holds.

Formalization targets

The two sided convex comparison

The goal is precisely the form printed as Theorem 15.1:

$$C_1 E\Phi(S(f))\le E\Phi(f^*)\le C_2 E\Phi(S(f)), \qquad C_1,C_2>0.$$

The constants depend only on $c_{(6.1)}$, and are uniform over the probability space, filtration, martingale, and particular choice of $\Phi$ with that growth bound. The statement includes both sides; the paper writes a proof for the right side and says the left side follows by the same pattern. No integrability or boundedness is imposed on $f$ or on the two expectations. Burkholder, 1973, Theorem 15.1, pp. 33–34

Supporting statements

The milestones record the paper's good $\lambda$ lemma, Doob's cited maximal estimate, the predictable jump inequalities of §12, the quasi subadditivity of $\Phi$, Davis's decomposition and its jump bounds, and the convexity lemma of §16. The latter compares a sum of nonnegative random variables with the sum of their conditional expectations. Its two Neveu statements are retained as cited intermediate targets. These results identify distinct mathematical interfaces that a solver can formalize and reuse; the milestone text is transcribed from the indicated pages of the article.

Significance

The theorem lets one replace the expected convex transform of a path's maximum by the expected transform of its quadratic fluctuation, up to constants controlled by a single growth parameter. Choosing $\Phi(x)=x$ recovers the $L^1$ comparison displayed after Davis's decomposition; choosing a convex power gives the $p\ge1$ power cases. The assertion is useful even when one or both expectations are infinite, because it gives a uniform relation across the whole class of admissible martingales and functions. Burkholder, 1973, §§14–15

The result is proved in the paper. This mission asks for a machine checked Lean proof of the known theorem and of the selected statements that support it. The definitions for square and maximal functions, moderate growth, and nonnegative conditional projections can be reused in other martingale comparisons. A previously posed platform theorem about Robbins–Monro noise sums has the shape of one power function instance, but its process and time window differ; it does not supply this general result.

Difficulty

The size of a single martingale increment can dominate both a maximum and a square function. A direct comparison of the two pathwise expressions therefore gives no uniform expectation bound for arbitrary martingales and convex $\Phi$. The §12 estimates require predictable control of jumps, while the target has no such hypothesis. Davis's decomposition exposes the small and large jump contributions as different objects, and the §16 convexity lemma is needed to compare the conditional terms arising from large jumps. Convexity is essential for that lemma and for Theorem 15.1; the §12 good $\lambda$ statements themselves assume only moderate growth. Burkholder, 1973, §§12, 14–16

Formalization scope

Lean uses Mathlib's Martingale f ℱ P for a process indexed by natural numbers. The article begins at $1$ and uses $f_0=0$ only in its difference formulas. The definitions of $d_k$, $S(f)$, $f^*$, and $\|f\|_p$ therefore read positive indices and insert zero in the article's formulas; Lean's actual $f(0)$ is the compatible conditional expectation extension needed by Mathlib. Davis's partial sums also begin at $1$, and the decomposition theorem specifies the index zero extensions for its two martingales.

The square function, maximal function, $L^p$ norm, and all nonnegative expectations take values in $[0,\infty]$. This retains unbounded sample paths and nonintegrable expectations. For a nonnegative variable $z_k$, $E(z_k\mid\mathcal A_{k-1})$ is the extended conditional expectation condLExp, so a nonintegrable $z_k$ cannot silently become zero. Davis's signed $y_k$ is integrable, so its real conditional expectation uses Mathlib's ordinary conditional expectation. Predictable bounds such as $|d_k|\le w_k$ and the resulting claims are stated almost everywhere at each positive index.

The Lean predicate for moderate growth states the doubling law at zero and infinity as well as positive finite $x$; zero is automatic from $\Phi(0)=0$, and the endpoint at infinity follows by continuity in the nontrivial case. Convexity is read from finite real arguments. The zero function is included. A valid formalization must retain both inequalities in the goal and choose its constants before the martingale and $\Phi$; choosing constants after the data would make the goal much weaker.

The development needs finite and infinite square function sums, maximal functions, stopping and tail events, Mathlib martingales, conditional expectations, and convexity on the nonnegative reals. Contributions proving or improving any of the named milestones are welcome, including independent proofs of the cited Doob and Neveu statements. No extra boundedness or integrability assumption should be inserted into the goal to simplify a proof.

Selected references

• D. L. Burkholder, Distribution Function Inequalities for Martingales, The Annals of Probability 1(1), 1973, pp. 19–42. DOI.

Motivation

The free Schrödinger operator $H_0 = -\Delta$ is the Hamiltonian of a quantum particle, or of $N$ non-interacting particles, moving in $\mathbb R^n$ without external forces. Every Schrödinger operator $H = -\Delta + V$ studied in quantum mechanics is a perturbation of it, and each standard tool of the theory refers back to $H_0$: the Kato–Rellich theorem asks that $V$ be relatively bounded with respect to $H_0$, Weyl's theorem compares essential spectra with that of $H_0$, and scattering theory compares the dynamics $e^{-itH}$ with the free dynamics $e^{-itH_0}$. Knowing exactly what $H_0$ is (its domain, its self-adjointness, its spectrum and its time evolution) is therefore the base case of the spectral theory of Schrödinger operators.

All of this is obtained from one tool, the Fourier transform, which turns differentiation into multiplication. This mission follows Chapter 7 of G. Teschl, Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009), doi:10.1090/gsm/099. The chapter first develops the Fourier transform on the Schwartz space, on $L^1$ and on $L^2$, and then applies it to $H_0$. The same material appears in Reed–Simon (Vol. II, Sec. IX.1 and IX.7).

Setting

Write $\mathbb R^n$ for Euclidean space with $px = \sum_j p_j x_j$ and $x^2 = |x|^2$. For an integrable $f : \mathbb R^n \to \mathbb C$ the Fourier transform and its inverse are

$$\hat f(p) = \mathcal F(f)(p) = \frac{1}{(2\pi)^{n/2}}\int_{\mathbb R^n} e^{-ipx} f(x)\,d^nx, \qquad \check g(x) = \frac{1}{(2\pi)^{n/2}}\int_{\mathbb R^n} e^{ipx} g(p)\,d^np .$$

The Schwartz space $\mathcal S(\mathbb R^n)$ consists of the smooth functions all of whose derivatives decay faster than any polynomial. $L^1(\mathbb R^n)$ and $L^2(\mathbb R^n)$ are the usual Lebesgue spaces, and $C_\infty(\mathbb R^n)$ denotes the continuous functions vanishing at infinity. The convolution of $f, g \in L^1$ is $(f*g)(x) = \int f(y)g(x-y)\,d^ny$.

The Sobolev space is $H^2(\mathbb R^n) = \{\psi \in L^2 \mid p^2\hat\psi(p) \in L^2\}$. The free Schrödinger operator is

$$H_0\psi = -\Delta\psi = \mathcal F^{-1}\big(p^2\hat\psi(p)\big), \qquad \mathfrak D(H_0) = H^2(\mathbb R^n),$$

in units with $\hbar = 1$ and mass $m = 1/2$. Its time evolution is $e^{-itH_0}\psi = \mathcal F^{-1}(e^{-itp^2}\hat\psi)$. For a linear operator $A$ with domain $\mathfrak D(A)$, the resolvent set $\rho(A)$ is the set of $z \in \mathbb C$ for which $A - z$ maps $\mathfrak D(A)$ bijectively onto the Hilbert space with a bounded inverse $R_A(z)$, and the spectrum is $\sigma(A) = \mathbb C\setminus\rho(A)$. For self-adjoint $A$ and a vector $\psi$, the spectral measure $\mu_\psi$ is the finite Borel measure on $\mathbb R$ with $\langle\psi, R_A(z)\psi\rangle = \int (\lambda - z)^{-1}\,d\mu_\psi(\lambda)$ for all $z \notin \mathbb R$. The absolutely continuous, singular continuous and pure point spectra $\sigma_{ac}, \sigma_{sc}, \sigma_{pp}$ are the spectra of $A$ restricted to the vectors whose spectral measures are of the respective type. A subspace $D \subseteq \mathfrak D(A)$ is a core if the closure of $A|_D$ is $A$.

Formalization targets

Goal: Theorem 7.8

For $n \ge 1$, $H_0$ is self-adjoint and

$$\sigma(H_0) = \sigma_{ac}(H_0) = [0,\infty), \qquad \sigma_{sc}(H_0) = \sigma_{pp}(H_0) = \emptyset .$$

In the Lean statement the spectral-type part is the equivalent assertion that every spectral measure $\mu_\psi$ of $H_0$ is absolutely continuous with respect to Lebesgue measure.

Milestones

• Gaussians (Lemma 7.3). For $\operatorname{Re} z > 0$, $e^{-zx^2/2} \in \mathcal S(\mathbb R^n)$ and $\mathcal F(e^{-zx^2/2})(p) = z^{-n/2} e^{-p^2/(2z)}$, with $z^{n/2} = (\sqrt z)^n$ for the principal root.
• Inversion on $\mathcal S$ (Theorem 7.4). $\mathcal F$ is a bijection of $\mathcal S(\mathbb R^n)$ with inverse $g \mapsto \check g$, and $\mathcal F^2 f(x) = f(-x)$, so $\mathcal F^4 = \mathbb I$.
• Plancherel (Theorem 7.5). $\mathcal F$ extends to a unitary operator on $L^2(\mathbb R^n)$ with $\sigma(\mathcal F) = \{1,-1,i,-i\}$.
• Riemann–Lebesgue (Lemma 7.6). $\mathcal F : L^1 \to C_\infty$ is injective and $\|\hat f\|_\infty \le (2\pi)^{-n/2}\|f\|_1$.
• Convolution (Lemma 7.7). $f * g \in L^1$, $\|f*g\|_1 \le \|f\|_1\|g\|_1$ and $(f*g)^\wedge = (2\pi)^{n/2}\hat f\hat g$.
• Core (Lemma 7.9). $C_c^\infty(\mathbb R^n)$ is a core for $H_0$.
• Asymptotics (Lemma 7.10). For $\psi \in L^2$, $e^{-itH_0}\psi(x) - (2it)^{-n/2} e^{ix^2/(4t)}\hat\psi(x/(2t)) \to 0$ in $L^2$ as $|t|\to\infty$.

Significance

The result. Theorem 7.8 says that a free quantum particle has no bound states and that its energy spectrum is purely absolutely continuous and fills $[0,\infty)$. Combined with the RAGE theorem this gives the escape of every free wave packet from bounded regions, and Lemma 7.10 makes the escape quantitative: at large times the position distribution is the momentum distribution rescaled by $2t$. The self-adjointness of $H_0$ on $H^2(\mathbb R^n)$ and the core $C_c^\infty(\mathbb R^n)$ are the inputs to the Kato–Rellich treatment of atomic Hamiltonians, and $\sigma_{ess}(H_0) = [0,\infty)$ is the reference spectrum of Weyl's theorem and of the HVZ theorem.

Formalizing it. The results are classical. Mathlib contains the Fourier transform on $L^1$, Schwartz space and $L^2$ in the normalization $e^{-2\pi i\langle x,\xi\rangle}$ (including Fourier inversion, Riemann–Lebesgue and the $L^2$ isometry), and the Prove2Me corpus holds several of these as FamousTheorems in that normalization. What is missing is Teschl's normalization with its constants, the spectrum of the $L^2$ Fourier transform, the operator $H_0$ as an unbounded self-adjoint operator, its resolvent spectrum and spectral type, and the free dynamics. This mission produces these objects in a form the later chapters (Kato–Rellich for atoms, Weyl, HVZ, scattering) can build on.

Difficulty

The Fourier-analytic milestones are close to Mathlib but not in it: every constant has to be transported from the $2\pi$-in-the-exponent convention to Teschl's $(2\pi)^{-n/2}$ convention, including the branch of $z^{n/2}$ in Lemma 7.3 and the phase $(2it)^{-n/2}$ in Lemma 7.10. The lower bound $\sigma(\mathcal F) \supseteq \{1,-1,i,-i\}$ in Theorem 7.5 needs an eigenfunction for each fourth root of unity, which the book defers to the Hermite functions of Section 8.3.

For the goal, self-adjointness and $\sigma(H_0) = [0,\infty)$ require working with the resolvent spectrum of an unbounded LinearPMap, which Mathlib does not provide, and transporting self-adjointness and resolvents through the unitary Fourier transform. The spectral-type statement requires identifying the spectral measure $\mu_\psi$ of an unbounded operator from its resolvent alone, without a spectral theorem in the library, and showing that it has a density for every $\psi \in L^2$, not only for nice $\psi$. Lemma 7.9 is a statement about the graph norm of $-\Delta$, which is not controlled by the $L^2$ norm alone.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), so that $px$ and $x^2$ are the Euclidean ones, and $L^2(\mathbb R^n)$ is Lp ℂ 2 volume. fourier and fourierInv are Teschl's integrals (7.3) and (7.8) with the prefactor $(2\pi)^{-n/2}$. The $L^2$ transform $\hat\psi$ (fourierL2) is Mathlib's unitary $L^2$ transform rescaled by $\hat\psi(p) = (2\pi)^{-n/2}(\mathcal F_{\mathrm M}\psi)(p/2\pi)$, and Theorem 7.5 asserts that it is the unitary extension of (7.3). $H_0$ (freeHamiltonian) and $e^{-itH_0}$ (timeEvolution) are defined as Fourier conjugates of the maximal multiplication operator by the symbol of $-\Delta$ and of multiplication by $e^{-itp^2}$, written with Mathlib's $L^2$ transform, where the symbol is $4\pi^2|\xi|^2$. These are the same operators as Teschl's, and the domain is exactly $H^2(\mathbb R^n)$. Unbounded operators are Mathlib LinearPMaps, self-adjointness is Mathlib's IsSelfAdjoint, and the resolvent and spectrum are the bijective-with-bounded-inverse notions of Teschl, p. 73, not Mathlib's Banach-algebra spectrum, which is used only for the bounded operator $\mathcal F$ in Theorem 7.5. Statements that need it carry $n \ge 1$, which the book leaves implicit.

No projection-valued measure or functional calculus is taken as data. The spectral types in (7.25) are expressed through the spectral measures $\mu_\psi$, and these are pinned down intrinsically by their Borel transforms $\langle\psi, R_{H_0}(z)\psi\rangle$.

A trivializing formalization is ruled out: $\sigma(H_0)$ is the resolvent spectrum of the operator, not the essential range of $p^2$, so $\sigma(H_0) = [0,\infty)$ is not a computation on a multiplication symbol. The absolutely continuous measure in the goal must reproduce the actual resolvent matrix elements, so it cannot be chosen freely, and $e^{-itH_0}$ is not defined by its integral kernel (7.30).

A complete development needs change of normalization lemmas for the Fourier transform, the Hermite eigenfunctions of $\mathcal F$, unitary equivalence of LinearPMaps and its effect on adjoints and resolvents, self-adjointness of maximal real multiplication operators, polar coordinates on $\mathbb R^n$, and graph-norm approximation by cut-offs. The normalization bridge and the multiplication-operator results are reusable across the series. Contributions of either are welcome.

Selected references

• G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, AMS, 2009, Chapter 7. https://doi.org/10.1090/gsm/099
• M. Reed and B. Simon, Methods of Modern Mathematical Physics II: Fourier Analysis, Self-Adjointness, Academic Press, 1975, Sections IX.1 and IX.7.
• E. M. Stein and G. Weiss, Introduction to Fourier Analysis on Euclidean Spaces, Princeton University Press, 1971, Chapter I. https://doi.org/10.1515/9781400883899

Motivation

In spectral theory the resolvent of a self-adjoint operator $A$ is studied through scalar functions $F_\psi(z) = \langle \psi, (A - z)^{-1}\psi\rangle$, defined for non-real $z$. Each $F_\psi$ is holomorphic on the upper half plane and maps it into itself. The spectral theorem, in the form presented in G. Teschl's Mathematical Methods in Quantum Mechanics (AMS Graduate Studies in Mathematics 99, 2009), comes down to the converse: a function of this kind with the right growth is the Cauchy–Stieltjes transform of a finite measure on $\mathbb{R}$, and that measure is the spectral measure of $\psi$. In the other direction, the absolutely continuous, singularly continuous and pure point spectra of Schrödinger operators are identified by looking at the boundary values of $F_\psi$ on the real axis. This mission formalizes the appendix to Chapter 3 of Teschl's book (Section 3.4, The Herglotz theorem, pp. 106–110) and Theorem 3.10, the measure-theoretic layer that the rest of the book's spectral analysis stands on.

The representation goes back to G. Herglotz (1911) for the disc and R. Nevanlinna (1922) for the half plane. The inversion formula is due to T. J. Stieltjes (1894). The link between boundary values and the Lebesgue decomposition of the measure is classical harmonic analysis on the half plane (Fatou, de la Vallée Poussin) and is the tool behind the spectral-type results of Gilbert–Pearson subordinacy theory and Aronszajn–Donoghue rank-one perturbation theory.

Setting

Write $\mathbb{C}_+ = \{z \in \mathbb{C} \mid \operatorname{Im}(z) > 0\}$. A Herglotz function is a holomorphic map $F$ on $\mathbb{C}_+$ with $\operatorname{Im} F(z) > 0$ for every $z \in \mathbb{C}_+$ (IsHerglotz).

For a Borel measure $\mu$ on $\mathbb{R}$, its Borel transform is

$$F(z) = \int_{\mathbb{R}} \frac{d\mu(\lambda)}{\lambda - z}$$

(borelTransform μ). The spectrum of $\mu$ is its set of growth points, $\sigma(\mu) = \{\lambda \mid \mu((\lambda-\varepsilon,\lambda+\varepsilon)) > 0 \text{ for all } \varepsilon > 0\}$ (measureSpectrum).

With $B_\varepsilon(x) = (x - \varepsilon, x + \varepsilon)$ and $|\cdot|$ Lebesgue measure, the upper and lower derivatives of $\mu$ are $(\overline{D}\mu)(x) = \limsup_{\varepsilon\downarrow0} \mu(B_\varepsilon(x))/|B_\varepsilon(x)|$ and $(\underline{D}\mu)(x) = \liminf_{\varepsilon\downarrow0} \mu(B_\varepsilon(x))/|B_\varepsilon(x)|$, values in $[0,\infty]$ (upperDeriv, lowerDeriv). The derivative $(D\mu)(x)$ is the limit when it exists, possibly $\infty$ (HasMeasureDeriv μ x d).

A set $A$ is a support of $\mu$ if $\mu(\mathbb{R}\setminus A) = 0$ (IsSupport). A support $M$ is a minimal support if every Borel $M_0 \subseteq M$ with $\mu(M_0) = 0$ is Lebesgue-null (IsMinimalSupport). The Lebesgue decomposition $d\mu = d\mu_{ac} + d\mu_s$ with respect to Lebesgue measure refines to $d\mu_s = d\mu_{sc} + d\mu_{pp}$, where $\mu_{pp}$ lives on the atoms of $\mu$. The absolutely continuous part $\mu_{ac}$ and the singularly continuous part $\mu_{sc}$ are acPart μ and scPart μ.

Formalization targets

Goal: Herglotz representation (Theorem 3.20)

If $F$ is a Herglotz function and $|F(z)| \le M/\operatorname{Im}(z)$ for all $z \in \mathbb{C}_+$, then there is a Borel measure $\mu$ on $\mathbb{R}$ with $\mu(\mathbb{R}) \le M$ and

$$F(z) = \int_{\mathbb{R}} \frac{d\mu(\lambda)}{\lambda - z}, \qquad z \in \mathbb{C}_+ .$$

Milestones

1. Theorem 3.10. For a finite Borel measure $\mu$, the transform is holomorphic on $\mathbb{C}\setminus\sigma(\mu)$, is a Herglotz function when $\mu \ne 0$, and satisfies $F(z^*) = F(z)^*$ and $|F(z)| \le \mu(\mathbb{R})/\operatorname{Im}(z)$ on $\mathbb{C}_+$.
2. Theorem 3.21. $\mu$ is determined by its transform on $\mathbb{C}_+$, and for $\lambda_1 < \lambda_2$

$$\tfrac12\bigl(\mu((\lambda_1,\lambda_2)) + \mu([\lambda_1,\lambda_2])\bigr) = \lim_{\varepsilon\downarrow0}\frac1\pi\int_{\lambda_1}^{\lambda_2}\operatorname{Im}F(\lambda+i\varepsilon)\,d\lambda .$$

3. Theorem 3.22. For every $\lambda$, $(\underline D\mu)(\lambda) \le \liminf_{\varepsilon\downarrow0}\frac1\pi\operatorname{Im}F(\lambda+i\varepsilon) \le \limsup_{\varepsilon\downarrow0}\frac1\pi\operatorname{Im}F(\lambda+i\varepsilon) \le (\overline D\mu)(\lambda)$.
4. Theorem 3.23. $\lim_{\varepsilon\downarrow0}\frac1\pi\operatorname{Im}F(\lambda+i\varepsilon)$ exists in $[0,\infty]$ for $\mu$-a.e. and Lebesgue-a.e. $\lambda$, equals $(D\mu)(\lambda)$ wherever the latter exists; the set where it is $\infty$ supports $\mu_{sc}$, and the set where it lies in $(0,\infty)$ is a minimal support of $\mu_{ac}$.
5. Corollary 3.24. If $\limsup_{\varepsilon\downarrow0}\operatorname{Im}F(\lambda+i\varepsilon) < \infty$ for all $\lambda$ in a Borel set $I$, then $\mu|_I$ is absolutely continuous.
6. Corollary 3.25. $\lim_{\varepsilon\downarrow0}F(\lambda+i\varepsilon)$ exists (finite or $\infty$) $\mu$-a.e. and Lebesgue-a.e., and is finite Lebesgue-a.e.

Significance

Theorem 3.20 together with Theorem 3.10 is a bijection between finite Borel measures on $\mathbb{R}$ and Herglotz functions of bounded growth $\operatorname{Im}(z)|F(z)|$. In Teschl's development it produces the spectral measures $\mu_\psi$ from the resolvent, and hence the projection-valued measure of an unbounded self-adjoint operator. Theorems 3.21–3.25 turn spectral questions into boundary-value questions. The later chapters on Sturm–Liouville operators and one-dimensional Schrödinger operators decide which spectral type an operator has by reading $\operatorname{Im} F(\lambda + i0)$ for the Weyl–Titchmarsh function.

These are textbook results with complete published proofs. Mathlib has the upper half plane as a type, Lebesgue decomposition, Radon–Nikodym derivatives and Vitali-family differentiation of measures, but it has no Borel (Cauchy–Stieltjes) transform of a measure on $\mathbb{R}$, no Herglotz representation on the half plane, and no Stieltjes inversion. The remaining work is to formalize the known proofs against Mathlib's measure theory and complex analysis. No machine-checked version of these statements is known to exist on Prove2Me.

Difficulty

For the goal, the measure has to be built: nothing in the hypothesis names it. A Herglotz function gives no measure directly, only a family of absolutely continuous approximations coming from the boundary values of $\operatorname{Im} F$ slightly above the real axis. The difficulty is to pass to a limit that is only a measure (it may have atoms and singular parts), and to identify the limit's transform with $F$ itself, not just its imaginary part. The uniform bound is what makes the limit exist and keeps its mass at most $M$. Without it the general Nevanlinna representation carries an extra linear term and a non-finite measure, and the statement here fails.

For the boundary-value theorems, the pointwise behaviour of the Poisson integral has to be compared with the symmetric derivatives of $\mu$ at each point, including points where $\mu$ is singular. The almost-everywhere statements for both $\mu$ and Lebesgue measure need the differentiation theory of measures in its singular form: the derivative is infinite $\mu_s$-almost everywhere, not only finite Lebesgue-almost everywhere.

Formalization scope

Measures are MeasureTheory.Measure ℝ on the Borel σ-algebra. Every theorem assumes IsFiniteMeasure μ, except the goal, whose conclusion μ Set.univ ≤ ENNReal.ofReal M makes μ finite. Functions on the half plane are ℂ → ℂ, constrained only on {z | 0 < z.im}. The Borel transform is a Bochner integral. Every claim evaluates it where the integrand is bounded, so Mathlib's convention that a non-integrable integral is $0$ never enters.

Limits as $\varepsilon \downarrow 0$ are taken along 𝓝[>] 0. The quantities that may be infinite (derivatives of measures, boundary values of $\operatorname{Im}F$) live in ℝ≥0∞, with $\operatorname{Im}F(\lambda+i\varepsilon)$, which is nonnegative for $\varepsilon > 0$, embedded by ENNReal.ofReal. An infinite limit of $F$ itself is Tendsto … (Bornology.cobounded ℂ). The lower and upper derivatives, the supports and the parts $\mu_{ac}$, $\mu_{sc}$ are defined in the mission's namespace exactly as in the book (Sec. A.8, Sec. 3.2).

Three readings of the printed text are fixed. Theorem 3.22 is stated for $\operatorname{Im}F(\lambda+i\varepsilon)$, which is what its proof estimates. Theorem 3.23's identity takes the factor $1/\pi$ once, consistent with Theorem 3.22. Theorem 3.10's Herglotz conclusion is stated for $\mu \ne 0$: the book's Herglotz functions map into the open half plane, and the zero measure's transform is identically zero.

A Herglotz function is defined analytically (holomorphic, positive imaginary part), never as "a Borel transform"; the latter would make the goal a tautology. No object is taken as data. The chunk uses no Hilbert space, no operator, and no projection-valued measure.

Useful infrastructure: UpperHalfPlane, Cauchy's integral formula on rectangles and semicircles, weak compactness of finite measures on $\mathbb{R}$ (Helly/Prokhorov), Mathlib's VitaliFamily.ae_tendsto_rnDeriv and Measure.singularPart. A reusable Poisson-kernel library for the half plane would be a welcome by-product, as would the vague-convergence lemmas of the book's Appendix A.

Selected references

• G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, American Mathematical Society, 2009, Sec. 3.2, Sec. 3.4 and Sec. A.8. https://doi.org/10.1090/gsm/099
• G. Herglotz, Über Potenzreihen mit positivem, reellen Teil im Einheitskreis, Berichte über die Verhandlungen der Königlich Sächsischen Gesellschaft der Wissenschaften zu Leipzig, Math.-Phys. Klasse 63 (1911), 501–511.
• R. Nevanlinna, Asymptotische Entwicklungen beschränkter Funktionen und das Stieltjessche Momentenproblem, Annales Academiae Scientiarum Fennicae A 18 (1922).
• T. J. Stieltjes, Recherches sur les fractions continues, Annales de la Faculté des Sciences de Toulouse 8 (1894), J1–J122. https://doi.org/10.5802/afst.108
• F. Gesztesy, E. Tsekanovskii, On matrix-valued Herglotz functions, Mathematische Nachrichten 218 (2000), 61–138. https://doi.org/10.1002/1522-2616(200010)218:1<61::AID-MANA61>3.0.CO;2-D

Motivation

Many operators of harmonic analysis are bounded on $L^2$ by an orthogonality argument but fail to be bounded on $L^1$; what survives at $p=1$ is a weak-type estimate $\lambda\,P(|Tf|>\lambda)\le c\,\|f\|_1$. For singular integrals the standard route to such an estimate is the Calderón–Zygmund decomposition, which splits a function at height $\lambda$ into a bounded part and a part supported on a small set. Martingale theory has the same need: square functions, martingale transforms and maximal operators of martingales are bounded on $L^2$ for orthogonality reasons, and their behaviour on $L^1$-bounded martingales is the delicate endpoint.

R. F. Gundy (1968) supplied the martingale analogue: an $L^1$-bounded martingale can be written as the sum of three martingales, one bounded in $L^2$, one whose differences are absolutely summable in $L^1$, and one that is non-zero only on an event of small probability (Gundy 1968). Gundy's construction used several stopping times. In his 1971 Wald Memorial Lectures, published as Distribution Function Inequalities for Martingales (Burkholder 1973), D. L. Burkholder gave a simplified version of the decomposition in which only one stopping time is used, with explicit constants $2$, $4$ and $1$. This mission formalizes that version, Theorem 4.1 of the lectures, together with the facts its proof rests on.

Timeline:

• 1953. J. L. Doob's Stochastic Processes establishes almost-everywhere convergence of $L^1$-bounded martingales and the maximal inequality.
• 1966. D. G. Austin proves that the integral of $S^2(f)$ over $\{f^*\le\lambda\}$ is finite for an $L^1$-bounded martingale (Austin 1966).
• 1968. Gundy proves the decomposition theorem for $L^1$-bounded martingales, with applications to weak-type estimates.
• 1973. Burkholder's Lemma 2.1, a refinement of Austin's theorem, yields a one-stopping-time proof of Gundy's decomposition with explicit constants.

Setting

Let $(\Omega,\mathcal A,P)$ be a probability space and $\mathcal A_0\subseteq\mathcal A_1\subseteq\cdots$ a nondecreasing sequence of sub-$\sigma$-fields of $\mathcal A$. A martingale relative to $\mathcal A_1,\mathcal A_2,\dots$ is a sequence $f=(f_1,f_2,\dots)$ of integrable random variables with $f_n$ $\mathcal A_n$-measurable and $E(f_{n+1}\mid\mathcal A_n)=f_n$. Its difference sequence is $d=(d_1,d_2,\dots)$ with $f_n=\sum_{k=1}^n d_k$, i.e. $d_1=f_1$, $d_k=f_k-f_{k-1}$ (the convention is $f_0=0$).

The maximal function is $f^*=\sup_{n\ge1}|f_n|$, the square function is $S(f)=\big[\sum_{k\ge1}d_k^2\big]^{1/2}$, and $S_n(f)$ is its $n$-th partial version. For $0<p<\infty$,

$$\|f\|_p=\sup_{n\ge1}\|f_n\|_p,\qquad \|f_n\|_p=(E|f_n|^p)^{1/p},$$

and $f$ is $L^p$-bounded when $\|f\|_p<\infty$. For $\lambda>0$, the exit time $\mu=\inf\{n\ge1:|f_n|>\lambda\}$ (with $\inf\emptyset=\infty$) is the first index at which $|f_n|$ exceeds $\lambda$; $f_\mu$, $f_{\mu-1}$, $S_{\mu-1}(f)$ denote evaluation at the random index, with $f_\infty=\lim_n f_n$.

The Lean development names these objects dseq ($d$), sqFnN/sqFn ($S_n(f)$, $S(f)$), maxFnN/maxFn ($f_n^*$, $f^*$), pNorm ($\|f\|_p$), exitTime ($\mu$) and valAt/sqFnAt (evaluation at an index in $\{0,1,\dots,\infty\}$), all in the namespace BurkholderDFI.Gundy.

Formalization targets

Goal: Theorem 4.1 (p. 23)

For every $L^1$-bounded martingale $f$ and every $\lambda>0$ there are martingales $X,Y,Z$ relative to the same $\sigma$-fields, with difference sequences $x,y,z$, such that

$$f=X+Y+Z,\qquad \|X\|_2^2\le2\lambda\|f\|_1,\qquad \Big\|\sum_{k=1}^\infty|y_k|\Big\|_1\le4\|f\|_1,\qquad P(Z^*>0)\le\|f\|_1/\lambda.$$

The three bounds hold together; each alone is trivial ($f=0+0+f$ satisfies the first two, $f=0+f+0$ the first and last).

Milestones

1. Doob's facts (cited, §1, p. 20). An $L^1$-bounded martingale or nonnegative submartingale converges almost everywhere, and $\|f_\mu\|_1\le\|f\|_1$ for every stopping time $\mu$.
2. (1.5) (p. 20). $\lambda^pP(f^*>\lambda)\le\|f\|_p^p$ for $1\le p<\infty$.
3. Lemma 2.1 (p. 21). For the exit time $\mu$ above $\lambda$,

$$\|S_{\mu-1}(f)\|_2^2+\|f_{\mu-1}\|_2^2\le2Ef_\mu f_{\mu-1}\le2\lambda\|f\|_1,$$

with equality on the left for martingales.

Significance

The result. The decomposition is the standard device for passing from $L^2$ to weak-type $(1,1)$ estimates for martingale operators: an operator that is bounded on $L^2$, controlled by total variation on the second piece, and local in the sense that it vanishes where the third piece vanishes, is of weak type $(1,1)$. Applications of the decomposition are given in Gundy's papers of 1968 and 1969 (On the class $L\log L$, martingales, and singular integrals, Studia Math. 33), which the lectures cite for this purpose. The explicit constants $2$, $4$, $1$ make every such weak-type constant explicit.

Formalizing it. The theorem is classical and proved; the remaining work is its formalization. As far as is known, no machine-checked proof of Gundy's decomposition, of Lemma 2.1, or of the weak-type maximal inequality in the form (1.5) for real martingales exists in Mathlib or on this platform. Mathlib provides almost-everywhere convergence of $L^1$-bounded submartingales and Doob's maximal inequality for nonnegative submartingales; the stopped-value bound for unbounded stopping times, the square-function identity of Lemma 2.1 and the decomposition itself are new. The milestones are shared with other missions of this series (Lemma 2.1 is also used for Burkholder's weak-type square function inequality and his exponential estimates), so each proof is reused.

Difficulty

The obvious attempt imitates the Calderón–Zygmund cut directly: truncate $f$ at height $\lambda$, or stop it when it first exceeds $\lambda$. Neither produces the required pieces. Truncation destroys the martingale property, and whatever restores it adds terms that must themselves be controlled in the right norm. Stopping at the exit time produces a martingale bounded by $\lambda$ only up to the overshoot at the exit, which is not bounded and lives on an event that is small only in probability. The $L^2$ estimate (4.2) is therefore not a consequence of boundedness; it needs a quantitative square-function bound for the martingale up to the exit, which is the content of Lemma 2.1, and that lemma in turn needs the limit $f_\infty$ and the stopped values $f_\mu$ on $\{\mu=\infty\}$ — so Doob's convergence theorem cannot be avoided.

Formalization scope

Processes are functions f : ℕ → Ω → ℝ with a Mathlib Filtration ℕ and Mathlib's Martingale/Submartingale. The paper indexes from $1$; Lean's index $0$ is never read by any quantity in the statements, which use the paper's convention $f_0=0$. Mathlib's martingale definition additionally constrains $f_0=E(f_1\mid\mathcal A_0)$; this is no restriction, since every martingale indexed from $1$ extends this way. The goal asserts that $X,Y,Z$ are Mathlib martingales for the same filtration as $f$, and the identity $f_n=X_n+Y_n+Z_n$ is required for $n\ge1$.

Further committed conventions:

• $S(f)$, $f^*$, $Z^*$, $\|\cdot\|_p$ and all expectations of nonnegative quantities take values in $[0,\infty]$ (lower Lebesgue integral), so no infinite value is silently replaced by $0$.
• $\|X\|_2=\sup_{n\ge1}\|X_n\|_2$, not the norm of a limit; $Z^*=\sup_{n\ge1}|Z_n|$; $\|\sum_k|y_k|\|_1$ is the integral of the series with $y_1=Y_1$.
• The exit time takes values in $\mathbb N\cup\{\infty\}$ and $\mu-1$ is truncated, with $\infty-1=\infty$; the a.e. limit $f_\infty$ is a function supplied with its convergence hypothesis (Lemma 2.1) or asserted to exist (Doob's facts).
• "Nonnegative submartingale" means $f_n\ge0$ almost surely for $n\ge1$.
• $\Omega$ is an arbitrary measurable space with a probability measure.

A formalization in which the existential could choose its own filtration, or in which the norms were Bochner integrals (which vanish on non-integrable functions), would trivialize the goal; both are excluded by the statement above.

Infrastructure needed: stopped values at unbounded stopping times and their $L^1$ bound; square-function identities for stopped martingales (orthogonality of martingale differences up to a stopping time); conditional-expectation compensators of predictable truncations. The definitions file is shared with the other eight missions of this series and is reusable for any work on discrete-time square and maximal functions. Proofs of the milestones, alternative arguments, and sharper constants are all welcome.

Selected references

• D. L. Burkholder, Distribution function inequalities for martingales, The Annals of Probability 1(1), 19–42, 1973. https://doi.org/10.1214/aop/1176997023
• R. F. Gundy, A decomposition for L¹-bounded martingales, The Annals of Mathematical Statistics 39(1), 134–138, 1968. https://doi.org/10.1214/aoms/1177698510
• D. G. Austin, A sample function property of martingales, The Annals of Mathematical Statistics 37(5), 1396–1397, 1966. https://doi.org/10.1214/aoms/1177699283
• J. L. Doob, Stochastic Processes, Wiley, New York, 1953.

Motivation

Poisson's equation $-\Delta u = f$ is the model elliptic partial differential equation. It describes the electrostatic potential of a charge density, the gravitational potential of a mass density, and the steady temperature of a body with internal heat sources. Its solution on the whole space by convolution with a point-source potential, and the fact that this solution has exactly two more derivatives than the data when smoothness is measured in Hölder norms, are the starting point of the regularity theory of second-order elliptic equations.

This mission formalizes §2.6–2.7 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis, revised 6/18/2014), which follow the classical line: the fundamental solution, the Newtonian potential, an integral representation of its second derivatives, and the Hölder estimate. The estimate goes back to J. Schauder (1934), who used it to build an existence theory for elliptic equations with Hölder continuous coefficients, now called Schauder theory (Gilbarg–Trudinger, Ch. 4 and 6). The singular integral operators that appear in the second derivatives were later placed in a general framework by A. P. Calderón and A. Zygmund (1952), whose theory gives the $L^p$ analogue.

Setting

Throughout, $n \ge 2$ and $\mathbb{R}^n$ carries the Euclidean norm $|x|$ and Lebesgue measure. Let $\alpha_n$ be the volume of the open unit ball. The fundamental solution of Laplace's equation is

$$\Gamma(x) = \frac{1}{n(n-2)\alpha_n}\,\frac{1}{|x|^{n-2}} \quad (n \ge 3), \qquad \Gamma(x) = -\frac{1}{2\pi}\log|x| \quad (n = 2),$$

defined for $x \neq 0$. With this sign convention (as in Evans, opposite to Gilbarg–Trudinger) $\Gamma$ is harmonic away from the origin and $-\Delta\Gamma = \delta$ in the sense of distributions. $\Gamma$ is locally integrable, and so is its gradient, but its second derivatives behave like $|x|^{-n}$ and are not.

For a smooth function $f$ with compact support, $f \in C_c^\infty(\mathbb{R}^n)$, the Newtonian potential of $f$ is the convolution

$$u(x) = (\Gamma * f)(x) = \int_{\mathbb{R}^n} \Gamma(x - y)\, f(y)\, dy.$$

Partial derivatives are written $\partial_i$, with $\partial_{ij} = \partial_i \partial_j$, and $\delta_{ij}$ is the Kronecker delta. For $0 < \alpha \le 1$ the Hölder seminorm of $v : \mathbb{R}^n \to \mathbb{R}$ is

$$[v]_{0,\alpha} = \sup_{x \neq y} \frac{|v(x) - v(y)|}{|x - y|^{\alpha}} \in [0, \infty].$$

In the Lean development these objects are fundamentalSolution n, unitBallVolume n, newtonianPotential n f, partialDeriv u i, secondPartial u i j and holderSeminorm α Set.univ v, all in the namespace HunterPDE.Newtonian.

Formalization targets

Goal: the Hölder estimate (Theorem 2.28)

For $0 < \alpha < 1$ there is a constant $C$, depending only on $\alpha$ and $n$, such that for every $f \in C_c^\infty(\mathbb{R}^n)$ and all indices $i, j$,

$$[\partial_{ij}(\Gamma * f)]_{0,\alpha} \le C\,[f]_{0,\alpha}.$$

The constant is not specified: the goal asserts the shape of the estimate, not a numerical value.

Milestones

1. Eq. (2.14). $\Gamma$ is $C^\infty$ on $\mathbb{R}^n \setminus \{0\}$ and $\partial_i\Gamma(x) = -\dfrac{1}{n\alpha_n}\dfrac{1}{|x|^{n-1}}\dfrac{x_i}{|x|}$ for $x \neq 0$.
2. Eq. (2.23). $\Gamma * (\Delta f) = -f$ for $f \in C_c^\infty(\mathbb{R}^n)$.
3. Theorem 2.25. $u = \Gamma * f$ is well defined, $u \in C^\infty(\mathbb{R}^n)$, and $-\Delta u = f$.
4. Corollary 2.27. For every $x$ and every open ball $B_R(x)$ containing the support of $f$,

$$\partial_{ij} u(x) = \int_{B_R(x)} \partial_{ij}\Gamma(x - y)\,[f(y) - f(x)]\,dy - \frac{1}{n} f(x)\,\delta_{ij},$$

with the integral absolutely convergent.

Significance

Theorem 2.25 is the existence theorem for Poisson's equation on the whole space. Corollary 2.27 expresses $D^2 u$ as a singular integral operator applied to $f$ plus a multiple of $f$; it is the prototype of the representations behind both the Hölder (Schauder) and the $L^p$ (Calderón–Zygmund) theories. Theorem 2.28 is the first Schauder estimate. With it, a priori estimates for equations with variable Hölder coefficients follow by freezing the coefficients, and existence follows by the method of continuity. The notes point out that the Hölder scale is essential: there are continuous compactly supported $f$ for which $\Gamma * f$ is not $C^2$, so no estimate of $D^2 u$ by the maximum of $|f|$ holds. The endpoint $\alpha = 1$ is excluded from the theorem.

All four statements are classical and proved in the notes; none is new mathematics. As far as the Prove2Me corpus and Mathlib show, none has been machine-checked. Mathlib has the Laplacian on inner product spaces, convolution, and the volume of Euclidean balls, but no fundamental solution of the Laplacian in general dimension, no Newtonian potential, and no Hölder estimates for it. A formalization would supply reusable infrastructure: the fundamental solution with its derivative formulas, differentiation under the integral sign with a locally integrable kernel, and estimates for kernels homogeneous of degree $-n$ with mean zero on spheres.

Difficulty

The obvious route to the second derivatives, differentiating twice under the integral sign, fails: $\partial_{ij}\Gamma$ is of order $|x|^{-n}$ near the origin and is not locally integrable, so $\int \partial_{ij}\Gamma(x-y) f(y)\,dy$ need not exist. Corollary 2.27 is precisely the statement that the correct formula carries a subtracted value $f(x)$ and a boundary contribution $-\frac1n f(x)\delta_{ij}$, and computing that contribution needs integrals over spheres, which Mathlib supports only indirectly. For the goal, a pointwise bound on the kernel is not enough. Estimating $|\partial_{ij}\Gamma(x-y)|\,|f(y)-f(x)|$ in absolute value gives a bound that grows with the radius of the ball containing the support of $f$, while the theorem's constant must be uniform over all $f$, all indices and all pairs of points. The estimate depends on cancellation in the kernel, and the maximum-norm version of the same statement is false.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) with volume. Every theorem assumes 2 ≤ n; the definition of $\Gamma$ returns junk values for $n = 0, 1$, which the book excludes.
• $\Gamma(0)$ is undefined in the book; in Lean it equals $0$ (from $1/0 = 0$ and $\log 0 = 0$), one point of measure zero.
• Coordinates are 0-based (i : Fin n). $\partial_i u(x)$ is fderiv ℝ u x (EuclideanSpace.single i 1), and $\partial_{ij} u = \partial_i(\partial_j u)$. fderiv is $0$ where $u$ is not differentiable, so $\partial_{ij}\Gamma(x-y)$ in Corollary 2.27 has an arbitrary value at the single point $y = x$.
• "Smooth" is ContDiff ℝ ∞ ($C^\infty$). In this Mathlib ContDiff ℝ ⊤ means analytic, and it is not used. Compact support is HasCompactSupport, and "the support of $f$" is the closed support tsupport f.
• $\Delta$ is Mathlib's InnerProductSpace.laplacian.
• The convolution $\Gamma * f$ is the Lebesgue integral $\int \Gamma(x-y) f(y)\,dy$, with no integrability assumed of $\Gamma$. Lean's Bochner integral is $0$ for a non-integrable integrand, so Theorem 2.25 asserts integrability of $y \mapsto \Gamma(x-y)f(y)$ for every $x$, and Corollary 2.27 asserts integrability of its integrand on the ball. Both are true and are implicit in the book's formulas; they rule out reading an identity between junk values as the theorem.
• The Hölder seminorm is a supremum in $[0,\infty]$ over all pairs of distinct points of $\mathbb{R}^n$, not Mathlib's HolderWith, which fixes a constant. In the goal $C$ is a finite nonnegative real quantified before $f$, $i$ and $j$. The inequality therefore also asserts that $\partial_{ij} u$ is uniformly $\alpha$-Hölder, because $[f]_{0,\alpha} < \infty$ for $f \in C_c^\infty$. A formalization that takes $C$ after $f$, lets it depend on the support of $f$, or includes the excluded endpoint $\alpha = 1$ is not the theorem.
• Theorem 2.26 of the notes (the same representation over an arbitrary smooth domain, with a surface integral over $\partial\Omega$) is not stated, because a faithful statement needs a surface measure on general smooth boundaries. The singular-integral discussion of §2.8 is commentary and is not stated.

Useful infrastructure, all reusable beyond this mission: differentiation of $\Gamma$ away from the origin; integration in polar coordinates and integrals of $|x|^{-a}$ over balls and annuli; surface integrals over spheres, or the divergence theorem on balls; differentiation under the integral sign for convolutions with a locally integrable kernel. Contributions of any of these as separate lemmas are welcome.

Selected references

• J. K. Hunter, Notes on Partial Differential Equations, UC Davis lecture notes, revised 6/18/2014, §2.6–2.8 and Definition 1.1. https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf
• L. C. Evans, Partial Differential Equations, 2nd ed., Graduate Studies in Mathematics 19, AMS, 2010, §2.2. https://doi.org/10.1090/gsm/019
• D. Gilbarg and N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Springer, 2001 (reprint of the 1998 ed.), Ch. 4. https://doi.org/10.1007/978-3-642-61798-0
• J. Schauder, Über lineare elliptische Differentialgleichungen zweiter Ordnung, Mathematische Zeitschrift 38 (1934), 257–282. https://doi.org/10.1007/BF01170635
• A. P. Calderón and A. Zygmund, On the existence of certain singular integrals, Acta Mathematica 88 (1952), 85–139. https://doi.org/10.1007/BF02392130