Analysis

Motivation

A holomorphic function on an open set of $\mathbb{C}^n$ restricts to a real hypersurface $M$ as a function that satisfies the tangential Cauchy–Riemann equations: it is annihilated by every antiholomorphic vector tangent to $M$. Functions on $M$ with this property are called CR functions, and they are the boundary values that several complex variables studies whenever a domain is approached through its boundary. The basic question is the converse: when is a CR function locally the restriction of a holomorphic function? For smooth data the answer is "not always" (the book's Example 3.2.7 gives a smooth CR function on the hyperplane $\operatorname{Im} z_2 = 0$ that is no such restriction). For real-analytic data the answer is "always", and that is Severi's theorem, the goal of this mission.

The mission follows Chapter 3 of Jiří Lebl's open textbook Tasty Bits of Several Complex Variables (version 4.4, 2026), where Severi's theorem is proved by complexification: a real-analytic function of $z$ and $\bar z$ is treated as a holomorphic function of two independent variables $(z, \zeta)$ restricted to the diagonal $\zeta = \bar z$. The milestones are the steps of that route: uniqueness on totally real slices, the two complexification propositions, the fact that restrictions of holomorphic functions are CR, and the normal form $\bar w = \Phi(z, \bar z, w)$ of a real-analytic hypersurface.

Setting

Write $\mathbb{C}^n \cong \mathbb{R}^{2n}$ with $z_k = x_k + i y_k$. A function on an open subset of $\mathbb{R}^N$ is real-analytic if near each point it equals a convergent power series in the real coordinates. A set $M \subset \mathbb{C}^n$ is a real-analytic hypersurface if near each of its points, after choosing one real coordinate $y$ among the $2n$ and collecting the other $2n-1$ as $x$, it is the graph $y = \varphi(x)$ of a real-analytic function $\varphi$.

A function $f$ on an arbitrary set $X \subset \mathbb{C}^n$ is smooth (respectively real-analytic) if near each point of $X$ it agrees on $X$ with a smooth (respectively real-analytic) function $F$ defined on an open neighbourhood. A defining function of $M$ at $p$ is a smooth real function $r$ on an open $V \ni p$ with nonvanishing derivative and $M \cap V = \{r = 0\}$; $M$ is a smooth real hypersurface if it has one at every point.

With the Wirtinger derivative $\partial/\partial\bar z_k = \tfrac12(\partial/\partial x_k + i\,\partial/\partial y_k)$, the space of antiholomorphic tangent vectors of $M$ at $p$ is

$$T^{(0,1)}_p M = \Big\{ \textstyle\sum_{k} a_k \frac{\partial}{\partial \bar z_k}\big|_p : \sum_k a_k \frac{\partial r}{\partial \bar z_k}(p) = 0 \Big\}.$$

A smooth $f : M \to \mathbb{C}$ is a CR function if $X_p f = 0$ for all $p \in M$ and $X_p \in T^{(0,1)}_pM$, where $X_p f$ is computed on any smooth local extension of $f$. A real-analytic CR function is a CR function that is real-analytic on $M$.

In Lean, $\mathbb{C}^n$ is Fin n → ℂ, and these notions are the definitions IsRealAnalyticOn, IsRealAnalyticHypersurface, IsSmoothHypersurface, IsSmoothOnSet / IsRealAnalyticOnSet, antiholTangent and IsSmoothCRFunction / IsRealAnalyticCRFunction of the namespace LeblSCV.CR.

Formalization targets

Goal: Severi's theorem (Theorem 3.2.9)

Let $M \subset \mathbb{C}^n$ be a real-analytic hypersurface, $p \in M$, and $f : M \to \mathbb{C}$ a real-analytic CR function. Then there are an open neighbourhood $U$ of $p$ and $F \in \mathcal{O}(U)$ with

$$F(q) = f(q) \qquad \text{for all } q \in M \cap U.$$

Milestones

1. Lemma 3.1.2. Holomorphic functions on a domain $V \subset \mathbb{C}^n$ that agree on $V \cap \mathbb{R}^n \neq \emptyset$ agree on $V$.
2. Proposition 3.1.3. A real-analytic function on a domain $U \subset \mathbb{R}^n$ extends to a unique holomorphic function on some domain $V \supset U$ of $\mathbb{C}^n$.
3. Lemma 3.1.4. Holomorphic functions on a domain $V \subset \mathbb{C}^n \times \mathbb{C}^n$ that agree on $V \cap \{\zeta = \bar z\} \neq \emptyset$ agree on $V$.
4. Proposition 3.1.5. A real-analytic $f$ on a domain $U \subset \mathbb{C}^n$ has a unique holomorphic $F$ on a domain $V \supset \{(z, \bar z) : z \in U\}$ with $F(z, \bar z) = f(z)$.
5. Proposition 3.2.6. The restriction of a holomorphic function to a smooth (respectively real-analytic) hypersurface is a smooth (respectively real-analytic) CR function.
6. Proposition 3.2.8. After a translation and a unitary rotation taking $p$ to $0$, a real-analytic hypersurface is locally $\bar w = \Phi(z, \bar z, w)$ with $\Phi$ holomorphic, $\Phi$, $\partial\Phi/\partial z_k$, $\partial\Phi/\partial\zeta_k$ vanishing at $0$, and $w = \bar\Phi(\zeta, z, \Phi(z, \zeta, w))$.

Significance

Severi's theorem identifies the real-analytic CR functions on a real-analytic hypersurface with the local traces of holomorphic functions. Together with Proposition 3.2.6 it shows that, in the real-analytic category, the tangential Cauchy–Riemann equations are exactly the obstruction to holomorphic extension. It is the model for the later extension theorems of the chapter: the Baouendi–Trèves approximation theorem (Theorem 3.3.1) and the Lewy extension theorem (Theorem 3.4.1), which replace real-analyticity with smoothness and pay for it with one-sided extension or approximation. Complexification (Propositions 3.1.3 and 3.1.5) is also a tool in its own right, used for the composition of real-analytic maps (Proposition 3.1.10) and for pluriharmonic functions.

All results here are classical and proved in the book; none of them is formalized in Lean or Mathlib as far as a search of the Prove2Me corpus and Mathlib shows. Mathlib has real and complex analyticity (AnalyticOnNhd), the one-variable and several-variable identity theorems for analytic functions, and the holomorphic implicit function theorem is within reach, but it has no notion of real hypersurface, CR vector or CR function. The mission produces that layer and a checked proof of the first extension theorem for CR functions.

Difficulty

The obvious idea is to take a real-analytic extension of $f$, complexify it to a holomorphic function $f(z, w, \zeta, \omega)$ of $2n$ variables, and substitute $\omega = \Phi(z, \zeta, w)$ to remove $\bar w$. That produces a holomorphic function of $(z, w, \zeta)$, not of $(z, w)$; showing that it does not depend on $\zeta$ requires transporting the CR equations, which hold only on $M$, to the whole complexified hypersurface. That transport is a uniqueness statement for the complexification, and it rests on the normal form of Proposition 3.2.8, itself an application of the holomorphic implicit function theorem to the complexified defining function together with its reality symmetry. On the Lean side, the diagonal $\{\zeta = \bar z\}$ is not a complex submanifold, so identity theorems along it (Lemmas 3.1.2 and 3.1.4) do not follow from the standard identity theorem for open sets.

Formalization scope

• $\mathbb{C}^n$ is Fin n → ℂ, with 0-based indices; $\mathbb{C}^n \times \mathbb{C}^n$ is the product type. The sup norm of Fin n → ℂ never enters a statement: no ball, norm or distance occurs.
• Holomorphic on an open set is DifferentiableOn ℂ, which is equivalent to the book's Definition 1.1.2 there. A domain is an open connected (hence nonempty) set.
• Real-analytic is Mathlib's AnalyticOnNhd ℝ on an open set, applied to $\mathbb{C}^n$ as a real vector space, which is the book's power series in $x, y$ (equivalently in $z, \bar z$).
• A real-analytic hypersurface is a local graph over one of the $2n$ real coordinates (Definition 3.1.9), not the zero set of a real-analytic function.
• Functions on $M$ are functions on $\mathbb{C}^n$ of which only the values on $M$ are read. "Smooth on $M$" means locally the restriction of a $C^\infty$ function (Definition 3.2.1). The CR condition is imposed for every defining function and every smooth local extension, which is equivalent to one choice because both are independent of the choice.
• Proposition 3.2.8 is stated for $n = m + 1$, with the unitary change of coordinates $q \mapsto U(q - p)$ and every "near the origin" made an explicit open set. Only its displayed statement is a target; the remarks that follow it on the page are not.
• The goal cannot be satisfied by an empty hypothesis: real-analytic hypersurfaces exist (a sorry-free check shows $\{\operatorname{Im} z_1 = 0\}$ qualifies), and by Proposition 3.2.6 every restriction of a holomorphic function is a real-analytic CR function. The CR condition is the intrinsic one on $T^{(0,1)}_pM$; replacing it with "restriction of a holomorphic function" would make the goal a tautology and is ruled out.
• Needed infrastructure: the several-variable identity theorem, holomorphic implicit functions, power series in $2n$ variables, and the chain rule for Wirtinger derivatives. The definitions of real-analytic hypersurface and CR function are reusable by the later extension theorems of Chapter 3. Contributions of any milestone, of a proof that $T^{(0,1)}_pM$ is independent of the defining function, or of Exercise 3.2.3 (independence of the extension) are welcome.

Selected references

• J. Lebl, Tasty Bits of Several Complex Variables, version 4.4, 2026, Chapter 3. https://www.jirka.org/scv/
• Mathlib documentation, Mathlib.Analysis.Analytic.Basic (analytic functions, AnalyticOnNhd). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Analytic/Basic.html

Motivation

The heat equation $u_t = \Delta u$ and the free Schrödinger equation $i u_t = -\Delta u$ are the two model evolution equations of linear PDE on $\mathbb{R}^n$. The first describes diffusion and is the prototype of every parabolic equation; the second describes a free quantum particle and is the prototype of dispersive wave equations. Both are solved explicitly by the Fourier transform and by convolution with a Gaussian-type kernel, and the estimates obtained from these formulas (smoothing, $L^2$ and $H^s$ energy bounds, $L^1 \to L^\infty$ decay) are the tools later used for nonlinear problems: semilinear heat equations, nonlinear Schrödinger equations, Galerkin constructions for general parabolic PDE, and Strichartz estimates.

This mission formalizes Chapter 5, §§5.1–5.3, of J. K. Hunter's Notes on Partial Differential Equations (UC Davis lecture notes, revised 6/18/2014, author's copy), which follows the presentation of Taylor's Partial Differential Equations (Taylor, vol. I, Ch. 3). The classical material goes back to Fourier (1822) for the heat kernel and to the analysis of dispersion for the Schrödinger group in the twentieth century; the goal and milestones are textbook results with complete proofs in the literature.

