Theorem 2.28 — Hölder estimate [∂ᵢⱼu]_{0,α} ≤ C [f]_{0,α} for the Newtonian potential

Fix a natural number $n$ with $n \ge 2$, and a real number $\alpha$ with $0 < \alpha < 1$. Write $\mathbb{R}^n$ for the $n$-dimensional Euclidean space $\mathbb{R}^{\mathrm{Fin}\,n}$, with coordinates indexed by $\{0, 1, \dots, n-1\}$. The statement then asserts that there exists a single non-negative real constant $C \in [0, \infty)$, chosen once and for all before any function or index is fixed, with the following property.

For every function $f : \mathbb{R}^n \to \mathbb{R}$ that satisfies both

• $f$ is infinitely differentiable, i.e. $C^k$ for every finite $k$ (the smoothness class $C^\infty$, not real-analyticity), and
• $f$ has compact support, meaning the closure of $\{x : f(x) \ne 0\}$ is compact,

and for every pair of coordinate indices $i, j \in \{0, \dots, n-1\}$, the following inequality holds in the extended non-negative reals $[0, \infty]$:

The symbols are all defined in the bundle's own definition files, and their bodies are not part of the code shown here:

• $u_f$ is newtonianPotential n f, the bundle's "Newtonian potential" of $f$ in dimension $n$. It is a function $\mathbb{R}^n \to \mathbb{R}$.
• $\partial_{ij} u_f$ is secondPartial (newtonianPotential n f) i j, the bundle's "second partial derivative" of $u_f$ with respect to coordinates $i$ and $j$. It is again a real-valued function on $\mathbb{R}^n$.
• $[g]_{\alpha;\,S}$ is Shared.holderSeminorm α S g, the bundle's "Hölder seminorm" of exponent $\alpha$ for a function $g$ over a set $S$. It takes values in $[0, \infty]$, so it may equal $+\infty$. Here the set is always $S = \mathbb{R}^n$, the whole space.
• $C$ is used as an element of $[0, \infty]$ on the right-hand side. It is finite, but it is allowed to be $0$.

The code itself does not fix what these three functions mean. Whether $u_f$ is a convolution with a fundamental solution, what sign or normalisation it carries, and how $\partial_{ij}$ behaves at points where the function is not differentiable are all determined solely by the bundle definitions. The same goes for the exact supremum defining the seminorm, for example whether it is over pairs $x \ne y$ and whether it uses $|g(x) - g(y)| / |x - y|^\alpha$.

The quantifier order is $\exists C\ \forall f\ \forall i, j$. $C$ may depend on $n$ and $\alpha$ only, not on $f$, $i$ or $j$. No hypothesis ties $i$ to $j$, so the diagonal case $i = j$ is included.

Degenerate cases.

• Dimension. $n = 0$ and $n = 1$ are excluded by hypothesis. For $n \ge 2$ the index set is non-empty, so the claim over $i, j$ is not vacuous.
• Exponent. The endpoints $\alpha = 0$ and $\alpha = 1$ are excluded. The hypotheses on $n$ and $\alpha$ are jointly satisfiable, so the statement is not vacuous.
• The zero function. $f = 0$ is smooth and compactly supported, since its support is empty. For it, the inequality requires $[\partial_{ij} u_0]_{\alpha} \le C \cdot [0]_{\alpha}$, whatever value the bundle definitions assign to these quantities.
• Infinite seminorm of $f$. Arithmetic is in $[0, \infty]$. If $[f]_\alpha = \infty$ and $C > 0$, the right-hand side is $\infty$ and the inequality holds trivially. If $C = 0$, the convention $0 \cdot \infty = 0$ applies, so the right-hand side is $0$.
• Zero seminorm of $f$. If $[f]_\alpha = 0$, the right-hand side is $0$ for every $C$. The statement then forces $[\partial_{ij} u_f]_\alpha = 0$.
• Total-function defaults. Suppose the bundle defines $u_f$ via an integral that could fail to be integrable, or defines $\partial_{ij}$ via a derivative that could fail to exist. Then the inequality concerns whatever default value those definitions produce there. For example, integrals of non-integrable functions and derivatives at non-differentiable points evaluate to $0$ in Mathlib's conventions. Whether any such case arises for smooth compactly supported $f$ with $n \ge 2$ depends on definitions not shown here.