Analysis

Motivation

Volatility estimates from daily high, low and closing prices have been used since Parkinson (1980) and Garman and Klass (1980): the range of a day's log-price carries much more information about the volatility $\sigma$ than the close alone. Rogers and Satchell (1991) propose an estimator, $S_1(S_1-X_1)+I_1(I_1-X_1)$, that is unbiased for $\sigma^2$ whatever the drift of the log-price. The companion mission (Part I) formalizes that unbiasedness.

Every such estimator meets the same practical problem. The true high and low of the continuous path are never observed; one sees the maximum and minimum of the path sampled at $N$ times. The sampled maximum $S$ falls short of the true maximum $S_1$ by an amount $\Delta = S_1 - S \ge 0$, and the resulting downward bias is large in practice (Garman and Klass, and Beckers (1983), identified it). Section 3 of Rogers and Satchell proposes a correction: model $\Delta$ by a random variable with an explicit law, compute its first two moments exactly, and subtract their effect. The constants that appear,

$$a=\sqrt{2\pi}\Big[\tfrac14-\tfrac{\sqrt2-1}{6}\Big],\qquad b=\frac{1+3\pi/4}{12},$$

enter the corrected estimator directly. Their simulations (Tables 1–3 of the paper) show that the correction removes most of the bias.

Setting

Fix a volatility $\sigma>0$ and a sampling mesh $h>0$ (in the paper $h=1/N$). For a level $\alpha\ge0$ define

$$G_{\sigma,h}(\alpha)=\int_0^h e^{-2\alpha^2/(u\sigma^2)}\,\frac{du}{(4uh)^{1/2}} .$$

The factor $e^{-2\alpha^2/(u\sigma^2)}$ is the probability that a Brownian bridge of duration $u$ and volatility $\sigma$ climbs above level $\alpha$. The factor $(4uh)^{-1/2}$ is a probability density on $(0,h]$. Since $G_{\sigma,h}(0)=1$ and $G_{\sigma,h}$ decreases continuously to $0$, it is the survival function of a law on $(0,\infty)$. This law is the paper's display (9).

A real random variable $Z$ has distribution (9) if it is measurable and $P(Z>\alpha)=G_{\sigma,h}(\alpha)$ for every $\alpha\ge0$. In the paper, $Z$ is the overshoot of the continuous maximum over the sampled maximum $x$ in the sampling interval to the left of the time $t$ at which $x$ is attained, and $Z'$ is the overshoot in the interval to the right. The paper then assumes (p. 508) that $Z$ and $Z'$ are independent, each with distribution (9), and approximates $\Delta$ by $Z\vee Z'=\max(Z,Z')$. Write $Z\wedge Z'=\min(Z,Z')$.

In Lean, overshootSurvival σ h α is $G_{\sigma,h}(\alpha)$, HasOvershootLaw P σ h Z is "$Z$ has distribution (9) under $P$", and constA, constB are $a$ and $b$.

Formalization targets

Goal: the two moments of $Z\vee Z'$ (Eq. (11), p. 508, and the display on p. 509)

For $\sigma,h>0$ and $Z,Z'$ independent with distribution (9), the variables $Z\vee Z'$ and $(Z\vee Z')^2$ are integrable, and

$$E(Z\vee Z')=a\,\sigma\sqrt h,\qquad E\big[(Z\vee Z')^2\big]=b\,\sigma^2h .$$

Milestones, in the order the paper uses them

1. (9), p. 507. The two integral forms of the survival function agree:

$$\int_0^h e^{-2\alpha^2/(u\sigma^2)}\frac{du}{(4uh)^{1/2}}=\int_{h^{-1}}^\infty e^{-2\alpha^2s/\sigma^2}\frac{ds}{(4hs^3)^{1/2}} .$$