Setting

Write $\mathbb{R}^n$ for Euclidean space with Lebesgue measure, $|x|$ for the Euclidean norm and $\Delta = \sum_i \partial_i^2$ for the Laplacian. The heat kernel is

$$\Gamma(x,t) = \frac{1}{(4\pi t)^{n/2}}\, e^{-|x|^2/4t}, \qquad x \in \mathbb{R}^n,\ t > 0,$$

and for data $f$ the heat convolution is $u(x,t) = \int_{\mathbb{R}^n} \Gamma(x-y,t) f(y)\,dy$.

The Schwartz space $\mathcal S(\mathbb{R}^n)$ consists of smooth functions all of whose derivatives decay faster than every power of $|x|$, with the Fréchet topology of the seminorms $\sup |x^\alpha \partial^\beta f|$. A curve $u : I \to \mathcal S$ on a time interval $I$ has a strong derivative $v$ at $t$ if the difference quotients $(u(t+h)-u(t))/h$ converge to $v$ in $\mathcal S$; $C^k(I;\mathcal S)$ and $C^\infty(I;\mathcal S)$ are defined with continuous strong derivatives. A Schwartz solution of the heat problem with data $f \in \mathcal S$ is a curve $u \in C([0,\infty);\mathcal S) \cap C^1(0,\infty;\mathcal S)$ with $u(0) = f$ and $u_t(t) = \Delta u(t)$ for $t > 0$; a Schwartz solution of the Schrödinger problem is $u \in C^1(\mathbb{R};\mathcal S)$ with $u(0) = f$ and $i u_t = -\Delta u$ for all $t$.

The Fourier transform is used in the book's normalization,

$$\hat f(k) = \frac{1}{(2\pi)^n}\int_{\mathbb{R}^n} f(x)\, e^{-ik\cdot x}\,dx,$$

and, with $\langle k\rangle = (1+|k|^2)^{1/2}$, the Sobolev norm is $\|f\|_{H^s} = \big((2\pi)^n\int \langle k\rangle^{2s}|\hat f(k)|^2\,dk\big)^{1/2}$ for $s \in \mathbb{R}$.

Formalization targets

Goal: smoothing by the heat kernel (Theorem 5.5)

Let $1 \le p \le \infty$ and $f \in L^p(\mathbb{R}^n)$. Then the heat convolution converges absolutely for $t>0$, $u$ is $C^\infty$ on $\mathbb{R}^n \times (0,\infty)$, and

$$u_t = \Delta u \quad (t > 0).$$

If $p < \infty$, every derivative of $u$ tends to zero as $|x| \to \infty$ at each fixed $t > 0$, and

$$u(\cdot,t) \to f \ \text{ in } L^p \text{ as } t \to 0^+.$$

This is the chapter's statement that rough data are instantly smoothed while the initial condition is attained in the $L^p$ sense; it involves no Fourier transform.

Milestones

1. Eq. (5.9): $\Gamma$ is $C^\infty$ on $\mathbb{R}^n \times (0,\infty)$ and $\Gamma_t = \Delta\Gamma$.
2. Theorem 5.4: for $f \in \mathcal S$ the heat problem has a unique Schwartz solution; it lies in $C^\infty([0,\infty);\mathcal S)$, satisfies $\hat u(k,t) = \hat f(k) e^{-t|k|^2}$, and equals the heat convolution for $t > 0$.
3. Theorem 5.8: $\|u(t)\|_{L^2} \le \|f\|_{L^2}$ and $\|u(t)\|_{L^\infty} \le (4\pi t)^{-n/2}\|f\|_{L^1}$.
4. Theorem 5.9: $\|u(t)\|_{H^s} \le \|f\|_{H^s}$ for all $s \in \mathbb{R}$, $t \ge 0$.
5. Theorem 5.10: on $[0,T]$, $\max_t \|u(t)\|_{H^s} \le \|f\|_{H^s}$ and $\|Du\|_{L^2([0,T];H^s)} \le \tfrac{1}{\sqrt 2}\|f\|_{H^s}$.
6. Theorem 5.15: for $f \in \mathcal S$ the Schrödinger problem has a unique solution in $C^\infty(\mathbb{R};\mathcal S)$, with $\hat u(k,t) = e^{-it|k|^2}\hat f(k)$ and $u(\cdot,t) = \Gamma_S(\cdot,t) * f$ for $t \ne 0$, $\Gamma_S(x,t) = (4\pi i t)^{-n/2} e^{i|x|^2/4t}$.
7. Theorem 5.16: $\|u(t)\|_{L^2} \le \|f\|_{L^2}$, $\|u(t)\|_{L^\infty} \le (4\pi|t|)^{-n/2}\|f\|_{L^1}$ and, for $2<p<\infty$, $\|u(t)\|_{L^p} \le (4\pi|t|)^{-n(1/2-1/p)}\|f\|_{L^{p'}}$.
8. Theorem 5.17: $\|u(t)\|_{H^s} = \|f\|_{H^s}$ for all $s$ and $t$.

A further item, not a milestone, records that $\int \Gamma(x,t)\,dx = 1$ for $t > 0$ (p. 131).

Significance

The result itself. Theorem 5.5 is the statement that the heat semigroup maps $L^p$ into smooth functions decaying with all derivatives, and that it is strongly continuous on $L^p$ for $p < \infty$. It is used whenever a parabolic problem with rough data is solved by the Duhamel formula, in particular for the semilinear heat equation in the next part of the chapter. Theorem 5.4 and the energy estimates 5.9–5.10 are the input for generalized $H^s$ solutions (Theorem 5.12) and for Galerkin existence for parabolic PDE in Chapter 6. The Schrödinger estimates 5.16–5.17 are the linear input of the local theory of nonlinear Schrödinger equations and of Strichartz estimates.

Formalizing it. All results are classical and fully proved on paper. Mathlib has Schwartz functions, its own Fourier transform on $\mathcal S$ with Plancherel, Gaussian integrals and Fourier transforms of Gaussians, convolution and approximate identities for compactly supported kernels, and the Laplacian on inner-product spaces. It does not have the heat kernel on $\mathbb{R}^n$ as a solution operator, the differentiation of Schwartz-valued curves, the $H^s$ energy estimates, or the dispersive estimates for the Schrödinger group. A platform development of the heat kernel exists only on $\mathbb{R}^3$ with a viscosity parameter (the Navier–Stokes mission), and the platform's Plancherel theorem is in Mathlib's normalization. The remaining work is to formalize the known proofs in the book's normalization and dimension.

Difficulty

For the goal, the obvious argument is "differentiate under the integral sign and apply the mollifier theorem". Both steps need care in Lean. Differentiation in $(x,t)$ requires domination of every derivative of $\Gamma$ uniformly on neighbourhoods of $(x,t)$, paired by Hölder's inequality with an arbitrary $f \in L^p$. The approximation-of-identity result in Mathlib and in the book (Theorem 1.28) is stated for compactly supported mollifiers, whereas $\Gamma(\cdot,t)$ has full support, so the $L^p$ convergence needs the Gaussian version with a tail estimate. The decay of all derivatives as $|x| \to \infty$ relies on $p < \infty$. For the Schwartz-space results the difficulty is the calculus of $\mathcal S$-valued curves: strong differentiability is convergence of difference quotients in every Schwartz seminorm, and uniqueness requires passing from the strong equation to the pointwise ODE for $\hat u(k,t)$. The $L^{p'} \to L^p$ bound (5.16) rests on Riesz–Thorin interpolation, which Mathlib does not have.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) with volume; coordinates are 0-based (i : Fin n). $\Delta$ is Mathlib's Laplacian: on functions for the goal and (5.9), and $\Delta : \mathcal S \to \mathcal S$ for the Schwartz solutions. Smoothness is ContDiff/ContDiffOn ℝ ∞.
• $\mathcal S$ is Mathlib's SchwartzMap with its Fréchet topology, the same as the book's. Real-valued for the heat equation, complex-valued for Schrödinger. Strong derivatives, $C^\infty(I;\mathcal S)$ and the two solution predicates are defined in HunterPDE.HeatFourier.SchwartzCurve. Uniqueness in Theorem 5.4 is agreement for $t \ge 0$.
• The Fourier transform is the book's $(2\pi)^{-n}\int f e^{-ik\cdot x}$, defined explicitly; Mathlib's 𝓕 is not used. The $H^s$ norm is $[0,\infty]$-valued and is the norm of the book's $H^s$ inner product, $\big((2\pi)^n\int\langle k\rangle^{2s}|\hat f|^2\big)^{1/2}$; the norm formula printed with Definition 5.74 places $(2\pi)^n$ outside the square root, which differs by the constant $(2\pi)^{n/2}$ and does not affect any statement here, since every $H^s$ inequality and identity has an $H^s$ norm on both sides. $L^p$ norms are eLpNorm in $[0,\infty]$, and the factors $1/(4\pi|t|)^{\dots}$ in Theorem 5.16 are divisions in $[0,\infty]$, so $t = 0$ gives the trivial bound $\infty$.
• Corrections of the page. (i) The book states $u \in C_0^\infty(\mathbb{R}^n \times (0,\infty))$ in Theorem 5.5 for every $p \le \infty$. For $p = \infty$ this fails ($f \equiv 1$), so the decay of derivatives is stated for $p < \infty$, which is the case its proof covers. "$C_0^\infty$" is read as the proof explains it: every derivative tends to zero as $|x| \to \infty$ at fixed $t > 0$. (ii) The Schrödinger kernel is printed as $(4\pi i t)^{-n/2}e^{-i|x|^2/4t}$. The sign of the exponent contradicts the book's (5.15), so the corrected $e^{+i|x|^2/4t}$ is used, with the principal-branch power.
• Theorems 5.9 and 5.10 assume the solution property of Theorem 5.4 rather than $C^\infty$ regularity in time. By Theorem 5.4 this is the same solution. The absolute convergence of (5.5) is part of the goal's conclusion.
• Ruling out trivializations. The goal is not the statement "$u$ is smooth": the heat equation, the decay of every derivative and the $L^p$ convergence are all required. No hypothesis restricts $f$ beyond $f \in L^p$. The solution predicates are satisfiable (the zero curve solves the problem with zero data), and existence in Theorems 5.4 and 5.15 is asserted, not assumed.
• Not included: generalized $H^s$ solutions (Definition 5.11, Theorem 5.12), the heat $L^{p'}\to L^p$ bound (5.10), and the Fourier-transform background of Appendix 5.B (Theorems 5.66–5.73). Contributions welcome: a Gaussian approximate-identity theorem in $L^p$, the $\mathcal S$-valued calculus of Proposition 5.3, and a conversion lemma between the book's and Mathlib's Fourier normalizations. All three are reusable across this series (semigroups, the semilinear heat equation, NLS).

Selected references

• J. K. Hunter, Notes on Partial Differential Equations, UC Davis lecture notes, revised 6/18/2014, Chapter 5. https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf
• M. E. Taylor, Partial Differential Equations I: Basic Theory, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-1-4419-7055-8
• L. C. Evans, Partial Differential Equations, 2nd ed., AMS Graduate Studies in Mathematics 19, 2010, §2.3 and §4.3. https://doi.org/10.1090/gsm/019
• T. Cazenave, Semilinear Schrödinger Equations, Courant Lecture Notes 10, AMS, 2003, Ch. 2. https://doi.org/10.1090/cln/010

Motivation

Several equations of mathematical physics are written down formally but have no classical meaning as stated. The dynamical $\Phi^4_3$ model $\partial_t u = \Delta u - u^3 + \xi$ on the three-dimensional torus, the KPZ equation $\partial_t h = \partial_x^2 h + (\partial_x h)^2 - \infty + \xi$, and the parabolic Anderson model $\partial_t u = \Delta u + u\,\xi$ all require multiplying a distribution of negative regularity by itself, an operation that Schwartz distribution theory does not provide. Martin Hairer's A theory of regularity structures (Invent. Math. 198 (2014) 269–504, arXiv:1303.5113) develops a calculus in which such products, and the resulting fixed-point problems, become well posed.

The line of work leading to it is short and well documented: rough path theory (Lyons, 1998) solved the analogous problem for controlled ordinary differential equations driven by irregular signals; Gubinelli's controlled paths (2004) and branched rough paths (2010) reorganised it around local expansions; Hairer's theory extends that idea from paths to fields on $\mathbb{R}^d$ with anisotropic (e.g. parabolic) scaling. Paracontrolled distributions (Gubinelli–Imkeller–Perkowski, 2015) give an alternative route to some of the same equations. The algebraic and probabilistic infrastructure around regularity structures has since been systematised (Bruned–Hairer–Zambotti, 2019; Chandra–Hairer, 2016), but the analytic core is still the 2014 paper.

Setting

Fix a dimension $d$ and a scaling $s = (s_1,\dots,s_d)$ of positive integers, with $|s| = \sum_i s_i$, and put $\|x\|_s = \max_i |x_i|^{1/s_i}$. For $\delta > 0$, a point $x \in \mathbb{R}^d$ and a test function $\varphi$, the rescaled test function is

$$(S^{\delta}_{s,x}\varphi)(y) = \delta^{-|s|}\,\varphi\!\left(\frac{y_1-x_1}{\delta^{s_1}},\dots,\frac{y_d-x_d}{\delta^{s_d}}\right).$$

Write $\mathcal{B}^r_{s,0}$ for the set of test functions supported in $\{\|y\|_s \le 1\}$ whose derivatives up to order $r$ are bounded by $1$. For $\alpha<0$, a distribution $\xi$ belongs to the Hölder–Besov space $\mathcal{C}^\alpha_s$ if, on every compact set $K$, $|\langle \xi, S^{\delta}_{s,x}\eta\rangle| \le C\delta^{\alpha}$ uniformly over $x\in K$, $\delta \in (0,1]$ and $\eta \in \mathcal{B}^r_{s,0}$ with $r=-\lfloor\alpha\rfloor$.

A regularity structure $(A,T,G)$ consists of an index set $A \subseteq \mathbb{R}$ containing $0$, bounded below and locally finite; a graded vector space $T = \bigoplus_{\alpha\in A} T_\alpha$ with $T_0 \cong \mathbb{R}$ spanned by a unit $\mathbf{1}$; and a group $G$ of linear operators on $T$ with $\Gamma a - a \in \bigoplus_{\beta<\alpha}T_\beta$ for $a \in T_\alpha$, and $\Gamma\mathbf{1} = \mathbf{1}$. Elements of $T_\alpha$ are "homogeneous of order $\alpha$": they are placeholders for objects whose size at scale $\varepsilon$ is $\varepsilon^{\alpha}$.

A model $(\Pi,\Gamma)$ assigns to each point $x$ a linear map $\Pi_x : T \to \mathcal{D}'(\mathbb{R}^d)$ and to each pair $(x,y)$ an element $\Gamma_{xy}\in G$, subject to $\Gamma_{xx}=\mathrm{id}$, $\Gamma_{xy}\Gamma_{yz}=\Gamma_{xz}$, $\Pi_y = \Pi_x\circ\Gamma_{xy}$ and, locally uniformly, the analytic bounds

$$|(\Pi_x a)(S^{\delta}_{s,x}\varphi)| \lesssim \|a\|_\ell\,\delta^{\ell}, \qquad \|\Gamma_{xy}a\|_m \lesssim \|a\|_\ell\,\|x-y\|_s^{\ell-m}, \qquad a \in T_\ell,\; m<\ell.$$

A modelled distribution of order $\gamma$ is a function $f : \mathbb{R}^d \to T_{<\gamma}$ such that on every compact $K$

$$|||f|||_{\gamma;K} = \sup_{x\in K,\ \beta<\gamma}\|f(x)\|_\beta + \sup_{\substack{x,y \in K,\ \|x-y\|_s\le 1 \\ \beta<\gamma}} \frac{\|f(x)-\Gamma_{xy}f(y)\|_\beta}{\|x-y\|_s^{\gamma-\beta}} < \infty;$$

the space of these is $\mathcal{D}^\gamma$, and $\mathcal{D}^\gamma(V)$ if $f$ takes values in a sector $V$, that is, a graded $G$-invariant subspace vanishing in degrees below its regularity.

Formalization targets

Goal — reconstruction theorem, Theorem 3.10 for $\gamma>0$

With $\alpha = \min A < 0$ and $r$ the order attached to $A$, for every $f \in \mathcal{D}^\gamma$ with $\gamma>0$ there is a unique distribution $\mathcal{R}f \in \mathcal{C}^\alpha_s$ with

$$\big|(\mathcal{R}f - \Pi_x f(x))(S^{\delta}_{s,x}\eta)\big| \lesssim \delta^{\gamma} \qquad (x \in K,\ \delta\in(0,1],\ \eta\in\mathcal{B}^r_{s,0}).$$

The statement asserts only the shape of the estimate — a constant per compact set — and so is insensitive to any later sharpening of constants.

Milestone level — the calculus around the reconstruction operator

The uniqueness clause of Theorem 3.10 in isolation; the existence of a linear reconstruction operator for arbitrary $\gamma \in \mathbb{R}$ (for $\gamma\le 0$ the bound no longer pins it down); Corollary 3.16, improving the regularity of $\mathcal{R}f$ to $\mathcal{C}^\beta_s$ when $f$ takes values in a sector of regularity $\beta$; Proposition 3.31, that for $\nu>0$ the action of $\Pi$ on $T_\nu$ is determined by $\Gamma$ and by $\Pi$ in lower homogeneities; and Theorem 4.7, that the truncated pointwise product of $f_1 \in \mathcal{D}^{\gamma_1}(V)$ and $f_2\in\mathcal{D}^{\gamma_2}(W)$ lies in $\mathcal{D}^{\gamma}$ with $\gamma = (\gamma_1+\alpha_2)\wedge(\gamma_2+\alpha_1)$.

Significance

The reconstruction theorem is what turns a book-keeping device into analysis: it says that a coherent family of local expansions, indexed by base point, glues to a single genuine distribution, with an error controlled by the order of the expansion. Every subsequent operation in the theory — multiplication (Theorem 4.7), composition with smooth functions (Theorem 4.16), the multi-level Schauder estimate (Theorem 5.12), and the fixed-point theorem for singular SPDEs (Theorem 7.8) — is stated and used through it. Without it, the abstract spaces $\mathcal{D}^\gamma$ carry no information about actual distributions.

Regularity structures are not currently available in Mathlib, and neither are the anisotropic Hölder–Besov spaces $\mathcal{C}^\alpha_s$ that the theory is phrased in. The result itself is proved in the literature; the work this mission asks for is a machine-checked proof of the known argument, together with the reusable definitions it needs. The formal development is a prerequisite for anything downstream — Schauder estimates, the fixed-point theory, or the $\Phi^4_3$ and PAM convergence results of §10 — which are natural follow-on missions rather than part of this one.

Difficulty

The naive construction fails: setting $\mathcal{R}f := \Pi_x f(x)$ for a fixed $x$ is wrong away from $x$, and the pointwise limit $\lim_{\delta\to0}$ of localisations of $\Pi_x f(x)$ around each $x$ does not obviously exist, because the objects being glued are distributions of negative order, not functions, so there is no value to take and no partition-of-unity argument that respects the scaling. Hairer's proof goes through a wavelet multiresolution analysis adapted to the scaling $s$: one defines the candidate on each dyadic level by pairing with wavelets centred at grid points, and shows the resulting sequence is Cauchy using the $\mathcal{D}^\gamma$ bound level by level. A formalization therefore needs either a scaled wavelet basis with Daubechies-type regularity (Theorem 3.17 in the paper) or a substitute for it; this, and the uniform-in-scale bookkeeping, is where the effort lies. Uniqueness for $\gamma>0$ is by contrast short, and is listed as a separate milestone.

Formalization scope

The development commits to the following conventions, fixed in the mission's definition files. Points of $\mathbb{R}^d$ are Fin d → ℝ. Test functions are smooth and compactly supported, forming a submodule of all real-valued functions, and a distribution is a linear functional on that submodule; the pairing is extended by $0$ to non-test functions, and a lemma in the definition file certifies that rescaling maps test functions to test functions, so no statement is vacuous for that reason. Hairer's $\mathcal{B}^r_{s,0}$ consists of $C^r$ functions; here it consists of smooth ones, which defines the same spaces $\mathcal{C}^\alpha_s$. The model space is the algebraic direct sum $\bigoplus_{a\in A} T_a$ over the index set, each $T_a$ a real normed space, with $Q_a$ the corresponding projection; the structure group is a subgroup of the linear automorphisms of that direct sum. Sectors are families of subspaces $V_a \subseteq T_a$; Hairer's requirement that each $V_a$ admit a complement is automatic in this algebraic setting. The integer $r$ appearing in the model bounds is the smallest one with $\ell > -r$ for all $\ell \in A$, which is part of the definition of a model rather than a free parameter. All statements quantify over an arbitrary regularity structure, an arbitrary model, and an arbitrary compact set, so they are not satisfiable by a degenerate choice; the goal in particular claims existence, membership in $\mathcal{C}^\alpha_s$, and uniqueness simultaneously.

Infrastructure that a complete proof will need, and which is reusable beyond this mission: scaled wavelet bases on $\mathbb{R}^d$, the elementary theory of $\mathcal{C}^\alpha_s$ (including the positive-regularity case), and basic operations on compactly supported test functions under anisotropic rescaling. Contributions of any of these as separate lemmas are welcome, as are reductions that decompose the goal into wavelet-level estimates.

Selected references

• M. Hairer, A theory of regularity structures, Inventiones Mathematicae 198 (2014) 269–504. arXiv:1303.5113, DOI:10.1007/s00222-014-0505-4
• T. Lyons, Differential equations driven by rough signals, Revista Matemática Iberoamericana 14 (1998) 215–310. DOI:10.4171/RMI/240
• M. Gubinelli, Controlling rough paths, Journal of Functional Analysis 216 (2004) 86–140. arXiv:math/0306433
• M. Gubinelli, P. Imkeller, N. Perkowski, Paracontrolled distributions and singular PDEs, Forum of Mathematics Pi 3 (2015) e6. arXiv:1210.2684
• Y. Bruned, M. Hairer, L. Zambotti, Algebraic renormalisation of regularity structures, Inventiones Mathematicae 215 (2019) 1039–1156. arXiv:1610.08468

Motivation

Time-series momentum is the empirical regularity that an asset's recent excess return predicts its future excess return. It has been documented across equity indices, currencies, commodities and bonds (Moskowitz, Ooi & Pedersen 2012), and momentum portfolios are among the most widely traded systematic strategies. Most of that literature builds portfolios from a single signal: the average return over a look-back window. Li and Liu (Operations Research 2022) ask what a long-horizon investor who rebalances should do when expected returns really are driven by such a moving average. Their answer has a structural feature that a Markovian model such as Merton's (Merton 1971) cannot produce. The optimal weight depends on the whole recent price path, not only on the current momentum.

Setting

A risky asset has price $S_t$ and log price $s_t=\ln S_t$, with

$$\frac{dS_t}{S_t} = [\alpha m_t + (1-\alpha)\mu + r]\,dt + \sigma\,dB_t,\qquad m_t = \frac1\tau\int_{t-\tau}^{t}\Big(\frac{dS_u}{S_u} - r\,du\Big),$$

where $B$ is a Brownian motion. Momentum $m_t$ is the equally weighted moving average of excess returns over a look-back window of length $\tau>0$. The parameter $0<\alpha<1$ measures how strongly momentum enters the expected return, $\mu$ is the unconditional risk premium, $r$ is the constant short rate and $\sigma>0$ is the volatility. Because the drift depends on $s_t - s_{t-\tau}$, the price is not Markov: the state at time $t$ is the whole path on $[t-\tau,t]$.

An investor with constant relative risk aversion $\gamma>0$ maximizes expected utility of terminal wealth at a horizon $T$ by trading the asset and a riskless bond. The mission works in the paper's short-horizon regime $0\le T\le\tau$, with the investor standing at time $0$, so the realized path $s$ on $[-\tau,0]$ is known.

The paper's analysis (Appendix A.2) produces the following objects:

• the market price of risk at time $0$, $\theta_0 = [(1-\alpha)\mu - \alpha(r-\sigma^2/2) + \frac\alpha\tau(s_0-s_{-\tau})]/\sigma$;
• functions $A_1, A_2$ on $[0,T]$ that solve a Riccati equation and a linear equation, the system (A.9), with $A_1(T)=A_2(T)=0$ and forcing term $s_{u-\tau}$;
• the optimal weight $\phi^*_0 = \theta_0/(\gamma\sigma) + A_{1,0}s_0 + A_{2,0}$ of (A.11);
• explicit functions $C_0$, $\hat\omega$, the weight $\omega$ on $[-\tau,0]$ and a constant $C_1$, all of (A.14).

The Lean development names them theta0, SolvesA9, phiStar, C0, omegaHat, omega and C1 in the namespace DynMomentum.ShortHorizon.

Formalization targets

Goal: Proposition 3.3

For every solution $(A_1,A_2)$ of (A.9),

$$\phi^*_0 = \underbrace{\frac{\alpha}{\gamma\sigma^2}\int_{-\tau}^{0}\frac1\tau\Big(\frac{dS_v}{S_v}-r\,dv\Big) + \frac{(1-\alpha)\mu}{\gamma\sigma^2}}_{\phi^M_0} + \underbrace{\frac{(1-\gamma)\alpha}{\gamma\sigma^2}\int_{-\tau}^{0}\omega_v\Big(\frac{dS_v}{S_v}-r\,dv\Big) + C_1}_{\phi^H_0}. \tag{3.8}$$

Moreover, $\omega$ is positive on $(-\tau,0]$ when $T>0$, strictly increasing on $[-\tau,T-\tau]$, and constant on $[T-\tau,0]$. The first summand $\phi^M$ is the myopic mean-variance weight; the second, $\phi^H$, is the hedging demand.

Milestones

1. (A.9) solves (A.8). The ansatz $f(x,t)=\exp\{A_{1,t}x^2/2+A_{2,t}x+A_{3,t}\}$ solves the Feynman–Kac PDE (A.8) whenever $(A_1,A_2,A_3)$ solve (A.9).
2. (A.13), $A_1$. The closed form $A_{1,t}=\alpha(\gamma-1)(1-e^{2\alpha(T-t)/(\sqrt\gamma\tau)})/(\gamma\sigma^2\tau D(T,t))$ solves the Riccati equation with $A_{1,T}=0$.
3. (A.13), $A_2$. For any solution $A_1$, the variation-of-constants integral for $A_2$ solves the linear equation with $A_{2,T}=0$.
4. (A.14). $\hat\omega_u>0$ for $u\in[-\tau,-\tau+T]$.
5. Proposition 3.3, last sentence. The positivity and shape of $\omega$, stated on its own.

Significance

The result. Proposition 3.3 shows that a momentum investor who rebalances should not trade on momentum alone. The hedging demand weights past returns unequally, with more weight on recent ones, so two price paths with identical momentum lead to different optimal positions. This is the paper's explanation of why path dependence is intrinsic to optimal momentum trading. It underlies the paper's later comparisons with momentum-only strategies, the horizon extension of Proposition 6.3, and the closed-form expansions of Online Appendix III.

Formalizing it. The proof's analytic half, from (A.9) to (3.8), is summarized in the paper by the phrase "after some manipulations". Writing that step out yields a checked identity between an ODE-defined weight and an explicit integral formula. Doing so has already caught an error. The constant $C_1$ printed in (A.14) is wrong: it differs from the true value by a path-independent amount, and it becomes correct after deleting both occurrences of $-\sigma^2/2$ (a numerical solution of (A.9) agrees with the corrected formula to $10^{-10}$). The proposition is proved in the paper. As far as is known, no part of it has been machine-checked.

Difficulty

Each milestone is a direct calculus statement; the goal is not. The obvious approach is to substitute the closed forms (A.13) into (A.11) and simplify. That leaves $A_{2,0}$ as a double integral of the past path $s$ against two nested exponential kernels written in the ODE's own parameterization, while (3.8) is a single integral of returns $dS/S$ against the weight $\omega$ of (A.14), which is written in a different parameterization. The paper gives no derivation of the match. The path is only continuous, so no step may differentiate $s$. Separately, the Riccati closed form divides by a quantity that vanishes for small $\gamma<1$, so every step has to track where that denominator is positive.

Formalization scope

• What is formalized. Everything from (A.9) to (3.8). The stochastic layer is not formalized: Lemmas 3.1–3.2 (martingale method), the measure change, the Feynman–Kac representation and the volatility matching (A.10)–(A.12) need stochastic integration, Itô's formula and martingale representation, which Mathlib does not have at this revision. Equation (A.11) is therefore taken as the definition of the optimal weight: $\phi^*_0 := \theta_0/(\gamma\sigma) + A_{1,0}s_0 + A_{2,0}$.
• Time. The statement is at $t=0$ with horizon $0\le T\le\tau$ and the path on $[-\tau,0]$, as in Appendix A.2. The model is time-homogeneous, so a general $t$ is a shift.
• ODEs. "Solves (A.9)" means a derivative within $[0,T]$ at every point of $[0,T]$, plus the terminal conditions. At $T=0$ the derivative clause is vacuous; that is the paper's zero-horizon case.
• Admissibility. The hypothesis $D(T,0)=(\sqrt\gamma-1)e^{2\alpha T/(\sqrt\gamma\tau)}+(\sqrt\gamma+1)>0$ is added. It holds automatically for $\gamma\ge1$. Without it, the Riccati solution blows up for small $\gamma<1$ and the goal would be vacuous.
• Pathwise returns. The return integral $\int_{-\tau}^0 w_v(dS_v/S_v - r\,dv)$, for a deterministic absolutely continuous weight $w$ with derivative $w'$, is read as $w_0s_0 - w_{-\tau}s_{-\tau} - \int_{-\tau}^0 w'_vs_v\,dv + (\sigma^2/2-r)\int_{-\tau}^0 w_v\,dv$. This is its value by Itô's formula and the product rule. With $w\equiv1/\tau$ it gives back $m_0$ of (2.3).
• Corrections. $C_1$ is the corrected constant described above. The positivity of $\omega$ is stated on $(-\tau,0]$ under $T>0$, because $\omega_{-\tau}=0$ and $\omega\equiv0$ when $T=0$.
• What a correct formalization rules out. The goal is not obtained by definition. $\phi^*$ is (A.11), never $\phi^M+\phi^H$. The functions $\omega$, $\hat\omega$, $C_0$ and $C_1$ are the explicit formulas of (A.14), never derived from the ODE solution. The goal quantifies over every solution of (A.9), not over the closed forms.
• Infrastructure. The development uses Mathlib's HasDerivWithinAt, interval integrals, Real.exp and Real.sqrt. Two lemmas are reusable well beyond this mission: the closed form of a constant-coefficient scalar Riccati equation, and variation of constants for a scalar linear ODE with merely continuous forcing. Contributions of those lemmas, of uniqueness for (A.9), and of the integration-by-parts step are welcome.

Selected references

• K. Li and J. Liu, Optimal Dynamic Momentum Strategies, Operations Research, 2022. https://doi.org/10.1287/opre.2021.2254
• R. C. Merton, Optimum consumption and portfolio rules in a continuous-time model, Journal of Economic Theory 3(4), 1971. https://doi.org/10.1016/0022-0531(71)90038-X
• T. J. Moskowitz, Y. H. Ooi and L. H. Pedersen, Time series momentum, Journal of Financial Economics 104(2), 2012. https://doi.org/10.1016/j.jfineco.2011.11.003

Motivation

In the rough Heston model of El Euch and Rosenbaum, the variance of an asset is driven by a fractional kernel with Hurst exponent $H<\tfrac12$, which matches the roughness observed in realized volatility. The model keeps one feature of the classical Heston model: the characteristic function of the log-price is explicit up to the solution of a deterministic equation, here a fractional Riccati equation

$$D^\alpha\psi=\lambda\psi^2+\mu\psi+\nu,\qquad \alpha=H+\tfrac12,$$

with complex coefficients $\lambda,\mu,\nu$ that depend on the Fourier variable (El Euch–Rosenbaum 2019). Pricing a vanilla option by Fourier inversion requires this solution for many complex parameters, and the equation has no closed form. The standard numerical method, the fractional Adams scheme, is slow because of the memory of the fractional derivative.

Callegaro, Grasselli and Pagès (arXiv:1805.12587v4) observe that with zero initial condition the solution is a fractional power series $\psi(t)=\sum_{k\ge0}a_kt^{k\alpha}$ whose coefficients obey an explicit convolution recursion. The series can be summed very fast, but only on its interval of convergence; beyond it they switch to a hybrid numerical scheme. Where the switch happens is governed by the convergence radius, and their Theorem 3.3 bounds it explicitly from below and, for parameters of equal sign, from above.

Setting

Fix $\alpha\in(0,2]$ and $\lambda,\mu,\nu\in\mathbb C$. Identifying the coefficients of the series in the Riccati equation yields the coefficient recursion $(A_{\lambda,\mu,\nu})$ (3.19)–(3.20):

$$a_0=0,\qquad a_1=\frac{\nu}{\Gamma(\alpha+1)},\qquad a_{k+1}=\big(\lambda\,a^{*2}_k+\mu\,a_k\big)\frac{\Gamma(\alpha k+1)}{\Gamma(\alpha k+\alpha+1)}\quad(k\ge1),$$

where $a^{*2}_k=\sum_{\ell=1}^{k-1}a_\ell a_{k-\ell}$ is the discrete convolution (so $a^{*2}_1=0$). Each $a_{k+1}$ depends on $a_1,\dots,a_k$ only, so the sequence is uniquely determined; in Lean it is coeff α lam mu nu : ℕ → ℂ.

The convergence radius of $\sum_ka_kt^{k\alpha}$ is given by Hadamard's formula (3.21):

$$R_{\psi_{\lambda,\mu,\nu}}=\liminf_k|a_k|^{-\frac1{\alpha k}}\in[0,+\infty],$$

in Lean radius α (coeff α lam mu nu). With $x_+=\max(x,0)$, $a\wedge b=\min(a,b)$ and the Beta function $B(a,b)=\Gamma(a)\Gamma(b)/\Gamma(a+b)$, the paper introduces the constants

$$c_\alpha=2^{2-(1-2\alpha)_+-2(\alpha-1)_+}\alpha^{\alpha-1}B(\alpha\wedge1,\alpha\wedge1),\qquad \widetilde B(\alpha)=B(\alpha,\alpha)-2^{1-2\alpha},$$ $$\tau_*=\frac{2^{\frac1\alpha-(\frac1\alpha-2)_+}\,\alpha}{\Big(|\mu|+\sqrt{|\mu|^2+c_\alpha\frac{|\lambda||\nu|}{\Gamma(\alpha)}}\Big)^{1/\alpha}},\qquad C_\alpha=\begin{cases}(3\cdot5^{\alpha-1})^{\frac1{2\alpha}}\sqrt\alpha,&\alpha\in(0,1],\\ \sqrt{2\alpha}/\widetilde B(\alpha),&\alpha\in(1,2].\end{cases}$$

Formalization targets

Goal: Theorem 3.3 (a)–(b)

For $0<\alpha\le2$:

1. for all $\lambda,\mu,\nu\in\mathbb C$ with $\lambda\nu\ne0$,

$$0<\tau_*\le R_{\psi_{\lambda,\mu,\nu}};$$

2. for real $\lambda,\nu>0,\ \mu\ge0$ (resp. $\lambda,\nu<0,\ \mu\le0$),

$$R_{\psi_{\lambda,\mu,\nu}}\le R_{\psi_{|\lambda|,0,|\nu|}}\le C_\alpha\Big(\frac{\Gamma(\alpha+1)}{\lambda\nu}\Big)^{\frac1{2\alpha}}.$$

Milestones

In attack order: the Riemann-sum Lemma A.1 (A.39); Kershaw's Gamma-ratio inequalities (A.41); the coefficient upper bounds $|a_k|\le C_*k^{\alpha-1}\rho_*^k$ of (B.49) for $\alpha\le1$ and (B.51) for $\alpha>1$; Proposition B.1 (a) (for $\mu=0$ the even coefficients vanish and $b_k=a^0_{2k-1}$ solves (B.50)) and (b) (comparison $a_k\ge a^0_k\ge0$); Theorem 3.3 (c) (sign symmetry $a^{(\lambda,\mu,\nu)}_k=(-1)^{k-1}a^{(\lambda,-\mu,\nu)}_k$); the lower-bound propagation $b_k\ge c^*\rho^{*k}k^{\alpha-1}$ of §B.1.2 ($\alpha\le1$); the Riemann-sum bound (B.52) with $\widetilde B(\alpha)>0$; and the lower-bound propagation of §B.2.2 ($\alpha>1$).

Significance

The lower bound $\tau_*$ is an explicit, parameter-dependent time up to which the series converges absolutely: on $[0,\tau_*)$ the Riccati solution, and with it the rough Heston characteristic function, can be evaluated by summing a series with no discretization error. The upper bound shows that for parameters of equal sign the radius is finite and of order $(\lambda\nu)^{-1/(2\alpha)}$, which is why the paper's hybrid scheme (series near $0$, a numerical scheme beyond) is needed for long maturities. The two bounds together fix the scale on which the hybrid scheme switches methods.

The result is proved in the paper (Appendix B). The proof has not been machine-checked. A formal development adds a checked convergence guarantee for a recursion used in option-pricing code, and its auxiliary results (Kershaw's inequality for the Gamma function, which the pinned Mathlib does not contain, and Riemann-sum bounds for symmetric monotone functions) are reusable outside this paper. The paper prints a strict inequality $R>\tau_*$; its proof gives $R\ge\tau_*$, which is what the goal asks. Upgrading to the strict inequality would be a sharpening beyond the paper.

Difficulty

The obvious approach is to bound $|a_k|$ by a geometric sequence $C\rho^k$ and propagate the bound by induction through the recursion. It fails: the convolution $\sum_{\ell=1}^{k-1}\rho^\ell\rho^{k-\ell}$ contributes a factor $k-1$ that the Gamma ratio $\Gamma(\alpha k+1)/\Gamma(\alpha k+\alpha+1)\approx(\alpha k)^{-\alpha}$ absorbs only when $\alpha\ge1$, and then with constants that are far from sharp. The propagated bound therefore needs a polynomial correction $k^{\alpha-1}$. That turns the convolution into a Riemann sum of $(x(1-x))^{\alpha-1}$, which is convex for $\alpha\le1$ and concave for $\alpha\ge1$, and controlling it takes a non-asymptotic Gamma-ratio inequality valid for every $k\ge1$ rather than Stirling asymptotics. For the upper bound on the radius, the coefficients must be bounded from below, which requires positivity, the vanishing of the even coefficients when $\mu=0$, and a separate comparison between the cases $\mu\ge0$, $\mu=0$ and $\mu\le0$.

Formalization scope

Everything is stated about the coefficient sequence and its Hadamard radius. The fractional derivative, the Riccati equation itself and the function $\psi$ do not appear, as in the paper, which identifies the coefficients formally. Conventions:

• Indexing. coeff α lam mu nu : ℕ → ℂ, with $a_0=0$; the convolution at index $j$ runs over $\ell\in\{1,\dots,j-1\}$ (Finset.Ico 1 j). Gamma factors are Real.Gamma of real arguments, cast to $\mathbb C$; for $\alpha>0$ every argument is at least $1$.
• Radius. radius α a = liminf_{k→∞} ‖a k‖₊^{-1/(α k)} in ℝ≥0∞, with $0^{-x}=+\infty$ for $x>0$, so vanishing coefficients (all even ones when $\mu=0$) do not lower the radius. Real bounds enter through ENNReal.ofReal.
• Beta function through Gamma, $B(a,b)=\Gamma(a)\Gamma(b)/\Gamma(a+b)$.
• Real parameters (Proposition B.1, Theorem 3.3 (b)–(c), the lower-bound propagations) are real numbers cast into $\mathbb C$; coefficient inequalities are stated on real parts.
• Hypotheses relative to the page: $0<\alpha\le2$ for the printed "$\alpha\in[0,2]$"; $\nu\ne0$ from the standing Assumption 3.1 ($\lambda\nu\ne0$); $|\mu|^2$ for the printed $\mu^2$ under the square roots; $\tau_*\le R$ in place of the printed $R>\tau_*$; $(-1)^{k-1}$ for the printed $(-1)^k$ in Theorem 3.3 (c); $\lambda\nu$ in the numerator of the §B.1.2 constant $\rho^*$. Lemma A.1 uses exactly its stated hypotheses; its printed "hence convex" claim does not follow from them and is not needed for its inequalities.

A trivializing formalization is excluded: the radius is Hadamard's $\liminf$ in $[0,+\infty]$, not a supremum of convergence points computed in $\mathbb R$ (which would be $0$ on an unbounded set), and the recursion carries the paper's $a_0=0$ and $\ell=1,\dots,k-1$ conventions, so that $a_2=\mu\nu/\Gamma(2\alpha+1)$ and, at $\alpha=1,\lambda=\nu=1,\mu=0$, the coefficients are those of $\tan$ ($1,0,\tfrac13,\dots$), with $\tau_*=1$ and $R=\pi/2$.

A complete development needs: real-analytic Gamma-function inequalities (log-convexity is in Mathlib; Kershaw's bounds are not); Riemann-sum estimates for symmetric monotone functions on $(0,1)$; the Beta integral $\int_0^1(u(1-u))^{\alpha-1}du=B(\alpha,\alpha)$ (Mathlib has Complex.betaIntegral); and $\liminf$ manipulations of $n$-th roots in ℝ≥0∞. The Gamma-ratio and Riemann-sum lemmas are reusable beyond this mission. Contributions to any milestone, and alternative proofs of the radius bounds, are welcome.

Not formalized: the "Moreover" sentences of Theorem 3.3 (b) (monotonicity and blow-up of the maximal Riccati solution) and (c) (convergence at the radius), the non-homogeneous Theorem 6.1, and the numerical scheme of §4–§5.

Selected references

• G. Callegaro, M. Grasselli, G. Pagès, Fast Hybrid Schemes for Fractional Riccati Equations (Rough is not so Tough), Mathematics of Operations Research 46(1), 2021; arXiv:1805.12587v4. https://arxiv.org/abs/1805.12587
• O. El Euch, M. Rosenbaum, The characteristic function of rough Heston models, Mathematical Finance 29(1):3–38, 2019. https://doi.org/10.1111/mafi.12173
• D. Kershaw, Some extensions of W. Gautschi's inequalities for the gamma function, Mathematics of Computation 41(164):607–611, 1983. https://doi.org/10.1090/S0025-5718-1983-0717710-7
• E. Abi Jaber, M. Larsson, S. Pulido, Affine Volterra processes, Annals of Applied Probability 29(5):3155–3200, 2019; arXiv:1708.08796. https://arxiv.org/abs/1708.08796