2. (10), p. 508. $EZ=\sigma(2\pi h)^{1/2}/8$.
3. Display before (11), p. 508. $E(Z\wedge Z')=\sqrt{2\pi h}\,(\sqrt2-1)\,\sigma/6$.
4. (12), p. 508. $EZ^2=\sigma^2h/6$.
5. (13), p. 509. $E[(Z\wedge Z')^2]=\frac{\sigma^2h}{4}\big(1-\frac\pi4\big)$.

The goal combines milestones 2–5 through $Z\vee Z'=Z+Z'-Z\wedge Z'$, which the paper uses in (11).

Significance

The result. The two identities are the coefficients of the corrected estimator (5): replacing $\Delta$ and $\Delta^2$ by $a\sigma\sqrt h$ and $b\sigma^2h$ turns the high–low estimator into an equation whose positive root $\hat\sigma_h$ largely removes the discretization bias. The same constants correct the Garman–Klass estimator (p. 509). Without exact values for $a$ and $b$ the correction has no concrete form.

Formalizing it. The paper does each of the four double integrals in a line and says "after some calculation" twice. A machine-checked derivation confirms the printed constants, which are reused in the high–low volatility literature. It also states precisely what is exact (moments of the model law (9) under independence) and what is approximation (that the model describes $\Delta$). To our knowledge none of these identities has been formalized before.

Difficulty

The statements are elementary but none of them is a one-line identity. Each moment is a double or triple improper integral with singular weights $(4hs^3)^{-1/2}$ on an unbounded domain. The minimum of $Z$ and $Z'$ couples two such integrals, and the resulting kernels $(s+u)^{-1/2}$ and $\sqrt{st}/(s+t)$ have to be integrated in closed form over the unit square. Matching $\sqrt2-1$ and $1-\pi/4$ exactly leaves no room for slack. In Lean, every exchange of integration order, change of variables and passage from survival functions to moments has to be justified for non-negative but unbounded functions, and the expectations must be shown finite: the Bochner integral of a non-integrable function is $0$.

Formalization scope

• Model. Random variables live on an arbitrary probability space (Ω, P) with [IsProbabilityMeasure P]. "Distribution (9)" is Measurable Z ∧ ∀ α ≥ 0, P.real {α < Z} = G σ h α, imposed only at levels $\alpha\ge0$: the formula is even in $\alpha$, and imposing it at negative levels would make the hypothesis unsatisfiable. Independence is IndepFun Z Z' P. $Z\vee Z'$ and $Z\wedge Z'$ are max and min.
• Parameters. $\sigma>0$ and $h>0$ only. The paper's $h=1/N\le1$ is not needed and not imposed.
• Explicit readings. "E" is the Bochner integral, and every expectation identity carries its integrability (Integrable, or MemLp … 2 for second moments). The conditioning "$\mid t-h<H_x<t,\ X_t=x$" in (9) and (10) is the modelling context in which the paper derives the law, not a hypothesis. The paper's "$E(Z\wedge Z')^2$" in (13) is read as $E[(Z\wedge Z')^2]$, as its first line shows. The integrals in (9) run over $(0,h]$ and $[h^{-1},\infty)$.
• Not formalized. The approximate statements $E\Delta\doteq a\sigma\sqrt h$ and $E\Delta^2\doteq b\sigma^2h$, the densities (6) and (7), and the independence remark of p. 508 are modelling approximations about the random walk, not theorems. The estimators (5) and $\hat\sigma^2_{GK,h}$ are definitions with no claim attached. The Brownian-bridge maximum (8) is not stated (its print also has a slip: $1-2/u$ for $1-s/u$). Section 4 (simulations) is out of scope.
• Non-triviality. The hypotheses are satisfiable for every $\sigma,h>0$: a probability measure on $\mathbb R$ with survival function $G_{\sigma,h}$ exists, and the two coordinates under its product measure are independent copies. A formalization that stated the survival condition for all $\alpha\in\mathbb R$ would be vacuous and is ruled out. So is one without the integrability conjuncts, which could hold with both sides $0$.
• Related items. The platform's generic identity survival_mean_ibp (mean as an integral of the survival function, under derivative hypotheses) is related but does not fit this setting. Mathlib's layer-cake formula is the general tool for passing between survival functions and moments.
• Welcome contributions. Closed forms for $\int_0^1\!\int_0^1(s+t)^{-1/2}\,ds\,dt$ and $\int_0^1\!\int_0^1\sqrt{st}/(s+t)\,ds\,dt$, which are reusable lemmas, and a general "moments of $\max$ and $\min$ of independent variables from their survival functions" lemma.

Selected references

• L. C. G. Rogers and S. E. Satchell, Estimating variance from high, low and closing prices, The Annals of Applied Probability 1(4) (1991), 504–512. https://doi.org/10.1214/aoap/1177005835
• M. B. Garman and M. J. Klass, On the estimation of security price volatilities from historical data, Journal of Business 53(1) (1980), 67–78. https://doi.org/10.1086/296072
• M. Parkinson, The extreme value method for estimating the variance of the rate of return, Journal of Business 53(1) (1980), 61–65. https://doi.org/10.1086/296071
• S. Beckers, Variances of security price returns based on high, low and closing prices, Journal of Business 56(1) (1983), 97–112.

Motivation

Many optimization algorithms are discretizations of a continuous-time descent: the gradient flow $\dot x=-\nabla f(x)$ for smooth objectives, and its nonsmooth analogue, the subgradient dynamical system, for objectives with kinks or constraints. A basic question about such a flow is whether a bounded trajectory actually converges, rather than merely accumulating on a continuum of critical points, and how fast. For real-analytic $f$ this was settled by Łojasiewicz through his gradient inequality, which forces bounded gradient trajectories to have finite length. Without some such structure the answer is negative: there are smooth functions whose bounded gradient trajectories spiral forever around a circle of critical points.

Bolte, Daniilidis and Lewis (SIAM J. Optim. 17 (2007) 1205–1223) extended the Łojasiewicz inequality to nonsmooth subanalytic functions, possibly taking the value $+\infty$, by replacing $\|\nabla f\|$ with the least norm of a limiting subgradient. Section 4 of the paper turns this inequality into convergence results for subgradient trajectories of convex and lower-$C^2$ functions. This mission formalizes that section. The same "Łojasiewicz argument" later became the Kurdyka–Łojasiewicz framework behind convergence proofs for proximal, alternating and splitting algorithms (Attouch–Bolte 2009; Bolte–Sabach–Teboulle 2014).

Timeline. Łojasiewicz (1963, 1984) proved the gradient inequality for real-analytic functions and finite length of bounded analytic gradient trajectories. Kurdyka (Ann. Inst. Fourier 1998) extended it to $C^1$ functions definable in an o-minimal structure. Kurdyka, Mostowski and Parusiński (2000) proved Thom's gradient conjecture for analytic functions. Bolte, Daniilidis and Lewis (2007) gave the nonsmooth subanalytic version and the trajectory results formalized here.

Setting

Let $f:\mathbb R^n\to\mathbb R\cup\{+\infty\}$ with domain $\operatorname{dom} f=\{x: f(x)<+\infty\}$. The Fréchet subdifferential $\hat\partial f(x)$ is the set of $x^*$ with $\liminf_{y\to x,\,y\neq x}\big(f(y)-f(x)-\langle x^*,y-x\rangle\big)/\|y-x\|\ge0$. The limiting subdifferential $\partial f(x)$ is the set of limits of $x_k^*\in\hat\partial f(x_k)$ with $x_k\to x$ and $f(x_k)\to f(x)$. The nonsmooth slope is $m_f(x)=\inf\{\|x^*\|: x^*\in\partial f(x)\}$, equal to $+\infty$ when $\partial f(x)=\emptyset$, and $\operatorname{crit} f=\{x: 0\in\partial f(x)\}$ is the set of critical points.

The standing assumptions of Section 4 are:

• $(\mathcal H1)$ $f$ is either lower semicontinuous and convex, or lower-$C^2$ with $\operatorname{dom} f=\mathbb R^n$. Lower-$C^2$ means that near each point $f=\max_{s\in S}F(\cdot,s)$ for a compact space $S$ and a jointly continuous $F$ with jointly continuous first and second $x$-derivatives.
• $(\mathcal H2)$ $f$ is somewhere finite and bounded from below.
• $(\mathcal H3)$ $f$ is subanalytic: its graph is locally the projection of a bounded set defined by finitely many real-analytic equalities and strict inequalities.

A trajectory of the subgradient system $(\mathcal G)$ is an absolutely continuous curve $x:[0,T)\to\mathbb R^n$, $T\in(0,+\infty]$, with $\dot x(t)+\partial f(x(t))\ni0$ for almost every $t$ and $\partial f(x(t))\neq\emptyset$ for every $t$. It is maximal if it admits no extension to a longer interval. The Łojasiewicz inequality holds around $a$ with exponent $\theta$ if $|f-f(a)|^\theta/m_f$ is bounded near $a$, with $0^0=1$ and $\infty/\infty=0/0=0$. A Łojasiewicz exponent at $a\in\operatorname{dom} f$ is any such $\theta\in[0,1)$.

Formalization targets

Goal: Theorem 4.7

Under $(\mathcal H1)$–$(\mathcal H3)$, every bounded maximal trajectory $x$ is defined on $[0,+\infty)$ and converges to a critical point $a$. For every Łojasiewicz exponent $\theta$ at $a$ there are $k,k'>0$ and $t_0\ge0$ such that for $t\ge t_0$

$$\|x(t)-a\|\le \begin{cases} k\,(t+1)^{-\frac{1-\theta}{2\theta-1}}, & \theta\in(\tfrac12,1),\\[2pt] k\,e^{-k't}, & \theta=\tfrac12,\end{cases}$$

and for $\theta\in[0,\tfrac12)$, $x(t)=a$ for all large $t$. The constants are existential, so the goal survives any later sharpening of them.

Milestones

1. Corollary 4.1(i): for almost every $t$, $\frac{d}{dt}f(x(t))=\langle\dot x(t),x^*\rangle$ for every $x^*\in\partial f(x(t))$.
2. Corollary 4.1(iii): every trajectory extends to a maximal one on $[0,+\infty)$ with $\dot x\in L^2$.
3. Corollary 4.2: $\|\dot x(t)\|=m_f(x(t))$ and $\frac{d}{dt}f(x(t))=-m_f(x(t))^2$ almost everywhere.
4. Inequality (20): the Łojasiewicz inequality holds around every point of $\operatorname{dom}\partial f$.
5. Theorem 4.5: bounded maximal trajectories have finite length $\int_0^\infty\|\dot x\|<\infty$ and converge to a critical point.
6. The tail bound $\int_t^\infty\|\dot x\|\le\frac{c}{1-\theta}(f(x(t))-f(a))^{1-\theta}$.
7. Inequality (27): $\int_t^\infty\|\dot x\|\le\frac{c^{1/\theta}}{1-\theta}\|\dot x(t)\|^{(1-\theta)/\theta}$ for almost every large $t$.

Significance

Theorem 4.5 says that for convex or lower-$C^2$ subanalytic objectives, including constrained problems through indicator functions of subanalytic sets, the subgradient flow never oscillates indefinitely: bounded trajectories converge to one critical point. Theorem 4.7 adds rates that depend only on the Łojasiewicz exponent at the limit: exponential at $\theta=\tfrac12$, polynomial above it, finite time below it. These are continuous-time templates for the convergence analyses of proximal and splitting methods under the Kurdyka–Łojasiewicz property.

On the formalization side, the results are proved on paper but, to our knowledge, not formalized in any proof assistant. A development would provide reusable infrastructure: a Lean notion of a trajectory of a differential inclusion on $[0,T)$, a chain rule for $f\circ x$ along absolutely continuous curves, and a comparison lemma for the differential inequality $\dot\sigma\le-L\sigma^\alpha$. The analysis of Section 4 uses subanalyticity only through inequality (20), so Theorems 4.5 and 4.7 can be attacked with (20) as an imported milestone, independently of the subanalytic geometry.

Difficulty

Compactness gives cluster points of a bounded trajectory, and the decrease of $f$ gives convergence of $f(x(t))$. Neither gives convergence of $x(t)$. The usual first idea, that $\int_0^\infty\|\dot x\|^2<\infty$ forces convergence, fails, since square-integrable speed allows infinite length. The difficulty is to control $\int\|\dot x\|$ rather than $\int\|\dot x\|^2$. That needs a lower bound on the slope in terms of the function gap near the cluster point, which is exactly what (20) supplies, plus a trapping argument showing the tail of the trajectory stays in the ball where (20) holds. In the nonsmooth setting the chain rule itself is nontrivial: $f\circ x$ is differentiable almost everywhere with derivative $\langle\dot x,x^*\rangle$ for every $x^*\in\partial f(x(t))$, which relies on $\partial f=\hat\partial f$ for convex and lower-$C^2$ functions. Global existence on $[0,+\infty)$ (Corollary 4.1(iii)) must also be established before any asymptotic statement makes sense.

Formalization scope

Space $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). Functions take values in EReal; "bounded from below" by a real number excludes $-\infty$. The limiting subdifferential is the published NonconvexSplitting.Shared.LimitingSubdiff, and convexity is the published MoreauProx.Characterization.EConvex (convex epigraph). The slope $m_f$ is valued in $[0,+\infty]$. The Łojasiewicz inequality is encoded as $|f(y)-f(a)|^\theta\le C\|v\|$ for $y$ near $a$ and every $v\in\partial f(y)$, which is the bounded ratio under the paper's conventions. Times are real numbers and $T\in[0,+\infty]$. Curves are functions $\mathbb R\to\mathbb R^n$ whose values outside $[0,T)$ are irrelevant. "Absolutely continuous on $[0,T)$" means absolutely continuous on every compact $[0,b]\subseteq[0,T)$. Velocities appear only "for almost every $t$". Lengths are lower Lebesgue integrals $\int^-\|\dot x\|$ in $[0,+\infty]$, never Bochner integrals (which would vanish for a non-integrable speed).

Two trivializations are ruled out. Maximality is a hypothesis and $T=+\infty$ is a conclusion: assuming $T=+\infty$ would narrow the theorem, and dropping maximality would make it false. Rates are claimed for every Łojasiewicz exponent at the limit, not for one chosen exponent. Corollary 4.1(iii) is stated as "defined on $\mathbb R_+$ with $\dot{\hat x}\in L^2$", because the printed $\hat x\in W^{1,2}(\mathbb R_+)$ would fail for any trajectory with nonzero limit.

Needed infrastructure: absolutely continuous curves and their a.e. derivatives (Mathlib's AbsolutelyContinuousOnInterval), chain rules for convex and lower-$C^2$ functions, existence and uniqueness for monotone differential inclusions (Brézis), and an ODE comparison principle. Contributions to any of these are reusable well beyond this mission.

Selected references

• J. Bolte, A. Daniilidis, A. Lewis, The Łojasiewicz inequality for nonsmooth subanalytic functions with applications to subgradient dynamical systems, SIAM J. Optim. 17(4) (2007) 1205–1223. https://doi.org/10.1137/050644641
• H. Brézis, Opérateurs maximaux monotones et semi-groupes de contractions dans les espaces de Hilbert, North-Holland, 1973.
• J.-P. Aubin, A. Cellina, Differential Inclusions, Springer, 1984. https://doi.org/10.1007/978-3-642-69512-4
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3
• K. Kurdyka, On gradients of functions definable in o-minimal structures, Ann. Inst. Fourier 48 (1998) 769–783. https://doi.org/10.5802/aif.1638
• H. Attouch, J. Bolte, On the convergence of the proximal algorithm for nonsmooth functions involving analytic features, Math. Program. 116 (2009) 5–16. https://doi.org/10.1007/s10107-007-0133-5

Motivation

The question of the largest area that can be moved around a corner has been studied since the late 1960s. Leo Moser posed it in 1966, and F. H. Hammersley gave the lower bound $\pi/2+2/\pi\approx2.2074$ and the upper bound $2\sqrt{2}\approx2.828$ in 1968. Joseph Gerver constructed a shape of area approximately $2.2195$ in 1992 and described four constants $A$, $B$, $\varphi$, $\theta$ satisfying four equations, from which the shape is built. Dan Romik rewrote those equations in exact form as equations (1)-(4) in 2018 and reported high-precision values of the constants. Jineon Baek proved in 2024 that Gerver's shape is optimal: no larger shape can be moved around the corner. The proof was autoformalized in Lean 4 by Dean Cureton and AI agents in 2026, as the repository deancureton/MovingSofa, building on Dawid Trela's formalization of Gerver's constants and motion, Jonathan Ho's Brunn-Minkowski development, the Jordan-curve developments of R. Kirov and the TauCeti project, and Google DeepMind's formal-conjectures statement.

Timeline: Moser poses the problem (1966); Hammersley gives the $\pi/2+2/\pi\approx2.2074$ lower bound and the $2\sqrt{2}\approx2.828$ upper bound (1968); Gerver exhibits the $2.2195$ shape and its differential equations (1992); Romik gives the exact equations and numerics (2018); Baek proves optimality (2024, arXiv:2411.19826); Cureton et al. complete a Lean 4 proof of optimality, existence and uniqueness of the constants, and movability of Gerver's shape (2026).

Setting

Work in the plane $\mathbb{R}^2$. The hallway is $(-\infty,1]\times[0,1]\cup[0,1]\times(-\infty,1]$, the union of its horizontal and vertical sides. A moving sofa is a nonempty closed connected set $s$ in the horizontal side together with a continuous path $m$ of plane isometries indexed by the unit interval, starting at the identity, keeping the image of $s$ inside the hallway at all times, and ending with the image inside the vertical side. Motions take values in the full isometry group $E(2)$; continuity together with $m(0)=\mathrm{id}$ forces the path to lie in the orientation-preserving component. The sofa constant is the supremum, in the extended nonnegative reals, of the areas $\mathrm{volume}(s)$ over all moving sofas. The supremum is finite, at least $11/5$, and attained.

Gerver's shape is defined from a rotation path. For constants $A$, $B$, $\varphi$, $\theta$, let $r$ be the piecewise function with breakpoints $\varphi$, $\theta$, $\pi/2-\theta$, $\pi/2-\varphi$ from Romik's Theorem 2, let $x$ and $y$ be its cosine and sine integrals, and let $p$ be the associated translation path. The sofa for those constants is the intersection over angles in $[0,\pi/2]$ of the correspondingly rotated and translated hallways, with the endpoints using the horizontal and vertical sides. The four equations ABphiThetaSpec cut out the constants. They have exactly one solution with $0\le\varphi\le\theta\le\pi/4$ and $0\le A$, $0\le B$. The same Lean development uses the identical notation as the formal statements, so prose and code read as one document.

Formalization targets

Goal: optimality of Gerver's sofa

For every $A$, $B$, $\varphi$, $\theta$ satisfying ABphiThetaSpec,

$$\mathrm{sofaConstant} = \mathrm{volume}(\mathrm{gerversSofaWith}(A,B,\varphi,\theta)).$$

The goal leaves unfixed which solution of the spec is used; by uniqueness all choices give the same shape up to the proved identification, so this is the stable form of Baek's Theorem 1.1. It asserts that the supremum equals the area of Gerver's shape, hence that no moving sofa has larger area and that the supremum is attained.

Supporting targets

$$\exists!\,(A,B,\varphi,\theta),\ \mathrm{ABphiThetaSpec}(A,B,\varphi,\theta).$$ $$\forall\,A,B,\varphi,\theta,\ \mathrm{ABphiThetaSpec}(A,B,\varphi,\theta)\implies \exists\,m,\ \mathrm{IsMovingSofa}(\mathrm{gerversSofaWith}(A,B,\varphi,\theta),m).$$

The first is Gerver's Theorem 2 in Romik's equation form on the closed domain. The second says every such shape admits a hallway motion. Together they supply the constants and the witness that the supremum is attained. The live mission records a root sketch composing the upper-bound half (every moving sofa is bounded by Gerver's area) with the movability witness into the supremum equality.

Significance

The result itself closes a problem open since 1966. It identifies the maximum area, shows the maximum is attained by an explicit shape, and determines that shape from four equations whose solution is unique. Consequences include the numerical enclosure $11/5\le\mathrm{volume}\le\infty$ proved by interval arithmetic, the finiteness of the supremum, and the reduction of future improvements to the analysis of the functional $Q$ on caps. Without it the exact maximum remains unknown.

Formalizing it adds a machine-checked proof that makes no classical area assumption: the Green-type curve-area identity and the Minkowski-type mixed-area facts quoted by the paper are proved, the paper's 11 proof gaps and 33 misprints are repaired, and the numerical certificate is kernel-checked. The hallway, motion, cap, convex-body, and surface-measure infrastructure is reusable for related isoperimetric and kinematic formalizations. Status honesty: the underlying paper proof is complete and has been formalized in the source repository; on this platform the three statements above are open targets awaiting proofs, and the uniqueness of the maximizer up to rigid motion remains open and is not part of this mission.

Difficulty

The obvious argument bounds the area of an arbitrary sofa by the area of a circumscribed cap, but caps need not satisfy the injectivity condition that makes the functional $Q$ an upper bound, and $Q$ need not be concave on the full space of caps. Maximizing sequences of polygons need not converge to a sofa, and limits need not be connected or attain the supremum. The naive idea of taking a supremum over all connected closed sets and extracting a convergent subsequence fails until compactness of motions, closedness of the moving-sofa predicate, and a balanced maximum with rotation angle $\pi/2$ are established. Each step fails for general sets and only holds after the polygon approximation and monotonization constructions.

Formalization scope

Lean represents the plane as EuclideanSpace ℝ (Fin 2) with its standard orientation, hallway sides as explicit sets, motions as I → E(2) where E(2) is ℝ² ≃ᵃⁱ[ℝ] ℝ² with the topology induced from continuous maps, and area as MeasureSpace.volume. The supremum is in ℝ≥0∞. Statements target the c5ea003 (Lean v4.30.0) environment, an older supported revision against which the development was verified locally. The spec uses non-strict inequalities, which makes uniqueness stronger than the strict-inequality literature form. The functions $r$, $x$, $y$, $p$ take the constants as explicit arguments rather than reading global chosen constants, so the definition bundle stays independent of the existence proof; given uniqueness this implies the source statements. Boundedness and measurability are not assumed; every moving sofa is proved compact in the source development. A submission that drops closedness or connectedness, that allows a discontinuous motion, or that hard-codes the numerical value $2.2195$ instead of proving equality with the volume of the defined shape, does not satisfy the statements. Contributions welcome: direct proofs of the three targets, sharper enclosures of the volume, and reusable hallway and motion lemmas. Out of scope: uniqueness up to congruence, the $11/5$ certificate details beyond the stated lower bound, and the 20 unformalized numbered environments listed in the source NOTES.md that none of the three targets depends on.

Selected references

• Jineon Baek, Optimality of Gerver's Sofa, arXiv:2411.19826, 2024. https://arxiv.org/abs/2411.19826
• Joseph L. Gerver, On moving a sofa around a corner, Geometriae Dedicata 42 (1992), 267-283.
• Dan Romik, Differential equations and exact solutions in the moving sofa problem, Experimental Mathematics 27 (2018), 316-330. https://arxiv.org/abs/1606.08111
• Dean Cureton et al., MovingSofa: Autoformalization of Baek's solution, 2026. https://github.com/deancureton/MovingSofa
• Google DeepMind, formal-conjectures, FormalConjectures/Wikipedia/MovingSofa.lean at ddfbaf90. https://github.com/google-deepmind/formal-conjectures
• Dawid Trela, GerverSofaLean v1.1.0. https://github.com/dawidmtrela-dotcom/GerverSofaLean

Motivation

Feedback laws that damp vibrations in elastic structures are implemented by sensors and actuators, and a physical loop always reacts with some time delay $\tau>0$: the damping force at time $t$ is computed from the velocity measured at time $t-\tau$. Datko, Lagnese and Polis showed in 1986 that an arbitrarily small delay in a boundary feedback can destroy the stability of a one-dimensional wave equation (Datko–Lagnese–Polis, SIAM J. Control Optim. 24 (1986)), and Datko showed that such fragility is common to a broad class of feedback-stabilized hyperbolic systems (Datko, SIAM J. Control Optim. 26 (1988)). Delay-robustness is therefore a genuine question for every stabilizing feedback, not a technicality.

Nicaise and Pignotti (SIAM J. Control Optim. 45 (2006) 1561–1585) identified a simple sufficient condition in several space dimensions: if the feedback contains an undelayed velocity term with gain $\mu_1$ and a delayed one with gain $\mu_2$, and $\mu_2<\mu_1$, the energy still decays exponentially; if $\mu_2\ge\mu_1$, instabilities appear for some delays. This mission formalizes the stability half for internal (distributed) damping, localized near the Neumann part of the boundary.

Timeline.

• 1986: Datko, Lagnese, Polis — small delays destabilize a boundary-damped 1D wave equation.
• 1988: Datko — many feedback-stabilized hyperbolic systems are not robust with respect to small delays.
• 1990: Zuazua — exponential decay for the semilinear wave equation with locally distributed damping, without delay (Comm. PDE 15 (1990)); Liu (1997) treats locally distributed damping for general conservative systems (SIAM J. Control Optim. 35 (1997)).
• 2006: Nicaise, Pignotti — exponential decay with a delayed boundary or internal feedback under $\mu_2<\mu_1$ (Theorems 1.1 and 1.3), and instability examples when $\mu_2\ge\mu_1$ (Theorems 1.2 and 1.4).

Setting

Let $\Omega\subset\mathbb{R}^n$, $n\ge1$, be a bounded open set with boundary $\Gamma$ of class $C^2$, split as $\Gamma=\Gamma_D\cup\Gamma_N$ with $\overline{\Gamma_D}\cap\overline{\Gamma_N}=\emptyset$ and $\Gamma_D\neq\emptyset$. Write $\nu$ for the outer unit normal, $d\Gamma$ for the surface measure, $u_t,u_{tt}$ for time derivatives and $\Delta$ for the Laplacian in $x$.

Geometric hypothesis (1.6)–(1.7): there are a $C^2$ function $v$ and $\alpha>0$ with $\langle D^2v(x)\xi,\xi\rangle\ge2\alpha|\xi|^2$ for all $x\in\overline\Omega$, $\xi\in\mathbb{R}^n$, and $\nabla v(x)\cdot\nu(x)\le0$ on $\Gamma_D$.

Damping coefficient. $\omega\subset\Omega$ is an open neighbourhood of $\Gamma_N$ (in $\Omega$), and $a\in L^\infty(\Omega)$ satisfies

$$a(x)\ge0\ \text{a.e. in }\Omega\quad(1.17),\qquad a(x)>a_0>0\ \text{a.e. in }\omega\quad(1.18).$$

The system (1.12)–(1.16): for gains $\mu_1,\mu_2>0$ and delay $\tau>0$,

$$u_{tt}(x,t)-\Delta u(x,t)+a(x)\big[\mu_1u_t(x,t)+\mu_2u_t(x,t-\tau)\big]=0\quad\text{in }\Omega\times(0,\infty),$$

with $u=0$ on $\Gamma_D$, $\partial u/\partial\nu=0$ on $\Gamma_N$, initial data $u(\cdot,0)=u_0$, $u_t(\cdot,0)=u_1$, and history $u_t(x,t-\tau)=g_0(x,t-\tau)$ for $t\in(0,\tau)$.

The energy. Assume $\mu_2<\mu_1$ (1.8) and fix $\xi$ with $\tau\mu_2<\xi<\tau(2\mu_1-\mu_2)$ (1.10). Then

$$\mathcal F(t)=\frac12\int_\Omega\big\{u_t^2(x,t)+|\nabla u(x,t)|^2\big\}dx+\frac\xi2\int_\Omega a(x)\int_0^1u_t^2(x,t-\tau\rho)\,d\rho\,dx\qquad(1.19).$$

The first summand is the standard energy $\mathcal E(t)$; the second accounts for the velocity history on the delay window.

Formalization targets

Goal: Theorem 1.3

There exist $C_1,C_2>0$, depending on the data but not on the solution, such that every solution satisfies

$$\mathcal F(t)\le C_1\,\mathcal F(0)\,e^{-C_2t}\qquad\forall t\ge0.$$

The constants are left existential, as in the paper, so no later sharpening of rates invalidates the goal.

Milestones (in the order of the proof)

1. (4.4) The energy identity

$$\mathcal F'(t)=-\mu_1\!\int_\Omega a u_t^2(t)-\mu_2\!\int_\Omega a u_t(t)u_t(t-\tau)+\frac{\xi\tau^{-1}}2\!\int_\Omega a u_t^2(t)-\frac{\xi\tau^{-1}}2\!\int_\Omega a u_t^2(t-\tau).$$

2. Proposition 4.1 $\mathcal F$ is nonincreasing and $\mathcal F'(t)\le-C\int_\Omega a\{u_t^2(t)+u_t^2(t-\tau)\}dx$ with $C>0$.
3. Proposition 4.2 Observability for the undamped mixed problem: for $T$ larger than some $T_0$, $\mathcal E_w(0)\le C_1\int_0^T\int_\omega w_t^2\,dx\,dt$.
4. Proposition 4.3 Observability for the delayed system: for $T$ larger than some $\overline T$, $\mathcal F(0)\le C_0\int_0^T\int_\Omega a\{u_t^2(t)+u_t^2(t-\tau)\}dx\,dt$.
5. Contraction step (p. 1579): some $T>0$ and $\widetilde C\in[0,1)$ with $\mathcal F(T)\le\widetilde C\,\mathcal F(0)$ for every solution.

Significance

The result. Theorem 1.3 shows that a localized viscous damping acting only near the Neumann boundary keeps its exponential stabilizing effect when part of the feedback is delayed, provided the delayed gain is dominated by the undelayed one. Together with Theorem 1.4 of the same paper (instability for $\mu_2\ge\mu_1$ and suitable delays) it gives a sharp threshold in terms of the gains. The energy $\mathcal F$ with its history term became the standard Lyapunov functional for delayed wave and plate equations in the literature that followed.

Formalizing it. The theorem is proved in the paper; no machine-checked proof of it, or of any exponential decay result for a multidimensional wave equation, is known to exist. A complete development would produce reusable Lean infrastructure: energy identities for the wave equation on $C^2$ domains via the divergence theorem, the delay-energy calculus, and an observability inequality for the wave equation with mixed boundary conditions. Each milestone has value on its own; Proposition 4.2 in particular is a classical control-theoretic result.

Difficulty

The energy estimates (milestones 1 and 2) are calculus once the divergence theorem is available. The central difficulty is observability. Energy dissipation alone gives only $\mathcal F$ nonincreasing; exponential decay needs the energy at time $0$ to be controlled by the energy dissipated on $[0,T]$ (Proposition 4.3), and that needs the conservative wave equation to be observable from $\omega$ (Proposition 4.2). The observability inequality does not follow from energy identities: the paper relies on Carleman estimates of Lasiecka–Triggiani–Yao (1999) and a compactness–uniqueness argument, neither of which is available in Mathlib. The obvious attempt, a multiplier identity with $\nabla v\cdot\nabla u$ alone, leaves boundary terms on $\Gamma_N$ that cannot be absorbed without a localization near $\Gamma_N$ and a lower-order compactness step.

Formalization scope

• Points are EuclideanSpace ℝ (Fin n) with 1 ≤ n; solutions are real valued.
• The $C^2$ boundary is given by a global $C^2$ defining function $\psi$ with $\Omega=\{\psi<0\}$, $\partial\Omega=\{\psi=0\}$, $\nabla\psi\ne0$ on $\partial\Omega$; $\nu=\nabla\psi/|\nabla\psi|$.
• The surface measure $d\Gamma$ is a finite measure carried by $\partial\Omega$ for which the Gauss–Green formula holds for every $C^1$ vector field; this determines it uniquely. It is not Mathlib's unnormalized Hausdorff measure.
• Solutions are classical: $u$ is $C^2$ on $\mathbb{R}^n\times\mathbb{R}$, the equation holds for every $t>0$ and almost every $x\in\Omega$ (because $a$ is only $L^\infty$), and the initial data and history are the values of $u$ and $u_t$ at $t\le0$. This is a subclass of the paper's solutions, so the formal theorems are consequences of the paper's.
• $a$ is measurable and essentially bounded on $\Omega$; (1.17) and (1.18) are almost-everywhere conditions. "Open neighbourhood of $\Gamma_N$" means $\omega\supseteq O\cap\Omega$ for some open $O\supseteq\Gamma_N$ (a subset of $\Omega$ cannot contain $\Gamma_N$ itself).
• Added hypothesis (Propositions 4.2, 4.3, the contraction step and Theorem 1.3): the closure of every connected component of $\Omega$ meets $\Gamma_D$; this holds whenever $\Omega$ is connected. The proof of Proposition 4.2 uses Poincaré's inequality for functions vanishing on $\Gamma_D$, and its compactness–uniqueness step concludes that a harmonic function vanishing on $\Gamma_D$ with zero normal derivative on $\Gamma_N$ is zero; both need this condition.
• "Decreasing" in Proposition 4.1 is read as nonincreasing; its constant $C>0$ is existential, chosen before the solution.
• Printed slips on p. 1575: the last line of (4.3) integrates with $d\Gamma$ where $dx$ is meant, and its first line repeats $u_\rho(x,t-\tau)$ for $u_\rho(x,t-\tau\rho)$. Neither affects any formal statement; (4.4) itself is correct.
• A formalization in which the $a$-weighted integrals are Lean's junk value $0$ (non-measurable $a$), in which $\omega$ is required to contain $\Gamma_N$ (unsatisfiable), or in which the surface measure is arbitrary, would trivialize or falsify the targets; all three are excluded by the definitions.

Needed infrastructure: the divergence theorem on $C^2$ domains (assumed here as a structure field), differentiation under the integral sign for the energies, Carleman estimates or another route to observability for the mixed wave problem, and a compactness argument (Rellich). Contributions of any of these as standalone lemmas are welcome.

Selected references

• S. Nicaise, C. Pignotti, Stability and instability results of the wave equation with a delay term in the boundary or internal feedbacks, SIAM J. Control Optim. 45(5):1561–1585, 2006. https://doi.org/10.1137/060648891
• R. Datko, J. Lagnese, M. P. Polis, An example on the effect of time delays in boundary feedback stabilization of wave equations, SIAM J. Control Optim. 24:152–156, 1986. https://doi.org/10.1137/0324007
• R. Datko, Not all feedback stabilized hyperbolic systems are robust with respect to small time delays in their feedbacks, SIAM J. Control Optim. 26:697–713, 1988. https://doi.org/10.1137/0326040
• E. Zuazua, Exponential decay for the semilinear wave equation with locally distributed damping, Comm. Partial Differential Equations 15:205–235, 1990. https://doi.org/10.1080/03605309908820684
• K. Liu, Locally distributed control and damping for the conservative systems, SIAM J. Control Optim. 35:1574–1590, 1997. https://doi.org/10.1137/S0363012995284928
• I. Lasiecka, R. Triggiani, P. F. Yao, Inverse/observability estimates for second-order hyperbolic equations with variable coefficients, J. Math. Anal. Appl. 235:13–57, 1999 (reference [14] of the paper; the Carleman estimates used in Proposition 4.2). https://doi.org/10.1006/jmaa.1999.6348

Motivation

In a scattering experiment a particle arrives from far away, interacts with a target, and leaves again. Far from the target the forces are negligible, so long before and long after the collision the particle should move like a free particle. Scattering theory makes this precise by comparing two quantum dynamics: the free evolution $\mathrm e^{-\mathrm itH_0}$ generated by the kinetic energy $H_0 = -\Delta$, and the full evolution $\mathrm e^{-\mathrm itH}$ generated by $H = H_0 + V$. The objects that compare them are the wave operators (Møller operators) $\Omega_\pm$, introduced by Møller (1945) and put on a rigorous footing by Jauch (1958) and Kato. Cook (1957) gave the first practical criterion for their existence. Kuroda, Birman, Agmon, Enß and others later developed the theory up to asymptotic completeness for short-range potentials.

This mission formalizes the abstract part of Chapter 12 of Teschl's Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009): the definition and basic structure of the wave operators, Cook's criterion, and the existence of the wave operators for a square-integrable potential in three dimensions.

Setting

Let $\mathfrak H$ be a complex Hilbert space. An operator $A$ is a linear map on a subspace $\mathfrak D(A)$, its domain; $A$ is self-adjoint if $\mathfrak D(A)$ is dense and $A = A^*$. A projection-valued measure $P$ assigns to each Borel set $\Omega \subseteq \mathbb R$ an orthogonal projection $P(\Omega)$, with $P(\mathbb R) = \mathbb I$ and $P(\bigcup_n\Omega_n)\psi = \sum_n P(\Omega_n)\psi$ for disjoint $\Omega_n$. The spectral measure of $\psi$ is $\mu_\psi(\Omega) = \langle\psi, P(\Omega)\psi\rangle$. By the spectral theorem every self-adjoint $A$ equals $\int\lambda\,dP(\lambda)$ for a unique $P$: $\mathfrak D(A) = \{\psi \mid \int\lambda^2\,d\mu_\psi < \infty\}$ and $\langle\psi, A\psi\rangle = \int\lambda\,d\mu_\psi$. The time evolution $\mathrm e^{-\mathrm itA}$ is the bounded operator with $\langle\psi, \mathrm e^{-\mathrm itA}\psi\rangle = \int\mathrm e^{-\mathrm it\lambda}\,d\mu_\psi(\lambda)$.

For two self-adjoint operators $H_0$, $H$ the wave operators are

$$\mathfrak D(\Omega_\pm) = \{\psi \in \mathfrak H \mid \exists\lim_{t\to\pm\infty}\mathrm e^{\mathrm itH}\mathrm e^{-\mathrm itH_0}\psi\}, \qquad \Omega_\pm\psi = \lim_{t\to\pm\infty}\mathrm e^{\mathrm itH}\mathrm e^{-\mathrm itH_0}\psi .$$

$\mathfrak D(\Omega_\pm)$ is the set of asymptotic states and $\operatorname{Ran}(\Omega_\pm) = \Omega_\pm\mathfrak D(\Omega_\pm)$ the set of states that have one. A closed subspace $\mathfrak H_1$ with projection $P_1$ reduces $A$ if $P_1\mathfrak D(A) \subseteq \mathfrak D(A)$ and $P_1A\psi = AP_1\psi$ for $\psi \in \mathfrak D(A)$.

On $L^2(\mathbb R^n)$ the free Schrödinger operator is $H_0 = -\Delta$ with domain the Sobolev space $H^2(\mathbb R^n)$: under the Fourier transform it is multiplication by $p^2$ on $\{\varphi \mid p^2\varphi \in L^2\}$. For a real potential $V$, $H = H_0 + V$ has $\mathfrak D(H) = H^2(\mathbb R^n)$ and $(H\psi)(x) = (H_0\psi)(x) + V(x)\psi(x)$.

Formalization targets

Goal: existence of the wave operators for $V \in L^2(\mathbb R^3)$ (Theorem 12.4)

Let $H_0$ be the free Schrödinger operator on $L^2(\mathbb R^3)$ and $H = H_0 + V$ with a real $V \in L^2(\mathbb R^3)$. Then

$$\mathfrak D(\Omega_+) = \mathfrak D(\Omega_-) = L^2(\mathbb R^3),$$

that is, $\lim_{t\to\pm\infty}\mathrm e^{\mathrm itH}\mathrm e^{-\mathrm itH_0}\psi$ exists for every $\psi$ and both signs. Since the spectrum of $H_0$ is purely absolutely continuous, this is exactly what Teschl calls "the wave operators exist" (12.14).

Milestones

• Lemma 12.1. $\mathfrak D(\Omega_\pm)$ and $\operatorname{Ran}(\Omega_\pm)$ are closed and $\Omega_\pm : \mathfrak D(\Omega_\pm) \to \operatorname{Ran}(\Omega_\pm)$ is unitary.
• Theorem 12.2. $\mathfrak D(\Omega_\pm)$ reduces $H_0$, $\operatorname{Ran}(\Omega_\pm)$ reduces $H$, and the restricted operators are unitarily equivalent: $\Omega_\pm H_0\psi = H\Omega_\pm\psi$ for $\psi \in \mathfrak D(\Omega_\pm) \cap \mathfrak D(H_0)$.
• Lemma 12.3 (Cook). If $\mathfrak D(H) \subseteq \mathfrak D(H_0)$, $\psi \in \mathfrak D(H_0)$ and $\int_0^\infty\|(H - H_0)\exp(\mp\mathrm itH_0)\psi\|\,dt < \infty$, then $\psi \in \mathfrak D(\Omega_\pm)$ and $\|(\Omega_\pm - \mathbb I)\psi\| \le \int_0^\infty\|(H - H_0)\exp(\mp\mathrm itH_0)\psi\|\,dt$.

Significance

Existence of the wave operators is the first step of every scattering theory for Schrödinger operators: without it the scattering operator $S = \Omega_+^{-1}\Omega_-$ is not defined on a useful set of states, and the questions of completeness and asymptotic completeness (Enß's theorem, Theorem 12.12 of the same chapter) cannot be posed. Lemma 12.1 and Theorem 12.2 are the structural facts that make $\Omega_\pm$ partial isometries intertwining the two Hamiltonians; they imply that $H$ restricted to $\operatorname{Ran}(\Omega_\pm)$ has absolutely continuous spectrum whenever $H_0$ does, and that kinetic energy is conserved in scattering. Cook's criterion is the tool used in practice to prove existence for concrete potentials, including Coulomb-type and time-dependent problems.

The results are classical and proved in the literature. They are not formalized. Mathlib has neither the spectral theorem nor a functional calculus for unbounded self-adjoint operators, and no scattering theory. The platform has no statement about wave operators; its BookProof development contains Stone's theorem for its own structure of unbounded operators, which this mission does not use.

Difficulty

The limit defining $\Omega_\pm$ involves two unitary groups whose generators do not commute, and neither group is explicit for the perturbed operator $H$. For Cook's criterion the product $\mathrm e^{\mathrm itH}\mathrm e^{-\mathrm itH_0}\psi$ has to be differentiated in $t$, which needs control of domains: $\mathrm e^{-\mathrm itH_0}\psi$ must stay in the domain of $H - H_0$, and the derivative of a strongly continuous unitary group exists only on the domain of its generator. For the goal, the time evolution of a general $\psi \in L^2(\mathbb R^3)$ has no decay rate at all, and the potential $V \in L^2$ is unbounded and has no decay assumption beyond square integrability, so the integrability condition of Cook's criterion cannot be checked for every $\psi$ directly. The intertwining relation (12.8) concerns unbounded operators and needs the reduction of the domains, not only an identity between bounded operators.

Formalization scope

The formalization uses Lean 4 with Mathlib. Operators are LinearPMaps H →ₗ.[ℂ] H on a complex Hilbert space; self-adjointness is Mathlib's IsSelfAdjoint. Separability is not assumed.

The spectral theorem is not part of this mission. Every statement takes projection-valued measures $P_0$ and $P$ as data, with the hypotheses $H_0 = \int\lambda\,dP_0(\lambda)$ and $H = \int\lambda\,dP(\lambda)$ (domain and quadratic form as above), which is the form the spectral theorem guarantees and which determines $P_0$ and $P$. The time evolutions are $\mathrm e^{-\mathrm itH_0} = \int\mathrm e^{-\mathrm it\lambda}\,dP_0$ and $\mathrm e^{-\mathrm itH} = \int\mathrm e^{-\mathrm it\lambda}\,dP$. In the goal, the self-adjointness of $H = H_0 + V$ (Theorem 10.2 of the book) enters only through the existence of $P$. Nothing is assumed about $\Omega_\pm$.

The sign of $\Omega_\pm$ is a unit s : ℤˣ, and $t \to \pm\infty$ is written as $t \to +\infty$ in the variable $st$. $\Omega_\pm$ is Mathlib's limUnder and is used only on $\mathfrak D(\Omega_\pm)$. A formalization that set $\Omega_\pm\psi = 0$ where the limit fails and then proved only that $\Omega_\pm$ is isometric would lose the content of the goal; here the goal asserts that the limit exists for every $\psi \in L^2(\mathbb R^3)$. In Cook's lemma the finiteness of the integral is integrability on $(0,\infty)$, the bound uses the Bochner integral, and the hypothesis that $\exp(\mp\mathrm itH_0)\psi$ lies in $\mathfrak D(H)$ for $t \ge 0$, which the integrand presupposes, is explicit.

$L^2(\mathbb R^3)$ is Mathlib's Lp ℂ 2 on EuclideanSpace ℝ (Fin 3). The free Schrödinger operator is characterized through Mathlib's unitary $L^2$ Fourier transform $\mathcal F_M f(\xi) = \int\mathrm e^{-2\pi\mathrm i\langle x,\xi\rangle}f(x)\,dx$, not the book's $(2\pi)^{-n/2}\int\mathrm e^{-\mathrm ipx}f(x)\,dx$. The constants are translated: $\mathfrak D(H_0) = \{\psi \mid |\xi|^2\mathcal F_M\psi \in L^2\}$ and $\mathcal F_M(H_0\psi) = 4\pi^2|\xi|^2\mathcal F_M\psi$. $H = H_0 + V$ has $\mathfrak D(H) = \mathfrak D(H_0)$ and $H\psi = H_0\psi + V\psi$ almost everywhere.

A complete development needs a functional calculus for projection-valued measures (strong continuity and differentiability of $\mathrm e^{-\mathrm itA}$ on $\mathfrak D(A)$, Theorem 5.1), the explicit $L^1 \to L^\infty$ decay of the free Schrödinger group in $\mathbb R^3$ ((7.31) of the book), and density of $L^1 \cap H^2$ in $L^2$. These pieces are reusable for the rest of Chapter 12 (incoming and outgoing states, short-range potentials, asymptotic completeness). Proofs of any milestone and of such supporting lemmas are welcome.

Selected references

• G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, American Mathematical Society, 2009. doi:10.1090/gsm/099. Chapter 12, pp. 247–257.
• J. M. Cook, Convergence to the Møller wave-matrix, J. Math. and Phys. 36 (1957), 82–87. doi:10.1002/sapm195736182.
• J. M. Jauch, Theory of the scattering operator, Helv. Phys. Acta 31 (1958), 127–158.
• M. Reed, B. Simon, Methods of Modern Mathematical Physics III: Scattering Theory, Academic Press, 1979.
• V. Enß, Asymptotic completeness for quantum mechanical potential scattering. I. Short range potentials, Comm. Math. Phys. 61 (1978), 285–291. doi:10.1007/BF01940771.

Motivation

Quantum mechanics describes mixed states by density operators: positive operators $\rho$ on a Hilbert space with $\operatorname{tr}(\rho) = 1$. Expectation values are traces $\operatorname{tr}(\rho A)$, perturbation determinants and spectral shift functions are built from traces of resolvent differences, and scattering theory (the Kato–Rosenblum and Birman–Krein theorems) is phrased in terms of trace class perturbations. All of this needs a trace in infinite dimensions, and the trace $\sum_n \langle \varphi_n, K\varphi_n\rangle$ only makes sense on a restricted class of operators.

This mission formalizes Sections 6.2–6.3 of G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators (AMS Graduate Studies in Mathematics 99, 2009), the standard route from compact operators through Hilbert–Schmidt operators to the trace class. The theory goes back to von Neumann and Schatten in the 1940s (R. Schatten, Norm Ideals of Completely Continuous Operators, Springer 1960). A modern account is B. Simon, Trace Ideals and Their Applications (AMS 2005).

Setting

Let $\mathfrak{H}$ be a complex Hilbert space, with inner product $\langle\cdot,\cdot\rangle$ conjugate-linear in the first argument, and let $\mathfrak{L}(\mathfrak{H})$ be the bounded linear operators on $\mathfrak{H}$ with the operator norm $\|A\|$. An operator is of finite rank if its range is finite dimensional, and the compact operators $\mathfrak{C}(\mathfrak{H})$ are the norm closure of the finite rank operators.

For $K \in \mathfrak{L}(\mathfrak{H})$ with adjoint $K^*$, the operator $K^*K$ is positive. The singular values $s_j(K) > 0$ of a compact $K$ are the square roots of the nonzero eigenvalues of $K^*K$, each repeated according to its multiplicity $\dim\operatorname{Ker}(K^*K - \mu)$. For $p \ge 1$ the Schatten $p$-norm and Schatten $p$-class are

$$\|K\|_p = \Big(\sum_j s_j(K)^p\Big)^{1/p} \in [0,\infty], \qquad \mathcal{J}_p(\mathfrak{H}) = \{K \in \mathfrak{C}(\mathfrak{H}) \mid \|K\|_p < \infty\}.$$

A compact $K$ is Hilbert–Schmidt if $K \in \mathcal{J}_2(\mathfrak{H})$ and trace class if $K \in \mathcal{J}_1(\mathfrak{H})$. For an orthonormal basis $\{\varphi_n\}$ of $\mathfrak{H}$ the trace is

$$\operatorname{tr}(K) = \sum_n \langle \varphi_n, K\varphi_n\rangle .$$

In Lean these are compactOperators H, schattenNorm p K, schattenClass H p, IsHilbertSchmidt K, IsTraceClass K and trace K, in the namespace TeschlQM.TraceClass.

Formalization targets

Goal: the trace is well defined (Lemma 6.15)

For every trace class $K$ and every orthonormal basis $\{\varphi_n\}$ the series (6.26) converges, and for any two orthonormal bases $\{\varphi_n\}$, $\{\psi_m\}$

$$\sum_n \langle \varphi_n, K\varphi_n\rangle = \sum_m \langle \psi_m, K\psi_m\rangle = \operatorname{tr}(K).$$

Milestones

1. Theorem 6.7 (canonical form): a compact $K$ has the form $K = \sum_j s_j\langle\phi_j, \cdot\rangle\hat\phi_j$ with orthonormal $\{\phi_j\}$, $\{\hat\phi_j\}$, and the $s_j^2$ are the nonzero eigenvalues of $K^*K$ and of $KK^*$, counted with multiplicity.
2. Lemma 6.10: a compact $K$ is Hilbert–Schmidt iff $\sum_n\|K\psi_n\|^2 < \infty$ for some orthonormal basis, and then $\sum_n\|K\psi_n\|^2 = \|K\|_2^2$ for every orthonormal basis.
3. Corollary 6.11: the Hilbert–Schmidt operators form a $*$-ideal, with $\|KA\|_2, \|AK\|_2 \le \|A\|\|K\|_2$.
4. Lemma 6.12: $(\mathcal{J}_p(\mathfrak{H}), \|\cdot\|_p)$ is a Banach space, and

$$\|K\|_p = \sup\Big\{\Big(\sum_j|\langle\psi_j, K\varphi_j\rangle|^p\Big)^{1/p} \;\Big|\; \{\psi_j\}, \{\varphi_j\} \text{ orthonormal}\Big\}.$$

5. Lemma 6.13: $K$ is trace class iff $K = K_1K_2$ with $K_1, K_2$ Hilbert–Schmidt, and then $\|K\|_1 \le \|K_1\|_2\|K_2\|_2$.
6. Corollary 6.14: the trace class is a $*$-ideal, with $\|KA\|_1, \|AK\|_1 \le \|A\|\|K\|_1$.
7. Lemma 6.16 (after the goal): the trace is linear, $\operatorname{tr}(K^*) = \overline{\operatorname{tr}(K)}$, it is monotone for the operator order, and $\operatorname{tr}(AK) = \operatorname{tr}(KA)$ for bounded $A$.

Significance

The result itself. Lemma 6.15 is what turns the trace into a linear functional on $\mathcal{J}_1(\mathfrak{H})$ at all. Every later use of the trace rests on it: the normalization of density matrices, the duality $\mathcal{J}_1(\mathfrak{H})^* \cong \mathfrak{L}(\mathfrak{H})$, trace formulas and spectral shift functions, and Lidskii's theorem (the trace is the sum of the eigenvalues), which Teschl mentions right after the lemma. The ideal properties (Corollaries 6.11 and 6.14) and the factorization (Lemma 6.13) are the everyday tools for proving that a concrete operator, such as $f(x)g(-i\nabla)$ in Chapter 7, is trace class.

Formalizing it. Mathlib has compact operators (IsCompactOperator), Hilbert bases, singular values and the trace of linear maps on finite-dimensional spaces (LinearMap.singularValues, LinearMap.trace), but no infinite-dimensional singular values, Schatten classes, Hilbert–Schmidt or trace class operators, and no basis-independent trace. The Prove2Me corpus has finite-dimensional trace norms (matrices) and $L^2$ kernel operators, but no statement of this section. The results are classical and fully proved in the literature; the work is to formalize them.

Difficulty

The obvious argument for basis independence is to expand $K$ in both bases and interchange the two sums. In infinite dimensions that interchange is not justified for an arbitrary bounded $K$: for the identity on an infinite-dimensional space, or for a non-trace-class compact operator, the diagonal series diverges. The trace class hypothesis must therefore enter through a factorization, and the factorization rests on the canonical form of Theorem 6.7, which in turn needs the spectral theorem for the compact self-adjoint operator $K^*K$, including finite multiplicity of its nonzero eigenvalues. A second difficulty is bookkeeping: the singular values are a family with multiplicities that may be finite or countably infinite, and the Schatten norm, the Hilbert–Schmidt sums over a basis and the supremum formula (6.23) all have to be matched as sums in $[0,\infty]$.

Formalization scope

• Hilbert space. {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]. Separability is not assumed. Orthonormal bases are Mathlib HilbertBasis ι ℂ H with arbitrary index types, so every statement covers the book's separable case.
• Operators. Bounded operators are H →L[ℂ] H, products are compositions, adjoints are ContinuousLinearMap.adjoint, and the operator order in Lemma 6.16 is Mathlib's Loewner order ($K_1 \le K_2$ iff $K_2 - K_1$ is positive). Traces are compared with the partial order of $\mathbb{C}$.
• Compactness is the book's definition, membership in the norm closure of the finite rank operators, not Mathlib's IsCompactOperator.
• Singular values are not enumerated. $\sum_j s_j(K)^p$ is written as $\sum_{\mu > 0} \dim\operatorname{Ker}(K^*K - \mu)\,\mu^{p/2}$, with the dimension in $\{0,1,\dots\}\cup\{\infty\}$. Norms and sums live in $[0,\infty]$, so a divergent series is $\infty$, never a junk $0$. Hilbert–Schmidt and trace class are defined by $\|K\|_2 < \infty$ and $\|K\|_1 < \infty$ on compact $K$. The basis characterizations (Lemma 6.10) and the factorization (Lemma 6.13) are theorems, not definitions.
• Trace. trace K is $\sum_n\langle\varphi_n, K\varphi_n\rangle$ in one fixed, chosen Hilbert basis. The goal states summability in every Hilbert basis, not merely equality of tsum values. Since the tsum of a non-summable family is $0$ in Mathlib, a statement asserting only that all tsums agree would be trivially satisfiable by divergent series. That trivializing reading is ruled out.
• Lemma 6.12 assumes $1 \le p$ (the book's proof uses the conjugate exponent). "Banach space" is spelled out as closure under the linear operations, the norm axioms, and completeness of $\|\cdot\|_p$-Cauchy sequences.
• No projection-valued measure, no functional calculus and no Fourier transform is used, and nothing is taken as data.

Reusable infrastructure a complete development will produce includes the spectral theorem for compact self-adjoint operators with multiplicities, the singular value decomposition in infinite dimensions, and the Hilbert–Schmidt and trace class ideals. All of these are welcome as independent contributions, and any of them would fill gaps in Mathlib.

Selected references

• G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, AMS, 2009, Sections 6.2–6.3. https://doi.org/10.1090/gsm/099
• R. Schatten, Norm Ideals of Completely Continuous Operators, Ergebnisse der Mathematik und ihrer Grenzgebiete, Springer, 1960 (no stable link verified).
• B. Simon, Trace Ideals and Their Applications, 2nd ed., Mathematical Surveys and Monographs 120, AMS, 2005. https://doi.org/10.1090/surv/120
• M. Reed and B. Simon, Methods of Modern Mathematical Physics I: Functional Analysis, Academic Press, 1980, Section VI.6 (no stable link verified).