Prove2Me

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

Analysis

323 missions · 177 completed

Missions

Partial Differential Equations·Captain: wurtle

Global Uniqueness for the Smooth Isotropic Elasticity Inverse ProblemResearch Paper

Motivation

An isotropic elastic body is described by two spatially varying Lamé moduli: the shear modulus μ\mu and the parameter λ\lambda (the bulk modulus is λ+2μ/3\lambda+2\mu/3). The elastic inverse problem asks whether static boundary measurements, the boundary tractions produced by all prescribed boundary displacements, determine both moduli inside the body. It is the elasticity analogue of Calderón's conductivity problem, with applications to elastography and nondestructive testing, and it is harder because two coefficients are coupled through a vector-valued system rather than a scalar equation.

Background

  • 1980, 1987. Calderón poses the scalar conductivity problem; Sylvester and Uhlmann prove uniqueness for smooth conductivities in dimension n≥3n\ge3 using complex geometric optics (doi:10.2307/1971291).
  • 1995. Nakamura and Uhlmann recover the boundary Taylor series of the Lamé moduli (doi:10.1137/S0036141093247494).
  • 2002–2003. Eskin and Ralston develop matrix complex geometric optics with planar transport frames and prove restricted uniqueness results (doi:10.1088/0266-5611/18/3/324).
  • 2003. Nakamura and Uhlmann's erratum corrects their earlier global claim, proving uniqueness only when ∇μ\nabla\mu is small in CmC^m (doi:10.1007/s00222-002-0276-1).
  • 2015. Imanuvilov and Yamamoto prove global uniqueness in two dimensions (doi:10.1088/0266-5611/31/3/035004).
  • 2017, 2023. Lin and Nakamura reconstruct boundary values at finite regularity (doi:10.1088/1361-6420/aa942d); Tan and Liu treat boundary jets on manifolds and analytic global recovery (doi:10.1088/1361-6420/ace649).

Without smallness, analyticity or symmetry hypotheses, three-dimensional global uniqueness was not established. The source of this mission is an OpenAI preprint dated September 24, 2026, which claims it for all smooth moduli satisfying the energy-positivity conditions.

Setting

Let Ω⊂R3\Omega\subset\mathbb R^3 be a bounded connected domain with C∞C^\infty boundary, and let λ,μ∈C∞(Ω‾)\lambda,\mu\in C^\infty(\overline\Omega) satisfy

μ>0,3λ+2μ>0on Ω‾.\mu>0,\qquad 3\lambda+2\mu>0\qquad\text{on }\overline\Omega.

For a displacement u:Ω→R3u:\Omega\to\mathbb R^3, the strain is e(u)=12(∇u+∇uT)e(u)=\tfrac12(\nabla u+\nabla u^{T}), the stress σ(u)=λ(div⁡u)I+2μ e(u)\sigma(u)=\lambda(\operatorname{div}u)I+2\mu\,e(u), and the elasticity system is div⁡σ(u)=0\operatorname{div}\sigma(u)=0. For boundary data f∈H1/2(∂Ω;R3)f\in H^{1/2}(\partial\Omega;\mathbb R^3) let uf∈H1(Ω;R3)u_f\in H^1(\Omega;\mathbb R^3) be the unique weak solution with trace ff. The displacement-to-traction map is

⟨Λλ,μf,g⟩=∫Ω[λ (div⁡uf)(div⁡vg)+2μ e(uf):e(vg)] dx,Tr⁡vg=g.\langle\Lambda_{\lambda,\mu}f,g\rangle=\int_\Omega\bigl[\lambda\,(\operatorname{div}u_f)(\operatorname{div}v_g)+2\mu\,e(u_f):e(v_g)\bigr]\,dx,\qquad \operatorname{Tr}v_g=g.

Formalization targets

Goal: Theorem 1.1

For admissible pairs (λ1,μ1)(\lambda_1,\mu_1), (λ2,μ2)(\lambda_2,\mu_2) on Ω\Omega,

Λλ1,μ1=Λλ2,μ2 ⟹ λ1=λ2 and μ1=μ2 in Ω.\Lambda_{\lambda_1,\mu_1}=\Lambda_{\lambda_2,\mu_2}\ \Longrightarrow\ \lambda_1=\lambda_2\ \text{and}\ \mu_1=\mu_2\ \text{in }\Omega.

The Lean statement OAI.Elasticity.global_uniqueness is open on the platform.

Significance

The theorem settles the smooth three-dimensional isotropic elastic Calderón uniqueness question under the natural energy-positivity assumptions, with no analyticity, no closeness to constants, and no prior agreement near the boundary. It identifies both moduli from the full zero-frequency boundary operator. It does not give a reconstruction algorithm or stability estimates, which remain natural follow-up questions.

The result is stated in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.

Difficulty

The scalar complex-geometric-optics method does not apply directly to the Lamé system. Earlier reductions to auxiliary systems ran into two problems documented in the Nakamura–Uhlmann erratum: the planar matrix transport equation with prescribed initial data need not be solvable, and the corrected solutions lead to a pseudodifferential rather than a differential identity. The Eskin–Ralston reduction from auxiliary fields to physical displacements is not injective, so equality of physical boundary maps does not by itself give equality of auxiliary Cauchy data. A proof must work with exact physical solutions and keep track of their actual divergences.

Formalization scope

  • Domain Ω: open, connected, bounded, with smooth boundary given by local C∞C^\infty diffeomorphisms of R3\mathbb R^3 flattening ∂Ω\partial\Omega.
  • Admissible Ω λ μ: both moduli smooth on an open neighbourhood of Ω‾\overline\Omega, with μ>0\mu>0 and 3λ+2μ>03\lambda+2\mu>0 on Ω‾\overline\Omega.
  • H1(Ω;R3)H^1(\Omega;\mathbb R^3) is the closure of jets (f,∂1f,∂2f,∂3f)(f,\partial_1f,\partial_2f,\partial_3f) of smooth ff in L2L^2; boundary data are H1H^1 modulo the closure of compactly supported smooth jets.
  • DN Ω λ μ f g is the energy pairing of a weak solution with trace ff against any representative of gg; the goal assumes equality of these two-variable functions and concludes pointwise equality of the moduli on Ω\Omega.

A complete development needs vector-valued Sobolev spaces, Korn's inequality, the weak Dirichlet problem for the Lamé system, Carleman estimates and complex geometric optics for elliptic systems. These tools are reusable for other inverse problems. Contributions formalizing Lemma 2.1 (common exterior extension), Proposition 2.2 (transfer of physical solutions) and Proposition 3.2 (supported Carleman estimate) are welcome.

Selected references

2 thms1 active userReviewed
Partial Differential Equations·Captain: wurtle

Strict hot spots and absence of interior critical points on smooth simply connected planar domainsResearch Paper

Motivation

Heat in an insulated planar plate evolves by the heat equation with Neumann boundary condition. For generic initial temperature, after a long time the temperature minus its average is dominated by an eigenfunction of the first positive Neumann eigenvalue. Rauch asked in 1974 where the hottest and coldest points of the plate end up, and conjectured that they move to the boundary (Rauch 1975). In spectral form, the hot spots conjecture asks whether a first nonconstant Neumann eigenfunction attains its maximum and minimum only on the boundary. The question links spectral geometry, reflected Brownian motion and elliptic PDE, and it is known to depend on topology: it fails for some domains with holes.

This mission asks for a machine-checked proof of the strict form of the conjecture for all smooth bounded simply connected planar domains, as claimed in an OpenAI preprint dated September 24, 2026 (source): every nonzero first-positive Neumann eigenfunction has no interior critical point at all. The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal below is open.

Timeline

  • 1975 — Rauch poses the problem in lectures on qualitative PDE theory (Rauch 1975).
  • 1999 — Bañuelos and Burdzy distinguish strict and nonstrict formulations and prove cases by coupling of reflected Brownian motions (J. Funct. Anal. 1999). Burdzy and Werner construct a counterexample with two holes (Ann. of Math. 1999).
  • 2000 — Jerison and Nadirashvili prove the conjecture for convex planar domains with two axes of symmetry (JAMS 2000); Bass and Burdzy find examples with both extrema in the interior (Duke 2000).
  • 2002–2004 — Pascu treats convex domains with one symmetry (Trans. AMS 2002); Atar and Burdzy treat lip domains (JAMS 2004).
  • 2005 — Burdzy obtains a counterexample with a single hole and states the simply connected planar conjecture explicitly (Duke 2005, Conjecture 1.2(ii)).
  • 2007 — Miyamoto handles nearly circular convex domains under a spectral-diameter condition.
  • 2015–2022 — Siudeja proves the conjecture for a class of acute triangles (Math. Z. 2015); Judge and Mondal exclude interior critical points on every triangle (Ann. of Math. 2020, erratum 2022).
  • 2021–2024 — Rohleder introduces a variational principle for tangent vector fields (arXiv:2106.05224; 2024), the starting point of the preprint.
  • 2025–2026 — Sharp bounds on the failure of the conjecture (de Dios Pont–Hsu–Taylor, 2025); classification of critical points on triangles (Chen–Gui–Yao, Invent. Math. 2026).
  • September 2026 — The OpenAI preprint claims the strict conjecture for all smooth bounded simply connected planar domains (Theorem 1.1, p. 1).

Setting

Let Ω⊂R2\Omega\subset\mathbb R^2 be a nonempty bounded open simply connected set with C∞C^\infty boundary. The first positive Neumann eigenvalue is

μ=μ1(Ω)=inf⁡{∫Ω∣∇v∣2∫Ωv2:v∈H1(Ω), ∫Ωv=0, v≠0},\mu=\mu_1(\Omega)=\inf\Bigl\{\frac{\int_\Omega|\nabla v|^2}{\int_\Omega v^2}: v\in H^1(\Omega),\ \int_\Omega v=0,\ v\ne0\Bigr\},

counting only positive eigenvalues (many sources call it μ2\mu_2). The first positive Neumann eigenspace VV consists of the u∈H1(Ω)u\in H^1(\Omega) with ∫Ωu=0\int_\Omega u=0 and

∫Ω∇u⋅∇v=μ∫Ωuvfor all v∈H1(Ω).\int_\Omega\nabla u\cdot\nabla v=\mu\int_\Omega uv\qquad\text{for all }v\in H^1(\Omega).

This weak formulation encodes −Δu=μu-\Delta u=\mu u in Ω\Omega with ∂νu=0\partial_\nu u=0 on ∂Ω\partial\Omega. Eigenspace functions are smooth up to the boundary.

Formalization targets

Goal: Theorem 1.1 (p. 1)

For every nonzero u∈Vu\in V,

∇u(x)≠0(x∈Ω),andmin⁡∂Ωu<u(x)<max⁡∂Ωu(x∈Ω).\nabla u(x)\ne0\quad(x\in\Omega),\qquad\text{and}\qquad \min_{\partial\Omega}u<u(x)<\max_{\partial\Omega}u\quad(x\in\Omega).

This holds for every member of the eigenspace, also when μ\mu is a multiple eigenvalue. In Lean this is OAI.StrictHotSpots.main_theorem.

Significance

The result itself. It resolves Burdzy's simply connected planar hot spots conjecture in its strongest form: not only do the extrema lie on the boundary, but there are no interior saddle points either, for every eigenfunction in the eigenspace. Combined with the Burdzy–Werner and Burdzy one-hole counterexamples, it shows that simple connectivity is exactly the dividing line among smooth planar domains. The intermediate kernel theorem (Theorem 5.1, p. 12), a conditional negativity statement for reciprocal Green kernels of the disk, is stated independently of the eigenfunction problem.

Formalizing it. A complete development needs Sobolev spaces on smooth planar domains, the Riemann mapping theorem with boundary regularity, Neumann elliptic regularity, and the theory of conditionally negative definite kernels. Each is reusable. No machine-checked proof of any hot spots result, including the triangle case, is known to exist.

Difficulty

Each Cartesian derivative of an eigenfunction solves the same Helmholtz equation, but its boundary values have no fixed sign, so a maximum-principle argument on one directional derivative fails on a general domain with no preferred direction. Coupling methods need convexity or symmetry. The preprint instead uses the Neumann condition jointly on both derivatives (the gradient is tangent to the boundary), via a nonnegative quadratic form whose null space consists exactly of eigenfunction gradients (Proposition 3.1, p. 7). The central difficulty is to build enough scalar boundary multipliers preserving that null space; this requires proving that a reciprocal kernel K(p,s)K(p,t)/N(s,t)K(p,s)K(p,t)/N(s,t) is conditionally negative semidefinite (Theorem 5.1, p. 12), through regularized Green kernels, a complete Nevanlinna–Pick-type matrix property, and a boundary limit.

Formalization scope

  • Ω\Omega is a subset of EuclideanSpace ℝ (Fin 2): nonempty, open, bounded, IsSimplyConnected (which includes path-connectedness), with a smooth local defining function ρ\rho with nonzero derivative at every boundary point.
  • H1H^1 is encoded by HasH1Gradient Ω v g: v,g∈L2(Ω)v,g\in L^2(\Omega) and gg is the weak gradient of vv against smooth test functions compactly supported in Ω\Omega. μ\mu is the sInf of Rayleigh quotients over mean-zero nonzero H1H^1 functions; this set is nonempty and bounded below by 00.
  • InFirstNeumannEigenspace Ω u requires u∈C∞(Ω‾)u\in C^\infty(\overline\Omega), mean zero, and the weak eigen-equation for all H1H^1 test pairs. The smoothness-up-to-the-boundary clause is a standard regularity fact for Neumann eigenfunctions on smooth domains (the preprint cites Showalter for it), so it does not exclude any eigenfunction.
  • The hypothesis u≠0u\ne0 is pointwise somewhere in Ω\Omega. The conclusion uses sInf/sSup of uu on frontier Ω, which is compact and nonempty, so these are the true minimum and maximum.
  • A vacuous reading is excluded: the eigenspace is nontrivial on every such domain (Rellich compactness), so the goal is a genuine statement about actual eigenfunctions.

Selected references

2 thms1 active userReviewed
Partial Differential Equations·Captain: wurtle

Nonuniqueness for bounded measurable scalar conductivities in three dimensionsResearch Paper

Motivation

Calderón's inverse conductivity problem asks whether the electrical conductivity inside a body is determined by voltage and current measurements on its boundary. Mathematically, a conductivity γ\gamma on a domain Ω\Omega defines the elliptic equation div⁡(γ∇u)=0\operatorname{div}(\gamma\nabla u)=0, and the boundary data are encoded by the Dirichlet-to-Neumann (DN) operator Λγ\Lambda_\gamma, which maps a boundary voltage to the resulting boundary current. The problem underlies electrical impedance tomography and is the model case of a large family of inverse boundary-value problems. Calderón (1980) posed it for bounded measurable conductivities bounded away from zero; how much regularity uniqueness requires has been a central question since.

Background

  • 1974. Miller constructs elliptic divergence-form equations with nonunique continuation (doi:10.1007/BF00247634).
  • 1980. Calderón poses the problem and proves injectivity of the linearization at constant conductivities.
  • 1987. Sylvester and Uhlmann prove uniqueness for smooth conductivities in dimension n≥3n\ge3 (doi:10.2307/1971291).
  • 2006. Astala and Päivärinta prove uniqueness for bounded measurable conductivities in the plane (doi:10.4007/annals.2006.163.265).
  • 2015–2016. Haberman proves uniqueness for W1,nW^{1,n} conductivities in dimensions three and four (doi:10.1007/s00220-015-2460-3); Caro and Rogers prove it for Lipschitz conductivities in all dimensions n≥3n\ge3 (doi:10.1017/fmp.2015.9).
  • 2020. Daudé, Kamran and Nicoleau give anisotropic (matrix-valued) counterexamples with partial data, via nonunique continuation (doi:10.1017/fms.2020.1).

In dimension n≥3n\ge3, uniqueness for merely bounded measurable scalar conductivities remained unresolved. The source of this mission is an OpenAI preprint dated September 23, 2026, which constructs a counterexample in dimension three.

Setting

Let Ω=B(0,3)⊂R3\Omega=B(0,3)\subset\mathbb R^3. A conductivity is a measurable γ:Ω→R\gamma:\Omega\to\mathbb R with 0<c≤γ≤C0<c\le\gamma\le C almost everywhere. Let H1(Ω)H^1(\Omega) be the Sobolev space, H01(Ω)H^1_0(\Omega) the closure of compactly supported smooth functions, and H1/2(∂Ω)≅H1(Ω)/H01(Ω)H^{1/2}(\partial\Omega)\cong H^1(\Omega)/H^1_0(\Omega) the trace space, with dual H−1/2(∂Ω)H^{-1/2}(\partial\Omega). For a trace ff, let uf∈H1(Ω)u_f\in H^1(\Omega) be the unique function with trace ff such that

∫Ωγ ∇uf⋅∇φ dx=0(φ∈H01(Ω)).\int_\Omega\gamma\,\nabla u_f\cdot\nabla\varphi\,dx=0\qquad(\varphi\in H^1_0(\Omega)).

The DN operator Λγ:H1/2(∂Ω)→H−1/2(∂Ω)\Lambda_\gamma:H^{1/2}(\partial\Omega)\to H^{-1/2}(\partial\Omega) is

⟨Λγf,g⟩=∫Ωγ ∇uf⋅∇v dx,Tr⁡v=g.\langle\Lambda_\gamma f,g\rangle=\int_\Omega\gamma\,\nabla u_f\cdot\nabla v\,dx,\qquad \operatorname{Tr}v=g.

Formalization targets

Goal: Theorem 1.1

There are γ0,γ1∈L∞(B(0,3))\gamma_0,\gamma_1\in L^\infty(B(0,3)) and 0<c<C0<c<C with

c≤γj≤C a.e.,γj=1 near ∂B(0,3),∣{γ0≠γ1}∣>0,Λγ0=Λγ1.c\le\gamma_j\le C\ \text{a.e.},\qquad \gamma_j=1\ \text{near }\partial B(0,3),\qquad |\{\gamma_0\ne\gamma_1\}|>0,\qquad \Lambda_{\gamma_0}=\Lambda_{\gamma_1}.

The Lean statement OAI.ScalarConductivity.main_nonuniqueness is open on the platform.

Significance

The theorem shows that scalar Calderón uniqueness fails in the bounded measurable class in dimension three, in contrast with the planar theorem of Astala–Päivärinta and the Lipschitz and W1,nW^{1,n} uniqueness results in higher dimensions. It locates the regularity threshold for uniqueness strictly between L∞L^\infty and the known positive classes. By Corollary 1.2, counterexamples can be localized: any finite family of disjoint balls inside any Lipschitz domain supports 2m2^m distinct conductivities with the same DN map.

The result is stated in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.

Difficulty

Matrix-valued counterexamples exist, but they do not transfer to scalar conductivities: scalar coefficients can approximate matrix ones only in the sense of GG- or HH-convergence, and Rondi's example shows that exact realization of a full boundary map by a scalar coefficient can fail. Moreover, Daudé–Kamran–Nicoleau note an obstruction for full-boundary data: a weakly harmonic factor with constant full boundary trace is constant. One must therefore match the entire DN operator (every boundary input) exactly, with a scalar coefficient, and with uniform ellipticity bounds; the paper does so with a nested family of scalar blocks realizing prescribed current triples exactly.

Formalization scope

  • H1(B(0,3))H^1(B(0,3)) is the closure, in L2(B;R4)L^2(B;\mathbb R^4), of the jets (f,∇f)(f,\nabla f) of smooth ff; H01H^1_0 is the closure of jets of smooth ff with compact support in the ball; the trace space is the quotient and the DN operator is a continuous linear map into its continuous dual.
  • IsDirichletToNeumann γ Λ requires existence and uniqueness of the weak γ\gamma-harmonic extension of every trace and the weak flux identity against every v∈H1v\in H^1.
  • EqualOneNearBoundary asks for r<3r<3 with γ=1\gamma=1 a.e. on {r<∣x∣<3}\{r<|x|<3\}; bounds and measurability are stated almost everywhere on the ball.

A complete development needs Sobolev spaces on a ball, weak solutions of divergence-form equations (Lax–Milgram), trace spaces, and the paper's block constructions (convex-integration-type scalarization). Contributions formalizing Theorem 3.1 (exact finite-field scalarization), Proposition 4.1 (branching block) and Corollary 1.2 are welcome.

Selected references

2 thms1 active userReviewed
Differential GeometryOptimal Transport·Captain: wurtle

Weak Hessian bounds along every geodesic in RCD spacesResearch Paper

Motivation: from weak Hessian bounds to every geodesic

On a smooth Riemannian manifold, an upper bound ∇2F≤G g\nabla^2F\le G\,g on the Hessian of a function FF immediately bounds the second derivative of FF along every geodesic: (F∘σ)′′≤∣σ˙∣2 G∘σ(F\circ\sigma)''\le|\dot\sigma|^2\,G\circ\sigma. In non-smooth geometry this step breaks down. On metric measure spaces with Ricci curvature bounded below in the synthetic sense — the RCD(K,N)\mathrm{RCD}(K,N) spaces — Hessians exist only weakly: inequalities are tested against the reference measure mm, whereas a single prescribed geodesic can lie in a set of measure zero. Passing from a distributional Hessian bound to a statement about every individual geodesic is a recurring need, for example in characterizing lower bounds on sectional curvature synthetically (in the same release the preprint accompanies an OpenAI preprint on Gigli's distributional-curvature characterization of Alexandrov spaces). Earlier results get this passage only under extra regularity.

Timeline

  • 2014 — Savaré's self-improvement of the Bakry–Émery condition gives a measure-valued Bochner calculus on RCD(K,∞)\mathrm{RCD}(K,\infty) spaces (Savaré 2014).
  • 2015 — Ambrosio, Gigli and Savaré identify Bakry–Émery bounds with Riemannian curvature-dimension bounds (Ann. Probab. 2015). Ketterer uses an exponential change of measure under a Hessian assumption with Sobolev regularity (Ketterer 2015, Thm 7.1).
  • 2018 — Gigli's second-order calculus on RCD\mathrm{RCD} spaces: Hessians of test functions and ∇∇g∇g=∇(Γ(g)/2)\nabla_{\nabla g}\nabla g=\nabla(\Gamma(g)/2) (Gigli, Mem. AMS 2018). Han passes from infinitesimal to weak convexity by entropy convexity for e−aume^{-au}m, assuming second-order Sobolev regularity (Han 2018); Sturm treats semiconvex functions by vanishing entropy (Sturm 2018).
  • 2020 — Kapovitch and Ketterer derive geodesic convexity from an L2L^2-Hessian bound for Laplacian-domain functions (J. reine angew. Math. 2020, Thm 4.7).
  • 2021 — Braun, Habermann and Sturm develop variable-curvature equivalences (J. Math. Pures Appl. 2021).
  • 2024–2025 — Brena and Gigli discuss the passage from weak Hessian bounds to geodesic convexity and propose a change-of-measure route, identifying the regularity it needs (Potential Anal. 2025, Remarks 2.3–2.4). Deng proves that finite-dimensional RCD(K,N)\mathrm{RCD}(K,N) spaces are non-branching (Geom. Topol. 2025, Thm 1.3).
  • 2026 — An OpenAI preprint, Weak Hessian bounds along every geodesic in RCD spaces (OpenAI Math Release, September 24, 2026), claims the passage under only bounded Lipschitz regularity of FF and bounded continuous GG. It has not been peer reviewed, and the claim has not been formally verified.

Setting

(M,d,m)(M,d,m) is a complete separable metric space with a Borel measure mm that charges every nonempty open set and is finite on bounded sets. RCD(K,N)\mathrm{RCD}(K,N), for K∈RK\in\mathbb R and 1<N<∞1<N<\infty, means the (unreduced) Lott–Sturm–Villani curvature-dimension condition CD(K,N)\mathrm{CD}(K,N) for optimal transport between absolutely continuous probability measures with finite second moment, together with a quadratic Cheeger energy (infinitesimal Hilbertianity).

The minimal weak upper gradient ∣∇f∣|\nabla f| is defined through test plans (probability measures on absolutely continuous curves with bounded compression and finite kinetic energy). Polarization gives Γ(u,v)=⟨∇u,∇v⟩\Gamma(u,v)=\langle\nabla u,\nabla v\rangle, and the Laplacian is the nonpositive generator, ∫Γ(u,v) dm=−∫(Δu)v dm\int\Gamma(u,v)\,dm=-\int(\Delta u)v\,dm. The test class consists of bounded, globally Lipschitz gg in the domain of Δ\Delta with Δg∈W1,2\Delta g\in W^{1,2}. For such compactly supported gg and nonnegative compactly supported Lipschitz hh, the weak Hessian evaluation of FF is

HF(∇g,∇g)(h)=−∫M(Γ(h,g)+h Δg) Γ(F,g) dm−∫Mh Γ ⁣(F,12Γ(g)) dm.H_F(\nabla g,\nabla g)(h)= -\int_M\big(\Gamma(h,g)+h\,\Delta g\big)\,\Gamma(F,g)\,dm-\int_M h\,\Gamma\!\big(F,\tfrac12\Gamma(g)\big)\,dm .

A constant-speed minimizing geodesic is a curve σ:[0,1]→M\sigma:[0,1]\to M with d(σs,σt)=∣s−t∣ ℓd(\sigma_s,\sigma_t)=|s-t|\,\ell, where ℓ=d(σ0,σ1)\ell=d(\sigma_0,\sigma_1). All of these notions are defined from scratch in the Lean development (IsTestPlan, weakGradient, gamma, IsLaplacian, IsTestFunction, weakHessian, CurvatureDimension, RCD).

Formalization targets

Goal: weak Hessian bounds along every geodesic (Theorem 1.1)

Let (M,d,m)(M,d,m) be a full-support RCD(K,N)\mathrm{RCD}(K,N) space with 1<N<∞1<N<\infty. Let FF be bounded and globally Lipschitz and GG bounded and continuous, and assume

HF(∇g,∇g)(h)≤∫Mh G Γ(g) dmH_F(\nabla g,\nabla g)(h)\le\int_M h\,G\,\Gamma(g)\,dm

for all compactly supported test functions gg and all nonnegative h∈Lipc(M)h\in\mathrm{Lip}_c(M). Then every constant-speed minimizing geodesic σ\sigma of length ℓ\ell satisfies (F∘σ)′′≤ℓ2 G∘σ(F\circ\sigma)''\le\ell^2\,G\circ\sigma in distributions on (0,1)(0,1):

∫01F(σt) φ′′(t) dt≤ℓ2∫01G(σt) φ(t) dtfor all 0≤φ∈Cc∞(0,1).\int_0^1F(\sigma_t)\,\varphi''(t)\,dt\le\ell^2\int_0^1G(\sigma_t)\,\varphi(t)\,dt\qquad\text{for all } 0\le\varphi\in C_c^\infty(0,1).

The goal is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. If the source's proof is correct, the theorem makes a measure-theoretic Hessian inequality usable on every prescribed geodesic, including geodesics that are invisible to almost-everywhere statements. For constant G=cG=c it says that t↦F(σt)−cℓ2t2/2t\mapsto F(\sigma_t)-c\ell^2t^2/2 is concave on every geodesic. Compared with earlier results, FF needs only to be bounded and Lipschitz (no second-order Sobolev or Laplacian-domain regularity), GG may vary in space, and mm may have infinite total mass. Such geodesic convexity statements feed into synthetic characterizations of sectional-curvature lower bounds and into rigidity arguments on RCD\mathrm{RCD} spaces.

Formalizing it. The statement depends on a large definitional layer: test plans, weak upper gradients, Cheeger energy, the Laplacian, Lott–Sturm–Villani CD(K,N)\mathrm{CD}(K,N) and the weak Hessian. None of these is in Mathlib. Formalizing them faithfully is reusable infrastructure for the whole theory of metric measure spaces with Ricci bounds. The proof itself relies on deep inputs (Savaré's self-improvement, the Ambrosio–Gigli–Savaré and Braun–Habermann–Sturm equivalences, Deng's non-branching theorem), so the realistic path is to state those inputs as milestones.

Difficulty

A weak Hessian bound holds only after integration against mm. A naive argument would average the bound over a family of geodesics and then localize, but a fixed geodesic can carry zero measure, and almost-everywhere statements about transport geodesics say nothing about it. The natural fix — change the measure to eλFme^{\lambda F}m and use entropy convexity — requires the weighted Bochner inequality on the weighted test class. A Lipschitz weight does not preserve that class: the drift term Γ(V,u)\Gamma(V,u) need not be Sobolev, as an explicit Euclidean example in the source shows (Remark 4.2). Localizing to one geodesic also needs uniqueness of geodesics between nearby endpoints, which in this generality comes from non-branching of finite-dimensional RCD\mathrm{RCD} spaces.

Formalization scope

  • XX is a MetricSpace with Borel σ-algebra, CompleteSpace and SeparableSpace; mm is a Measure X with FullSupport and FiniteOnBoundedSets. RCD m K N is the unreduced CurvatureDimension with the τ\tau coefficients for all N′≥NN'\ge N, plus QuadraticCheegerEnergy (the parallelogram law for Cheeger energy).
  • IsTestFunction requires the function itself (not merely a representative) to be bounded and globally Lipschitz, in the Laplacian domain, with Sobolev Laplacian. WeakHessianUpperBound m F G quantifies over compactly supported test functions gg and compactly supported nonnegative Lipschitz hh.
  • Geodesics are continuous maps Set.Icc 0 1 → X with d(σs,σt)=∣s−t∣ d(σ0,σ1)d(\sigma_s,\sigma_t)=|s-t|\,d(\sigma_0,\sigma_1), so constant curves are included (the conclusion is then trivial). The conclusion CurveSecondDerivativeBound integrates over [0,1][0,1] against smooth nonnegative φ\varphi with tsupport φ ⊆ Ioo 0 1.
  • Choice-based definitions (weakGradient, laplacian) return 00 when the object does not exist. The hypotheses on FF (bounded Lipschitz) and the test-function requirements ensure that the relevant gradients and Laplacians exist, so the hypothesis is not vacuous.
  • Contributions welcome: a faithful library of test plans, minimal weak upper gradients and the Laplacian on metric measure spaces; the Lott–Sturm–Villani CD(K,N)\mathrm{CD}(K,N) condition; entropy and Wasserstein geodesics.

Selected references

2 thms1 active userReviewed
Differential GeometryPartial Differential Equations·Captain: wurtle

Smooth counterexamples to Yau's nodal upper bound in dimensions three and fourResearch Paper

Motivation

The nodal set of a Laplace eigenfunction is the set where it vanishes. In 1982 Yau asked whether, on a fixed smooth closed Riemannian manifold of dimension dd, the (d−1)(d-1)-dimensional measure of the nodal set of every eigenfunction with eigenvalue λ\lambda is comparable to λ\sqrt\lambda from above and below (Yau, Problem section, Annals of Math. Studies 102, 1982). The conjectured two-sided bound

cgλ≤Hgd−1(Zu)≤Cgλ,c_g\sqrt\lambda\le\mathcal H^{d-1}_g(Z_u)\le C_g\sqrt\lambda,

with constants depending only on the metric, has organized several decades of work on unique continuation and quantitative zero sets of elliptic equations. The lower and upper inequalities are logically separate, and a fixed metric must be distinguished from a metric chosen anew for each eigenvalue.

Timeline

After Logunov, the smooth upper bound was known to be polynomial in λ\lambda but not of order λ\sqrt\lambda. The source of this mission, an OpenAI preprint dated September 23, 2026, claims that the upper bound fails for fixed smooth metrics in dimensions three and four.

Setting

Let (M,g)(M,g) be a closed connected smooth Riemannian manifold of dimension dd. In local coordinates, with ∣g∣=det⁡(gij)|g|=\det(g_{ij}) and (gij)(g^{ij}) the inverse matrix, the Laplace–Beltrami operator is Δgu=∣g∣−1/2∂i(∣g∣1/2gij∂ju)\Delta_g u=|g|^{-1/2}\partial_i(|g|^{1/2}g^{ij}\partial_j u). An eigenfunction with eigenvalue λ>0\lambda>0 is a nonzero real uu with −Δgu=λu-\Delta_g u=\lambda u; its nodal set is Zu={u=0}Z_u=\{u=0\}, measured by Hgd−1\mathcal H^{d-1}_g, Hausdorff measure for the Riemannian distance of gg.

The round metric g∗g_* on S3⊂R4S^3\subset\mathbb R^4 is the pullback of the Euclidean inner product. A C∞C^\infty neighborhood of g∗g_* is any set of metrics containing all gg whose coefficient functions, in finitely many charts and on compact subsets, have derivatives up to some order within ε\varepsilon of those of g∗g_*.

Formalization targets

Goal: Theorem 1.1 (three-sphere)

For every C∞C^\infty neighborhood N\mathcal N of g∗g_* there are g∞∈Ng_\infty\in\mathcal N, nonzero smooth uju_j and λj>0\lambda_j>0 with

−Δg∞uj=λjuj,λj→∞,Hg∞2(Zuj)λj→∞.-\Delta_{g_\infty}u_j=\lambda_ju_j,\qquad \lambda_j\to\infty,\qquad \frac{\mathcal H^2_{g_\infty}(Z_{u_j})}{\sqrt{\lambda_j}}\to\infty.

Lean: OAI.YauCounterexamples.sphere_three, open on the platform.

Milestone: Theorem 1.2 (four-manifold)

There are a smooth metric g∞g_\infty on S2×T2S^2\times\mathbb T^2, nonzero smooth uju_j and λj→∞\lambda_j\to\infty with −Δg∞uj=λjuj-\Delta_{g_\infty}u_j=\lambda_ju_j and Hg∞3(Zuj)/λj→∞\mathcal H^3_{g_\infty}(Z_{u_j})/\sqrt{\lambda_j}\to\infty.

Significance

Theorem 1.1 disproves the upper-bound half of Yau's conjecture for smooth metrics already in dimension three, with metrics arbitrarily close to the round sphere, where the bound does hold. Neither theorem asserts a power-law excess, and neither contradicts the lower bound. Together with the companion preprints of this family (a sharp λ\sqrt\lambda upper bound on smooth surfaces, and power-law violations in dimension at least five) it would locate the boundary of validity of the upper bound by dimension. The result is claimed in an OpenAI preprint that has not been peer reviewed, and no machine-checked proof exists.

Difficulty

Approximate eigenfunctions (quasimodes) with large nodal sets are comparatively easy to build locally. The obstacle is to replace each quasimode by an exact eigenfunction of an ordinary Laplace–Beltrami operator of one fixed metric, while keeping every sign change that witnesses nodal measure, and to do this for infinitely many eigenvalues at once with corrections that converge in C∞C^\infty. A scalar potential or conductivity correction would be easy, but the operator must be a genuine metric Laplacian, which imposes a determinant identity between conductivity and density; the paper uses different, dimension-specific repairs in dimensions three and four. Also, the nodal set is not assumed regular, so its measure must be bounded below by a stable, lower semicontinuous count of sign changes.

Formalization scope

  • SmoothMetric E M is Mathlib's ContMDiffRiemannianMetric on the tangent bundle. Sphere 3 is the unit sphere of EuclideanSpace ℝ (Fin 4) with its standard charts; the four-manifold is Sphere 2 × (Circle × Circle).
  • laplaceBeltrami g u x is the coordinate formula above, in the chart at x with coordinates from Module.finBasis; only values in the open chart target are used.
  • IsSmoothNeighborhood g₀ N: some finite list of compact-chart derivative tests and one ε>0\varepsilon>0 such that every metric passing them lies in N. Quantifying over all such N is the C∞C^\infty topology.
  • nodalMeasure g d u is Measure.hausdorffMeasure d of {u=0}\{u=0\} for the path distance of g itself (EMetricSpace.ofRiemannianMetric), not the distance inherited from R4\mathbb R^4.
  • HasUnboundedNodalRatio g d asks for smooth nonzero eigenfunctions with positive eigenvalues tending to ∞\infty, finite nodal measures, and ratio Hd−1/λ→∞\mathcal H^{d-1}/\sqrt\lambda\to\infty. Finiteness rules out the degenerate reading where an infinite measure would become 00 under toReal; it holds for every eigenfunction of a smooth metric on a compact manifold (Hardt–Simon).

A complete development needs elliptic regularity and perturbation theory for simple eigenvalues of metric Laplacians, WKB-type quasimode constructions, and Hausdorff-measure lower bounds from sign changes along segments. Contributions formalizing the named propositions (Proposition 2.6 spherical profiles, Proposition 3.6 simultaneous wave realization, Proposition 4.4 exactification, Proposition 6.2 one construction step) are welcome.

Selected references

3 thms1 active userReviewed
Differential GeometryPartial Differential Equations·Captain: wurtle

Sharp nodal length on smooth surfacesResearch Paper

Motivation

The nodal set of a Laplace eigenfunction is the set where it vanishes. On a vibrating membrane these are the curves that stay at rest (Chladni patterns), and in quantum mechanics they are the points where a stationary wave function has zero amplitude. A basic question is how large the nodal set is as the frequency grows. Yau conjectured in 1982 that on a smooth closed nn-dimensional Riemannian manifold the (n−1)(n-1)-dimensional measure of the nodal set of an eigenfunction with eigenvalue λ\lambda is comparable to λ\sqrt\lambda, from above and below, with constants depending only on the manifold (Yau, Problem section, Annals of Math. Studies 102, 1982). The question is a test case for unique continuation and quantitative control of the zeros of solutions to elliptic equations.

Timeline

The source of this mission, an OpenAI preprint dated September 23, 2026, claims the sharp upper bound CλC\sqrt\lambda on every smooth closed surface, which together with Brüning's lower bound would settle Yau's conjecture in dimension two.

Setting

Let (M,g)(M,g) be a closed (compact, without boundary) connected smooth Riemannian surface. In local coordinates write g=(gij)g=(g_{ij}), ∣g∣=det⁡(gij)|g|=\det(g_{ij}) and (gij)(g^{ij}) for the inverse matrix. The Laplace–Beltrami operator is

Δgu=∣g∣−1/2∑i,j∂i(∣g∣1/2gij∂ju).\Delta_g u=|g|^{-1/2}\sum_{i,j}\partial_i\bigl(|g|^{1/2}g^{ij}\partial_j u\bigr).

A Laplace eigenfunction with eigenvalue λ>0\lambda>0 is a nonzero real function uu with −Δgu=λu-\Delta_g u=\lambda u. Its nodal set is Zu={x∈M:u(x)=0}Z_u=\{x\in M: u(x)=0\}, and its nodal length is Hg1(Zu)\mathcal H^1_g(Z_u), the one-dimensional Hausdorff measure for the Riemannian distance dgd_g.

Formalization targets

Goal: Theorem 1.1

∃ C=C(M,g)<∞  ∀λ>0  ∀u≢0:−Δgu=λu ⟹ Hg1(Zu)≤Cλ.\exists\,C=C(M,g)<\infty\ \ \forall\lambda>0\ \ \forall u\not\equiv0:\quad -\Delta_g u=\lambda u\ \Longrightarrow\ \mathcal H^1_g(Z_u)\le C\sqrt\lambda.

The constant depends only on the surface and its metric and is the same for every eigenfunction in every positive eigenspace. The Lean statement OAI.SharpNodal.Main asserts MainStatement M; it is open on the platform.

Significance

The order λ\sqrt\lambda is optimal: Brüning's lower bound shows it cannot be improved, and on the round sphere spherical harmonics attain it. Before this work the best smooth-surface upper bound was Cλ3/4−βC\lambda^{3/4-\beta}. A sharp upper bound on every smooth surface, combined with the known lower bounds, would resolve Yau's conjecture for smooth closed surfaces; in dimensions three and higher the smooth upper bound remains a separate question (the companion missions in this family address it).

The theorem is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists. A formal proof would certify a long chain of quantitative estimates (Carleman inequalities, multiscale subdivision, packing), each of which is a natural target for reuse in other unique-continuation problems.

Difficulty

For a real-analytic metric, an eigenfunction extends holomorphically and its zeros can be counted by complex-analytic methods; this is how Donnelly and Fefferman obtain λ\sqrt\lambda. For a merely smooth metric no such extension exists. The standard route bounds nodal length on each wavelength-sized square by the local doubling exponent (growth of the L2L^2 norm from a disk to a larger disk). The known bounds on individual doubling exponents are too weak: a square can have growth much larger than average, and summing worst-case local bounds loses a power of λ\lambda. What is needed is control of the average growth over all wavelength-scale squares, while allowing large values on individual squares.

Formalization scope

  • The surface is a type M with [MetricSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 2)) M] [IsManifold 𝓘(ℝ, Plane) ∞ M], a smooth RiemannianBundle on the tangent bundle, and [IsRiemannianManifold 𝓘(ℝ,Plane) M], so the metric-space distance is the Riemannian distance. CompactSpace and ConnectedSpace encode closed and connected; the model space has no boundary.
  • laplaceBeltrami is the coordinate formula above, computed through chartAt with the metric matrix obtained from mfderiv of the inverse chart. No orientability is assumed.
  • Eigenfunctions are assumed ContMDiff … ∞ and nonzero, with −Δgu=λu-\Delta_g u=\lambda u at every point; smoothness is automatic by elliptic regularity, so this does not weaken the statement.
  • nodalLength u is Measure.hausdorffMeasure 1 of {u=0}\{u=0\} for the Borel structure of the metric, valued in ℝ≥0∞; the bound is ≤ ENNReal.ofReal (C * Real.sqrt lam) with C≥0C\ge0 fixed before λ\lambda and uu.

A complete development needs local isothermal coordinates or a coordinate-free substitute, Carleman estimates, L2L^2 growth bounds, and a planar comparison between growth and nodal length (Roy-Fortin's theorem). Much of this, especially Hausdorff-measure estimates for zero sets of solutions of planar elliptic equations, is reusable. Contributions formalizing the paper's intermediate results (Theorem 2.2, Proposition 3.4, Theorem 5.5, Lemma 6.2) or Roy-Fortin's planar theorem are welcome.

Selected references

2 thms1 active userReviewed
Functional Analysis·Captain: wurtle

Universal strong Kadison–Kastler stabilityResearch Paper

Motivation

How rigid is a von Neumann algebra inside B(H)B(H)? If two algebras M,N⊆B(H)M,N\subseteq B(H) have unit balls that are uniformly close, must they be the same algebra up to a small change of coordinates? Kadison and Kastler introduced the distance between the unit balls in 1972 (Amer. J. Math. 1972) and asked whether sufficiently close algebras are spatially isomorphic, implemented by a unitary close to the identity. The positive answer for a class of algebras is called (strong) Kadison–Kastler stability. The problem connects perturbation theory, Hochschild cohomology, and Kadison's similarity problem, and it was settled previously only for injective (amenable) algebras, type I algebras, and specific nonamenable examples.

This mission asks for a formal proof of the uniform strong Kadison–Kastler stability theorem stated in an OpenAI preprint dated September 23, 2026 (source): a single tolerance works for all von Neumann algebras on all Hilbert spaces. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

  • 1972 — Kadison and Kastler introduce the metric and prove stability results for type I algebras (Amer. J. Math. 1972).
  • 1974–1975 — Phillips proves spatial isomorphism for close type I algebras (Pacific J. Math. 1974); Christensen obtains a conjugating unitary near the identity (J. LMS 1975).
  • 1977 — Christensen (Invent. Math. 1977), Johnson (Proc. LMS 1977) and Raeburn–Taylor (JFA 1977) settle the injective case.
  • 1980 — Christensen's theory of near inclusions (Acta Math. 1980).
  • 1982 — Johnson's examples show that for C*-algebras the implementing unitary cannot always be chosen near the identity in a uniform way (Canad. Math. Bull. 1982).
  • 1983 — Haagerup's cyclic similarity estimate (Ann. of Math. 1983).
  • 2010–2012 — Christensen, Sinclair, Smith, White and Winter prove spatial isomorphism for close separable nuclear C*-algebras (PNAS 2010; Acta Math. 2012).
  • 2012–2014 — Cameron, Christensen, Sinclair, Smith, White and Wiggins construct the first nonamenable Kadison–Kastler stable factors, (L∞(X)⋊SLn(Z))⊗ˉR(L^\infty(X)\rtimes SL_n(\mathbb Z))\bar\otimes R for n≥3n\ge3 (PNAS 2012; Duke 2014).
  • September 2026 — The OpenAI preprint claims uniform stability for all von Neumann algebras (Theorem 1.1, p. 2).

Setting

Let HH be a complex Hilbert space and B(H)B(H) the bounded operators with the operator norm. A von Neumann algebra M⊆B(H)M\subseteq B(H) is a unital ∗*-subalgebra equal to its double commutant (in particular it contains the identity IHI_H). Write M1={x∈M:∥x∥≤1}M_1=\{x\in M:\|x\|\le1\} for its unit ball. The Kadison–Kastler distance is the Hausdorff distance of unit balls,

d(M,N)=max⁡(sup⁡x∈M1inf⁡y∈N1∥x−y∥, sup⁡y∈N1inf⁡x∈M1∥x−y∥).d(M,N)=\max\Bigl(\sup_{x\in M_1}\inf_{y\in N_1}\|x-y\|,\ \sup_{y\in N_1}\inf_{x\in M_1}\|x-y\|\Bigr).

A unitary u∈B(H)u\in B(H) conjugates MM to NN if uMu∗=NuMu^*=N.

Formalization targets

Goal: Theorem 1.1 (p. 2)

For every ε>0\varepsilon>0 there is δ>0\delta>0 such that for every complex Hilbert space HH and all von Neumann algebras M,N⊆B(H)M,N\subseteq B(H) with d(M,N)<δd(M,N)<\delta, there is a unitary u∈B(H)u\in B(H) with

uMu∗=Nand∥u−IH∥<ε.uMu^*=N\qquad\text{and}\qquad\|u-I_H\|<\varepsilon .

The tolerance δ\delta depends only on ε\varepsilon: not on the algebras, their type, their representations, or the size of HH.

Significance

The result itself. It answers the Kadison–Kastler perturbation question in its strongest uniform form for von Neumann algebras, including all nonamenable and type III cases and non-separable Hilbert spaces. Consequences include that every algebraic or analytic invariant preserved by unitary conjugacy (type, factoriality, property Γ\Gamma, Cartan subalgebras) is locally constant in the Kadison–Kastler metric. The analogous C*-algebra statement fails in its uniform-unitary form by Johnson's examples, so the theorem is specific to von Neumann algebras.

Formalizing it. The statement uses only Mathlib's VonNeumannAlgebra, unitary operators and Hausdorff distance, so it is fully expressible today. The proof, however, draws on free probability, tracial ultraproducts, Tomita–Takesaki theory, crossed products, Poisson boundaries and measurable cocycles, most of which are absent from Mathlib. Formalizing even the amenable (injective) case would be a substantial reusable contribution.

Difficulty

Closeness of unit balls supplies nearby elements but no linear or multiplicative correspondence between the algebras, and it gives no control at matrix levels, where perturbation arguments naturally live. For nonamenable algebras the classical route through vanishing Hochschild cohomology is unavailable. The preprint proceeds by cases. For finite factors it proves a uniform bound on all matrix amplifications of commutator maps (Theorem 3.1, p. 11) and corrects nearby unitaries to a measurable cocycle over an amenable boundary action (Section 4). Infinite factors require comparing modular groups through Tomita graphs (Proposition 6.5, p. 41) and aligning the modular action (Proposition 7.1, p. 45) before passing to crossed products (Theorem 8.4, p. 59). General algebras then require aligning centers and passing from separable to arbitrary Hilbert spaces (Section 9) without losing uniformity.

Formalization scope

  • HH ranges over complex Hilbert spaces (NormedAddCommGroup, InnerProductSpace ℂ, CompleteSpace) in a fixed universe u; δ\delta is chosen before HH, so the uniformity over Hilbert spaces is part of the statement.
  • VonNeumannAlgebra H is Mathlib's notion; these algebras contain the identity, so "unital with identity IHI_H" is built in.
  • kkDistance M N is Metric.hausdorffDist of the closed unit balls. Both balls contain 00 and are bounded, so the Hausdorff distance is finite and the definition is exactly (1.1).
  • NearConjugacy M N ε asks for a unitary vv with v M v∗=Nv\,M\,v^*=N as sets and ∥v−1∥<ε\|v-1\|<\varepsilon.
  • There is no trivializing reading: the hypotheses are satisfied by M=NM=N, and the conclusion is nontrivial for M≠NM\neq N.

Selected references

2 thms1 active userReviewed
Mathematical PhysicsPartial Differential Equations·Captain: wurtle

Sharp one-dimensional Lieb–Thirring constantsResearch Paper

Motivation

Lieb–Thirring inequalities bound the negative eigenvalues of a Schrödinger operator −Δ−W-\Delta-W by an integral of the potential. Lieb and Thirring introduced them in 1975 to give a short proof of the stability of matter, and they remain basic tools in mathematical physics, spectral theory and the analysis of many-fermion systems. The sharp constants are known only in a few cases. In one dimension, the Lieb–Thirring conjecture predicts the sharp constant for every exponent γ\gamma: for 1/2<γ<3/21/2<\gamma<3/2 it should be the constant of the best potential with a single bound state, given by an explicit sech⁡2\operatorname{sech}^2 profile.

Timeline

The source of this mission, an OpenAI preprint dated September 23, 2026, proves the conjectured sharp constant for every 1/2<γ<3/21/2<\gamma<3/2.

Setting

For 0≤W∈Lγ+1/2(R)0\le W\in L^{\gamma+1/2}(\mathbb R), let H−WH_{-W} be the self-adjoint operator of the quadratic form

h−W[v]=∫R∣v′∣2 dx−∫RW∣v∣2 dx,v∈H1(R).h_{-W}[v]=\int_{\mathbb R}|v'|^2\,dx-\int_{\mathbb R}W|v|^2\,dx,\qquad v\in H^1(\mathbb R).

For γ>1/2\gamma>1/2 its negative spectrum is discrete; write Tr⁡(H−W)−γ=∑λj<0∣λj∣γ\operatorname{Tr}(H_{-W})_-^\gamma=\sum_{\lambda_j<0}|\lambda_j|^\gamma with multiplicity, possibly +∞+\infty a priori. The optimal constant is

Lγ,1=sup⁡0≤W∈Lγ+1/2, W≢0Tr⁡(H−W)−γ∫Wγ+1/2,L_{\gamma,1}=\sup_{0\le W\in L^{\gamma+1/2},\ W\not\equiv0}\frac{\operatorname{Tr}(H_{-W})_-^\gamma}{\int W^{\gamma+1/2}},

Lγ,1(1)L^{(1)}_{\gamma,1} is the same supremum with only the lowest eigenvalue retained, and the semiclassical constant is

Lγ,1cl=Γ(γ+1)2π Γ(γ+3/2).L^{\rm cl}_{\gamma,1}=\frac{\Gamma(\gamma+1)}{2\sqrt\pi\,\Gamma(\gamma+3/2)}.

Formalization targets

Goal: Theorem 1.1

For 1/2<γ<3/21/2<\gamma<3/2 and every 0≤W∈Lγ+1/2(R)0\le W\in L^{\gamma+1/2}(\mathbb R),

Tr⁡(H−W)−γ ≤ 2(γ−1/2γ+1/2)γ−1/2Lγ,1cl∫RWγ+1/2;\operatorname{Tr}(H_{-W})_-^\gamma\ \le\ 2\Bigl(\frac{\gamma-1/2}{\gamma+1/2}\Bigr)^{\gamma-1/2}L^{\rm cl}_{\gamma,1}\int_{\mathbb R}W^{\gamma+1/2};

the constant equals Lγ,1=Lγ,1(1)L_{\gamma,1}=L^{(1)}_{\gamma,1}, and with r=(γ−1/2)−1r=(\gamma-1/2)^{-1} equality holds for W(x)=(r+1)sech⁡2(rx)W(x)=(r+1)\operatorname{sech}^2(rx). The Lean statement OAI.SharpLiebThirring.sharp_lieb_thirring is open on the platform.

Significance

The theorem settles the one-dimensional Lieb–Thirring conjecture on the whole interval 1/2<γ<3/21/2<\gamma<3/2, extending the case γ=1\gamma=1 of Read and Schulz: allowing many bound states never beats a single optimally shaped well. Combined with the known endpoint results (γ=1/2\gamma=1/2 and γ≥3/2\gamma\ge3/2), it completes the sharp one-dimensional constants. It also gives the corresponding bound for signed potentials (Corollary 7.3), and through the Laptev–Weidl lifting method one-dimensional sharp constants feed into higher-dimensional estimates.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. A formal proof would certify a proof whose key step is a finite-interval action inequality established by a continuation and degree argument for matrix fields.

Difficulty

Single-state bounds and numerical evidence say nothing about potentials with many bound states, and the conjecture requires a bound uniform over all orthonormal families of eigenfunctions. Methods that work at γ=1\gamma=1 (where the inequality is dual to a kinetic-energy bound for orthonormal families) do not directly apply at other exponents, since the moment ∑∣λj∣γ\sum|\lambda_j|^\gamma is not linear in the density matrix. The proof must keep track of the individual eigenvalue scales.

Formalization scope

  • H1 packages u∈L2(R;C)u\in L^2(\mathbb R;\mathbb C) with a weak derivative in L2L^2, tested against smooth compactly supported functions.
  • A negative eigenvalue −k2-k^2 (k>0k>0) is a weak eigenvalue of the form: h−W(v,u)=−k2⟨v,u⟩h_{-W}(v,u)=-k^2\langle v,u\rangle for all v∈H1v\in H^1.
  • negativeMoment γ W is the supremum, in [0,∞][0,\infty], over all finite orthonormal families of such eigenfunctions of ∑iki2γ\sum_ik_i^{2\gamma}; this counts multiplicity and does not presuppose finiteness. oneStateMoment retains one eigenfunction.
  • Admissible γ W is W≥0W\ge0 a.e. and W∈Lγ+1/2W\in L^{\gamma+1/2}; potentialMass is the lower Lebesgue integral of Wγ+1/2W^{\gamma+1/2}; the optimal constants are suprema over admissible WW with positive mass.
  • For admissible WW the integral ∫Wuˉv\int W\bar uv converges for u,v∈H1u,v\in H^1, so the form is correctly defined.

A complete development needs Sobolev space H1(R)H^1(\mathbb R) and form methods, the variational characterization of negative eigenvalues, Gamma-function identities for Lγ,1clL^{\rm cl}_{\gamma,1}, the explicit sech⁡2\operatorname{sech}^2 eigenvalue computation, and the paper's action inequality. Contributions formalizing Theorem 2.1 (action inequality) and the equality computation for the sech⁡2\operatorname{sech}^2 potential are welcome.

Selected references

2 thms1 active userReviewed
Dynamical Systems·Captain: wurtle

Two limit cycles for quintic Liénard systemsResearch Paper

Motivation

A limit cycle of a planar vector field is a periodic orbit that is isolated among periodic orbits. The second part of Hilbert's sixteenth problem asks how many limit cycles a polynomial vector field of a given degree can have, and it is open even for quadratic fields. The classical Liénard systems

x˙=y−F(x),y˙=−x,\dot x=y-F(x),\qquad \dot y=-x,

equivalent to the oscillator equation x′′+F′(x) x′+x=0x''+F'(x)\,x'+x=0, are the most studied restricted family. In 1977 Lins, de Melo and Pugh conjectured that for deg⁡F=n\deg F=n the maximum number of limit cycles is ⌊(n−1)/2⌋\lfloor (n-1)/2\rfloor. The conjecture is now known to fail for n≥6n\ge6, holds for n≤4n\le4, and degree five was the remaining undecided case, where it predicts exactly two.

This mission asks for a formal proof of the degree-five bound and its sharpness, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

  • 1975 — Rychkov proves the two-cycle bound for odd quintic FF (Differ. Uravn. 11, 1975).
  • 1977 — Lins, de Melo and Pugh formulate the ⌊(n−1)/2⌋\lfloor(n-1)/2\rfloor conjecture (LNM 597).
  • 2007 — Dumortier, Panazzolo and Roussarie find four cycles with deg⁡F=7\deg F=7 (Proc. AMS 2007).
  • 2011 — De Maesschalck and Dumortier find ⌊(n−1)/2⌋+2\lfloor(n-1)/2\rfloor+2 cycles for every n≥6n\ge6 (JDE 2011); De Maesschalck and Huzak later obtain at least n−2n-2 (JDDE 2015).
  • 2012 — Li and Llibre prove at most one limit cycle for deg⁡F=4\deg F=4 (JDE 2012).
  • 2014 — Li and Lu bound by two the cyclicity of nondegenerate slow–fast cycles in degree five (JDE 2014), a limiting-regime result.
  • 2017 — Llibre and Zhang survey the conjecture (Expo. Math. 2017).
  • September 2026 — The OpenAI preprint claims the unrestricted degree-five bound of two (Theorem 1.1, p. 1).

Setting

For a real polynomial FF (the primitive of the damping), consider the vector field VF(x,y)=(y−F(x), −x)V_F(x,y)=(y-F(x),\,-x) on R2\mathbb R^2. A solution is a differentiable z:R→R2z:\mathbb R\to\mathbb R^2 with z′(t)=VF(z(t))z'(t)=V_F(z(t)) for all tt. A periodic orbit is the image of a nonconstant solution that is periodic with some period T>0T>0. A limit cycle is a periodic orbit CC having an open neighbourhood UU such that every periodic orbit contained in UU equals CC. Limit cycles are counted as sets: once each, regardless of multiplicity, stability or hyperbolicity. The periodic orbits of a centre are not limit cycles.

Formalization targets

Goal: Theorem 1.1 (p. 1)

For every real polynomial FF with deg⁡F≤5\deg F\le5,

#{C⊂R2: C is a limit cycle of VF} ≤ 2,\#\{C\subset\mathbb R^2:\ C\ \text{is a limit cycle of }V_F\}\ \le\ 2,

and some FF with deg⁡F≤5\deg F\le5 has exactly two limit cycles. No parity, coefficient-sign, hyperbolicity or amplitude restriction is imposed.

Significance

The result itself. It decides the last open degree of the Lins–de Melo–Pugh conjecture in the affirmative, so the conjecture is true exactly for deg⁡F≤5\deg F\le5. Unlike the slow–fast result of Li and Lu, it bounds all cycles of every quintic system, including degenerate (multiple) ones and cycles of large amplitude. The preprint also corrects a proposed four-cycle quintic example from the literature by identifying it with a family known to have exactly two periodic solutions (p. 2).

Formalizing it. The statement uses only polynomials, ODE solutions and planar topology, so it is well suited to formal verification, and it would be one of the first machine-checked global limit-cycle bounds for a nonlinear family. The proof's general comparison results for smooth profiles (Propositions 5.2 and 5.3, pp. 32–34) and the global quadratic fit (Theorem 3.6, p. 18) are independent of the polynomial application and reusable.

Difficulty

Small-amplitude (Hopf/Melnikov) calculations only control cycles near the origin or near a perturbation of a centre; they say nothing about distant cycles. The even coefficients of FF prevent the reduction to the odd quintic family settled by Rychkov. Generic-perturbation arguments that remove multiple cycles cannot be used, since the count must include degenerate cycles. The preprint keeps the two half-orbits separate, writes each as an arch in coordinates u=x2/2u=x^2/2 valid at every amplitude, fits each arch by a quadratic comparison profile (Theorem 3.6), and controls how the fitted parameters move with width through a Schwarzian-type model inequality (Theorem 4.1, p. 20). Periodic orbits then become zeros of a single matching function (Proposition 2.5, p. 10), whose isolated zeros are bounded using an integrating factor (Section 6).

Formalization scope

  • The plane is ℝ × ℝ; vectorField F z = (z.2 - F.eval z.1, -z.1) with F : Polynomial ℝ and F.degree ≤ 5 (this includes constants and the zero polynomial, which have no limit cycles).
  • IsSolution requires HasDerivAt at every real time; IsPeriodicOrbit asks for a solution, a period T > 0, non-constancy, and C = range z.
  • IsLimitCycle F C is a periodic orbit with an open U ⊇ C such that every periodic orbit C' ⊆ U equals C.
  • Counting uses Set.encard on the set of limit cycles, so infinitely many would give ⊤; the goal asks for ≤ 2 for every admissible F and = 2 for some.
  • Neither conjunct is vacuous: the lower bound requires two actual distinct isolated periodic orbits.

Welcome contributions: existence and smooth dependence of return maps for planar polynomial flows, and the energy-identity first-order return calculation used for sharpness (Section 7, p. 39).

Selected references

2 thms1 active userReviewed
Discrete Geometry·Captain: wurtle

The logarithmic Brunn–Minkowski conjectureResearch Paper

Motivation: a logarithmic strengthening of Brunn–Minkowski

The Brunn–Minkowski inequality ∣(1−λ)K+λL∣≥∣K∣1−λ∣L∣λ|(1-\lambda)K+\lambda L|\ge|K|^{1-\lambda}|L|^\lambda is a cornerstone of convex geometry, with consequences ranging from the isoperimetric inequality to concentration of measure. The LpL_p Brunn–Minkowski theory of Firey and Lutwak replaces the Minkowski combination, whose support function is (1−λ)hK+λhL(1-\lambda)h_K+\lambda h_L, by a pp-mean of support functions. As p↓0p\downarrow0 the pp-mean becomes the geometric mean hK1−λhLλh_K^{1-\lambda}h_L^{\lambda}, giving the logarithmic combination of two bodies. In 2012 Böröczky, Lutwak, Yang and Zhang conjectured that, for origin-symmetric convex bodies, the logarithmic combination already satisfies the multiplicative Brunn–Minkowski bound. This would be a strict strengthening of the classical inequality in the symmetric case. The conjecture is equivalent to a logarithmic Minkowski inequality for cone-volume measures and, by work of Saroglou, implies the (B)-conjecture for even log-concave measures. Symmetry is essential: the inequality fails for general bodies.

Timeline

  • 1962–1993 — Firey introduces pp-means of convex bodies (Math. Scand. 10); Lutwak develops the LpL_p Brunn–Minkowski–Firey theory (J. Differential Geom. 38).
  • 2012 — Böröczky, Lutwak, Yang and Zhang pose the origin-symmetric log-Brunn–Minkowski conjecture (Problem 1.1), prove it in the plane, and show its equivalence with the logarithmic Minkowski inequality (Adv. Math.); in 2013 they characterize even cone-volume measures (J. Amer. Math. Soc. 26).
  • 2015–2016 — Saroglou proves the inequality for bodies unconditional in a common basis (Geom. Dedicata) and shows that the Lebesgue case implies the same inequality for all even log-concave measures, hence the (B)-conjecture (Mathematika).
  • 2017 — Colesanti, Livshyts and Marsiglietti prove a local version near Euclidean balls (J. Funct. Anal. 273).
  • 2020–2022 — Chen, Huang, Li and Liu prove the global LpL_p inequality for pp close to 11 (Adv. Math. 368); Kolesnikov and Milman prove the local LpL_p inequality for p≥1−cn−3/2p\ge1-cn^{-3/2} (Mem. AMS 277); Putterman proves local-to-global equivalence for all p∈[0,1)p\in[0,1) (J. Funct. Anal. 280); Böröczky and Kalantzopoulos treat bodies with common reflection symmetries (Trans. AMS 375, 2022).
  • 2023 — van Handel proves the local logarithmic inequality for origin-symmetric zonoids (GAFA Seminar).
  • 2026 — An OpenAI preprint, The logarithmic Brunn–Minkowski conjecture (OpenAI Math Release, September 23, 2026), claims the conjecture for origin-symmetric convex bodies in every dimension. It has not been peer reviewed, and its proof is not formally verified.

Setting

A convex body K⊂RnK\subset\mathbb R^n is a compact convex set with nonempty interior; it is origin-symmetric if K=−KK=-K, in which case 00 is an interior point. Its support function is

hK(u)=max⁡x∈K⟨x,u⟩,u∈Sn−1,h_K(u)=\max_{x\in K}\langle x,u\rangle ,\qquad u\in S^{n-1},

which is strictly positive for origin-symmetric bodies. For a positive function ff on the sphere, the Wulff body is

W[f]=⋂u∈Sn−1{x:⟨x,u⟩≤f(u)}.\mathcal W[f]=\bigcap_{u\in S^{n-1}}\{x:\langle x,u\rangle\le f(u)\}.

The logarithmic combination of K,LK,L with parameter λ∈[0,1]\lambda\in[0,1] is W[hK1−λhLλ]\mathcal W[h_K^{1-\lambda}h_L^{\lambda}]. In general hK1−λhLλh_K^{1-\lambda}h_L^{\lambda} is not itself a support function, which is why the Wulff body is needed. ∣⋅∣|\cdot| denotes Lebesgue measure.

Formalization targets

Goal: the even logarithmic Brunn–Minkowski inequality (Theorem 1.1)

For n≥1n\ge1, origin-symmetric convex bodies K,L⊂RnK,L\subset\mathbb R^n and 0≤λ≤10\le\lambda\le1,

∣W[hK1−λhLλ]∣ ≥ ∣K∣1−λ ∣L∣λ.\bigl|\mathcal W[h_K^{1-\lambda}h_L^{\lambda}]\bigr|\ \ge\ |K|^{1-\lambda}\,|L|^{\lambda}.

The goal statement is published on the platform with status Open.

Significance

The result itself. By the arithmetic–geometric mean inequality, W[hK1−λhLλ]⊆(1−λ)K+λL\mathcal W[h_K^{1-\lambda}h_L^\lambda]\subseteq(1-\lambda)K+\lambda L, so the theorem strengthens the multiplicative Brunn–Minkowski inequality for symmetric bodies. It implies the symmetric LpL_p Brunn–Minkowski inequality for every 0<p<10<p<1 (Corollary 1.2 of the source), the logarithmic Minkowski inequality for cone-volume measures, and, through Saroglou's transfer, the (B)-conjecture: t↦μ(etK)t\mapsto\mu(e^tK) is log-concave for every even log-concave measure μ\mu and origin-symmetric convex body KK (Corollary 8.1 of the source).

Formalizing it. The statement uses only Euclidean space, support functions and Lebesgue measure, all in Mathlib. The proof uses smooth approximation of polytopes, moment coordinates, a variance bound and a tensor estimate. A formal proof would put a long-standing conjecture of convex geometry on a machine-checked footing; Mathlib does not yet contain the classical Brunn–Minkowski inequality in this generality, and that would be a natural reusable milestone.

Difficulty

The classical proofs of Brunn–Minkowski (Prékopa–Leindler, mass transport) apply to Minkowski sums, but the logarithmic combination is not a Minkowski sum and hK1−λhLλh_K^{1-\lambda}h_L^\lambda is not a support function, so these tools give only the weaker inclusion bound. Local (second-variation) approaches reduce the problem to a spectral gap for the Hilbert–Brunn–Minkowski operator on even functions, but local-to-global arguments had only been completed near the ball, for zonoids, or under extra symmetry. Without symmetry the inequality is false, so any argument must use the evenness of the bodies.

Formalization scope

  • Space is EuclideanSpace ℝ (Fin n) with n≥1n\ge1; convex bodies are compact, convex, with nonempty interior; symmetry is x ∈ K ↔ -x ∈ K.
  • The support function is a real sSup of ⟨x,u⟩\langle x,u\rangle over KK, nonempty and bounded for a convex body, so it is the true maximum. Real powers rpow are applied to positive support values (positivity follows from symmetry and nonempty interior).
  • The Wulff body is the intersection of half-spaces over unit vectors uu. Volumes are volume in ℝ≥0∞, with ℝ≥0∞-valued powers 1−λ1-\lambda and λ\lambda. At λ∈{0,1}\lambda\in\{0,1\} the inequality reduces to ∣K∣≤∣K∣|K|\le|K| (resp. ∣L∣≤∣L∣|L|\le|L|), so the edge cases are consistent.
  • Needed infrastructure: support functions and Wulff shapes, polytope approximation, the Prékopa–Leindler inequality, and log-concave measures. Contributions formalizing the planar case, the unconditional case (Saroglou) or Corollary 1.2 from Theorem 1.1 are welcome.

Selected references

2 thms1 active userReviewed
Harmonic Analysis·Captain: wurtle

An Endpoint Gradient Bound for the Centered Disk Maximal OperatorResearch Paper

Motivation

The Hardy–Littlewood maximal function replaces a function by the largest of its averages around each point. It is the basic tool for differentiation theorems and singular integrals, and it is bounded on LpL^p for p>1p>1 but not on L1L^1. Kinnunen showed that it also preserves first-order Sobolev regularity: it is bounded on W1,p(Rn)W^{1,p}(\mathbb R^n) for 1<p<∞1<p<\infty, because ∣∇Mf∣≤M∣∇f∣|\nabla Mf|\le M|\nabla f| pointwise (Kinnunen 1997). At p=1p=1 this argument breaks, since MM is unbounded on L1L^1. Hajłasz and Onninen asked whether the gradient estimate ∥∇Mf∥1≤C∥∇f∥1\|\nabla Mf\|_1\le C\|\nabla f\|_1 nevertheless holds (Question 1 in Ann. Acad. Sci. Fenn. Math. 2004). The question is a test of whether maximal operators improve or destroy regularity at the endpoint, where the usual LpL^p machinery is unavailable.

This mission asks for a formal proof of the planar centered-disk case, as stated in an OpenAI preprint dated September 26, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

  • 1997 — Kinnunen: MM is bounded on W1,pW^{1,p}, 1<p<∞1<p<\infty (Israel J. Math. 1997).
  • 2002–2007 — In one dimension, Tanaka proves an L1L^1 derivative bound for the uncentered operator (Bull. Austral. Math. Soc. 2002); Aldaz and Pérez Lázaro obtain the sharp variation constant and absolute continuity (Trans. AMS 2007).
  • 2004 — Hajłasz and Onninen pose the endpoint question.
  • 2009 — Aldaz and Pérez Lázaro treat block-decreasing inputs in higher dimensions (Studia Math. 2009).
  • 2015 — Kurka proves a variation bound for the one-dimensional centered operator (Ann. Acad. Sci. Fenn. Math. 2015).
  • 2018 — Luiro proves the L1L^1 gradient estimate for radial inputs and the uncentered ball operator (Ark. Mat. 2018).
  • 2020–2025 — Beltran–Madrid and Weigt treat fractional centered operators (JFA 2020; Math. Z. 2022); Weigt proves variation bounds for dyadic and uncentered-cube maximal operators (IMRN 2023; JEMS 2025); Lahti and Weigt show that a variation bound for the centered operator upgrades to Sobolev regularity (arXiv:2510.01936).
  • September 2026 — The OpenAI preprint claims the planar centered-disk endpoint bound (Theorem 1.1, p. 1).

Setting

Identify R2\mathbb R^2 with the Euclidean plane and write B(x,r)B(x,r) for the open disk of radius rr centered at xx. For a locally integrable real function ff, the centered disk maximal function is

Mf(x)=sup⁡r>01πr2∫B(x,r)∣f(y)∣ dy∈[0,∞].Mf(x)=\sup_{r>0}\frac1{\pi r^2}\int_{B(x,r)}|f(y)|\,dy\in[0,\infty].

The space W1,1(R2)W^{1,1}(\mathbb R^2) consists of integrable ff whose distributional gradient is represented by an integrable vector field ∇f\nabla f, i.e. ∫f ∂iφ=−∫(∇f)iφ\int f\,\partial_i\varphi=-\int(\nabla f)_i\varphi for all φ∈Cc∞\varphi\in C_c^\infty. Norms of gradients are Euclidean: ∥∇f∥1=∫∣∇f∣\|\nabla f\|_1=\int|\nabla f|. For the signed estimate, put Atg(x)=1πt2∫B(x,t)gA_tg(x)=\frac1{\pi t^2}\int_{B(x,t)}g and Sa,bg(x)=sup⁡a≤t≤bAtg(x)S_{a,b}g(x)=\sup_{a\le t\le b}A_tg(x).

Formalization targets

Milestone: Proposition 1.2 (signed finite-band estimate, p. 2)

There is an absolute constant CC such that for every real g∈Cc∞(R2)g\in C_c^\infty(\mathbb R^2) and 0<a≤b0<a\le b with b/ab/a a power of two (including 11),

∫R2∣∇Sa,bg∣ dx≤C∫R2∣∇g∣ dx,\int_{\mathbb R^2}|\nabla S_{a,b}g|\,dx\le C\int_{\mathbb R^2}|\nabla g|\,dx,

with CC independent of aa, bb and the number of dyadic scales.

Goal: Theorem 1.1 (p. 1)

There is an absolute constant C<∞C<\infty such that for every real f∈W1,1(R2)f\in W^{1,1}(\mathbb R^2), MfMf is finite almost everywhere, locally integrable, belongs to Wloc1,1(R2)W^{1,1}_{\mathrm{loc}}(\mathbb R^2), and has a globally integrable weak gradient with

∫R2∣∇Mf∣ dx≤C∫R2∣∇f∣ dx.\int_{\mathbb R^2}|\nabla Mf|\,dx\le C\int_{\mathbb R^2}|\nabla f|\,dx.

Significance

The result itself. It resolves the planar centered-disk case of the Hajłasz–Onninen question with no radiality or support assumption. As a consequence (Corollary 6.3, p. 39) the bound extends to BV(R2)BV(\mathbb R^2) inputs and yields a co-area type perimeter bound for level sets of M1EM\mathbf 1_E. The constant is absolute but not optimized. Higher dimensions, other centered maximal operators, and continuity of f↦∇Mff\mapsto\nabla Mf in W1,1W^{1,1} remain separate questions.

Formalizing it. Mathlib has Lebesgue integration, weak derivatives only in limited form, and no maximal-function regularity theory. A formal proof would need distributional gradients, Poincaré inequalities on squares, dyadic multiscale decompositions and a vector-measure representation of bounded distributional derivatives (the preprint's Appendix A). These pieces are reusable across harmonic analysis.

Difficulty

For p>1p>1 one bounds ∣∇Mf∣≤M∣∇f∣|\nabla Mf|\le M|\nabla f| and uses the strong maximal inequality, which fails for p=1p=1. One-dimensional proofs order the optimizing intervals, and that ordering has no analogue for families of centered disks. Fractional-order proofs use that optimizing balls overlap little, a mechanism that degenerates at order zero. The preprint (Sections 2–5) instead proves the signed finite-band estimate uniformly in the number of scales: it uses a vanishing first moment at interior maximizing radii, a concentration-in-a-thin-shell lemma (Lemma 2.4, p. 8), and two multiscale constructions that pay for direction changes in scale and space. A variation bound alone would leave a possibly singular derivative measure; removing the singular part needs the signed form of Proposition 1.2 applied to locally mean-subtracted inputs (Section 6).

Formalization scope

  • The plane is EuclideanSpace ℝ (Fin 2). maximal f x is an ℝ≥0∞-valued supremum over all real r>0r>0 of lower Lebesgue integrals of ∣f∣|f| over Metric.ball x r divided by πr2\pi r^2; the goal asserts it is finite a.e. before passing to maximalReal = toReal.
  • HasWeakGradient f g is the integration-by-parts identity against every C∞C^\infty compactly supported test function, coordinatewise; the input is Integrable f, Integrable g, HasWeakGradient f g, which is exactly W1,1W^{1,1} with weak gradient g. The bound is stated against this g, so it does not depend on a choice of representative.
  • InW11Loc asks for local integrability and a locally integrable weak gradient; the goal also asks for one integrable weak gradient G with ∫ ‖G‖ ≤ C * ∫ ‖g‖, C ≥ 0 chosen before f.
  • The milestone uses signed averages (Bochner integrals) and sSup over the closed radius band [a,2ma][a,2^ma]; the band envelope is continuous in rr, so the supremum is finite. Inputs are ContDiff ℝ ∞ with compact support.
  • The BV extension (Corollary 6.3) is not part of either target.

Selected references

4 thms1 active userReviewed
Harmonic Analysis·Captain: wurtle

A uniform Hilbert transform estimate for Lipschitz directionsResearch Paper

Motivation

The Hilbert transform Hf(x)=p.v.∫f(x−t) dttHf(x)=\mathrm{p.v.}\int f(x-t)\,\frac{dt}{t} is the basic singular integral of harmonic analysis. In the plane one can take it along a line through each point, with the direction of the line allowed to depend on the point: given a unit vector field v:R2→S1v:\mathbb R^2\to S^1, integrate ff along the segment through xx in direction v(x)v(x). Whether such directional Hilbert transforms are bounded on L2L^2 is one of the central problems connecting singular integrals, Kakeya-type geometry and time–frequency analysis. If vv depends on only one coordinate, the L2L^2 problem already contains Carleson's theorem on almost-everywhere convergence of Fourier series. For general fields some regularity of vv is necessary, and some truncation of the integration length is necessary because a field can turn.

Stein asked whether a Lipschitz field suffices when the integration length is at most a small multiple of 1/Lip(v)1/\mathrm{Lip}(v). In the formulation of Lacey and Li, this is a uniform weak-(2,2)(2,2) conjecture. A parallel conjecture of Zygmund concerns the corresponding maximal averages.

Timeline

  • 1966. Carleson proves almost-everywhere convergence of Fourier series of L2L^2 functions (doi:10.1007/BF02392815); the one-variable-field L2L^2 case of the directional problem reduces to this.
  • 1987. Stein lists the Lipschitz directional Hilbert transform among problems in harmonic analysis in his ICM address (Problems in harmonic analysis related to curvature and oscillatory integrals).
  • 1989. Bourgain proves an L2L^2 bound for the maximal averaging operator along analytic vector fields (doi:10.1017/CBO9780511662294.006).
  • 2006. Lacey and Li prove annular weak-(2,2)(2,2) and strong LpL^p, p>2p>2, bounds for directional Hilbert transforms with measurable directions (doi:10.1090/S0002-9947-06-03869-4), and a Lipschitz Kakeya maximal theorem.
  • 2010. Lacey and Li's memoir develops the relation between maximal operators and the Hilbert-transform problem, with conditional results requiring stronger maximal estimates or C1+ηC^{1+\eta} fields (doi:10.1090/S0065-9266-10-00572-7).
  • 2012. Stein and Street prove local LpL^p bounds for singular Radon transforms associated with real-analytic maps (doi:10.1016/j.aim.2011.11.016).
  • 2013. Bateman proves single-annulus LpL^p estimates for fields depending on one coordinate (doi:10.4171/RMI/748); Bateman and Thiele prove strong LpL^p bounds, 3/2<p<∞3/2<p<\infty, for the full transform along one-variable fields (doi:10.2140/apde.2013.6.1577).
  • 2015–2017. Guo extends the one-variable setting to fields constant along Lipschitz curves (doi:10.2140/apde.2015.8.1263, doi:10.1090/tran/6750) and proves single-annulus variation-norm bounds for Lipschitz fields; Guo and Thiele treat a lacunary model of Lipschitz fields (doi:10.1112/S0025579316000280).
  • 2018. Di Plinio and Parissis extend the lacunary framework (doi:10.1007/s11856-018-1724-y); Di Plinio, Guo, Thiele and Zorin-Kranich show that uniform L2L^2 bounds on vertical frequency bands imply the full short principal-value bound under a small Lipschitz condition (doi:10.1016/j.jfa.2018.07.005).

The source of this mission, an OpenAI preprint dated September 25, 2026, claims the uniform strong L2L^2 bound at short scale for every Lipschitz field.

Setting

Let v:R2→S1v:\mathbb R^2\to S^1 be Lipschitz with Lip(v)≤1\mathrm{Lip}(v)\le1. For 0<ε<a0<\varepsilon<a the short directional Hilbert transform is

Hv,aεf(x)=∫ε<∣t∣<af(x−t v(x)) dtt.H^{\varepsilon}_{v,a}f(x)=\int_{\varepsilon<|t|<a} f\bigl(x-t\,v(x)\bigr)\,\frac{dt}{t}.

The direction is frozen at the output point xx. For a Schwartz function ff the principal value Hv,af=lim⁡ε↓0Hv,aεfH_{v,a}f=\lim_{\varepsilon\downarrow0}H^\varepsilon_{v,a}f exists at every point, since f(x−tv(x))−f(x+tv(x))=Ox(∣t∣)f(x-tv(x))-f(x+tv(x))=O_x(|t|).

Formalization targets

Goal: Theorem 1.1

There are absolute constants a∗∈(0,1/2)a_*\in(0,1/2) and C∗<∞C_*<\infty such that every unit field vv with Lip(v)≤1\mathrm{Lip}(v)\le1 satisfies, for all f∈S(R2)f\in\mathcal S(\mathbb R^2),

sup⁡0<ε<a∗∥Hv,a∗εf∥L2≤C∗∥f∥L2,∥Hv,a∗f∥2≤C∗∥f∥2,\sup_{0<\varepsilon<a_*}\|H^{\varepsilon}_{v,a_*}f\|_{L^2}\le C_*\|f\|_{L^2},\qquad \|H_{v,a_*}f\|_2\le C_*\|f\|_2, ∣{x:∣Hv,a∗f(x)∣>λ}∣≤C∗2λ−2∥f∥22(λ>0),\bigl|\{x:|H_{v,a_*}f(x)|>\lambda\}\bigr|\le C_*^2\lambda^{-2}\|f\|_2^2\qquad(\lambda>0),

and the truncations and the principal value extend to bounded operators on L2L^2 with norm at most C∗C_*. The constants a∗a_* and C∗C_* are existential; no numerical value is fixed. The Lean statement OAI.LipschitzHilbert.main is open on the platform.

The proposal also contains OAI.LipschitzHilbert.uniform_truncation, the rescaled form for KK-Lipschitz fields at every outer length R≤1/(106K)R\le 1/(10^6K). By the dilation x↦Kxx\mapsto Kx it is the same estimate at the reciprocal-Lipschitz scale; its explicit constant 10−610^{-6} is a convention of the formalization, not of the paper.

Significance

The theorem answers the short-scale form of Stein's question affirmatively and with a strong (not only weak-type) L2L^2 bound, for fields depending on both coordinates and with no regularity beyond Lipschitz. Earlier unconditional results required the field to depend on one variable, to be constant along a foliation, to be analytic, to take lacunary directions, or restricted the frequency to one annulus. The uniformity in the inner truncation is an operator bound for each truncation, which is what the principal value and the weak-type bound are derived from.

The result is claimed in an OpenAI preprint of 87 pages; it has not been peer reviewed and no machine-checked proof exists. The Lean goal records the complete short-scale conclusion; a formal proof would certify a long chain of time–frequency arguments (wave-packet decompositions, size and density selection, a Lipschitz Kakeya input, and a phase-gain iteration).

Difficulty

Restricting to short scales limits how far the field turns but does not make the operator a Fourier multiplier: the line of integration still varies with the output point. Positive (maximal) operator bounds lose all oscillation, while the one-variable reduction to Carleson's theorem is unavailable when vv depends on both coordinates. The known band-to-full reassembly reduces matters to one vertical frequency band, but on a band one needs a restricted estimate with a logarithmic gain in the ratio of the measures of the input and test sets; the Lacey–Li Kakeya estimate only provides a polynomial loss in that ratio, so an additional oscillatory saving is required.

Formalization scope

  • The plane is EuclideanSpace ℝ (Fin 2); inputs are SchwartzMap Plane ℂ, norms are eLpNorm _ 2 volume in ℝ≥0∞.
  • The field is v : Plane → Plane with LipschitzWith 1 v and ‖v x‖ = 1 for all x.
  • twoSidedTruncation v ε a f x is the sum of interval integrals over [−a,−ε][-a,-\varepsilon] and [ε,a][\varepsilon,a] of t−1f(x−tv(x))t^{-1}f(x-tv(x)); smoothPrincipalValue integrates the symmetric quotient over (0,a)(0,a), with the removable value at t=0t=0 filled by the derivative.
  • ShortHilbertConclusion a C bundles the five clauses (truncation bound for 0<ε<a0<\varepsilon<a, principal-value bound, weak-(2,2) bound at every finite nonzero level, and bounded Lp extensions agreeing a.e. on Schwartz inputs). The goal asks for a∈(0,1/2)a\in(0,1/2) and C>0C>0.

A complete development needs singular-integral and Littlewood–Paley machinery on R2\mathbb R^2, wave-packet analysis and a Lipschitz Kakeya maximal estimate; much of this is reusable for other time–frequency problems. Contributions formalizing the band-restricted estimate, the band-to-full reassembly, or the one-dimensional inputs (the maximal truncated Hilbert transform) are welcome.

Selected references

3 thms1 active userReviewed
Harmonic Analysis·Captain: wurtle

The Falconer distance conjecture in all dimensionsResearch Paper

Motivation

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

Background

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

Setting

  • Rd\mathbb R^d carries the Euclidean distance ∣x−y∣|x-y|.
  • For E⊂RdE\subset\mathbb R^d, the Hausdorff dimension dim⁡HE\dim_HE is the infimum of s≥0s\ge0 for which the ss-dimensional Hausdorff measure of EE vanishes.
  • Δ(E)={∣x−y∣:x,y∈E}⊂[0,∞)\Delta(E)=\{|x-y|:x,y\in E\}\subset[0,\infty), and L1\mathcal L^1 is Lebesgue measure on R\mathbb R.

Formalization targets

Milestone: the planar case

E⊂R2 compact, dim⁡HE>1 ⟹ L1(Δ(E))>0.E\subset\mathbb R^2\ \text{compact},\ \dim_HE>1\ \Longrightarrow\ \mathcal L^1(\Delta(E))>0.

Goal: Theorem 1.1

d≥2, E⊂Rd compact, dim⁡HE>d2 ⟹ L1(Δ(E))>0.d\ge2,\ E\subset\mathbb R^d\ \text{compact},\ \dim_HE>\tfrac d2\ \Longrightarrow\ \mathcal L^1(\Delta(E))>0.

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

3 thms1 active userReviewed
Geometry & Topology·Captain: wurtle

Koebe's Circle-Domain ConjectureResearch Paper

Motivation

The Riemann mapping theorem says that every simply connected proper domain in the plane is conformally equivalent to the unit disk. For domains with more complicated complements one needs a model with many "holes". Koebe's Kreisnormierungsproblem (1908) asks whether every domain in the Riemann sphere is conformally equivalent to a circle domain, one whose complementary components are all round disks or points. Such a model would give a canonical geometric picture of an arbitrary planar domain, and it is closely tied to circle packings, Kleinian groups and the geometry of hyperbolic surfaces of genus zero.

Timeline

  • 1908. Koebe poses the problem (Nachr. Ges. Wiss. Göttingen, 1908).
  • 1920. Koebe's treatment of the finitely connected case (doi:10.1007/BF01199400).
  • 1993. He and Schramm prove the conjecture for countably connected domains (doi:10.2307/2946541).
  • 1995. Schramm introduces transboundary extremal length and treats domains bounded by points and KK-quasicircles (doi:10.1007/BF02788827).
  • 2025. Rajala shows that arbitrary interior exhaustions can fail to have circle-domain limits and proves an exhaustion refinement theorem for countably connected domains (doi:10.1353/ajm.2025.a966291); Ntalampekos and Rajala study exhaustions of circle domains (arXiv:2312.06840).
  • 2026. Esmayli and Rajala prove uniformization for cospread domains and under a quasitripod condition (arXiv:2401.08485); Karafyllia and Ntalampekos treat spherical Gromov-hyperbolic domains (arXiv:2405.13782). Ntalampekos surveys the area (arXiv:2603.15098).

The source of this mission, an OpenAI preprint dated September 23, 2026, claims the conjecture in its unrestricted form.

Setting

The Riemann sphere is C^=C∪{∞}\widehat{\mathbb C}=\mathbb C\cup\{\infty\}, with local coordinate zz near finite points and 1/z1/z near ∞\infty. A domain is a nonempty connected open subset. A map ff is conformal at pp if it is continuous at pp and, in these coordinates, complex differentiable at pp with nonzero derivative. A conformal equivalence f:U→Vf:U\to V is a bijection that is conformal at every point of UU and whose inverse is conformal at every point of VV.

A closed round disk in C^\widehat{\mathbb C} is the image of the closed unit disk under a Möbius transformation z↦(az+b)/(cz+d)z\mapsto (az+b)/(cz+d), ad−bc≠0ad-bc\ne0; these are closed Euclidean disks, closed half-planes together with ∞\infty, and complements of open disks. A circle domain is a domain each of whose complementary connected components is a closed round disk or a single point. The complement may be empty, finite, countable or uncountable.

Formalization targets

Goal: Theorem 1.1 (circle-domain uniformization)

∀ G⊂C^ domain∃ Ω circle domain, ∃ f:G→ conformal Ω bijective.\forall\,G\subset\widehat{\mathbb C}\ \text{domain}\quad\exists\,\Omega\ \text{circle domain},\ \exists\,f:G\xrightarrow{\ \text{conformal}\ }\Omega\ \text{bijective}.

Lean: OAI.Problem047.koebe_circle_domain, open on the platform.

Significance

The theorem would complete the existence half of Koebe's problem with no restriction on the number, size or geometry of the complementary components. The paper derives a consequence for hyperbolic geometry (Corollary 8.1): every complete hyperbolic surface of genus zero is isometric to the boundary of the convex hull of a closed set in ∂∞H3\partial_\infty\mathbb H^3 whose components are round disks or points. Combined with the exhaustion theorem of Ntalampekos and Rajala, it also gives convergent finitely connected approximations for every proper domain. Uniqueness up to Möbius maps is a different question (the He–Schramm rigidity conjecture), addressed in the companion mission on removable boundaries.

The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists. Mathlib has neither the Riemann mapping theorem in full generality nor finitely connected circle-domain uniformization, so a formal proof would build substantial reusable complex-analytic infrastructure.

Difficulty

The standard approach uniformizes finitely connected approximations, whose complements are finitely many round disks, and passes to a limit. The difficulty is control at the limit: with possibly uncountably many complementary components, a limiting component can be strictly larger than the round disk obtained by following one approximating disk, or can be a non-round continuum for which no disk was followed at all. Rajala showed that arbitrary exhaustions can indeed fail to produce circle-domain limits, so the approximations must be chosen with care, and all components must be controlled simultaneously, not one at a time.

Formalization scope

  • Sphere := OnePoint ℂ; Möbius maps are Matrix.GeneralLinearGroup (Fin 2) ℂ acting on it.
  • IsConformalAt f p: ContinuousAt f p and a nonzero HasDerivAt of ff in the charts chart p, chart (f p) (identity coordinate at finite points, z↦1/zz\mapsto1/z at ∞\infty).
  • IsConformalEquivalence f U V: ff conformal on UU, MapsTo f U V, and a conformal g on VV with MapsTo g V U that is a two-sided inverse.
  • IsCircleDomain V: open, IsConnected (hence nonempty), and every connectedComponentIn Vᶜ p is a singleton or IsRoundClosedDisk (a Möbius image of the closed unit disk).
  • The goal quantifies over all open connected U; there is no countability or regularity assumption on the complement.

A complete development needs finitely connected uniformization, normal families on the sphere, Dirichlet energy and extremal length, and component correspondence for limits. Contributions formalizing the named intermediate results (Theorem 3.1 finite transfer, Theorem 4.3 compatible barrier lemma, Theorem 5.1 positive-law alternative, Theorem 7.5 retained-test transfer) or the classical He–Schramm countable case are welcome.

Selected references

2 thms1 active userReviewed
Geometry & Topology·Captain: wurtle

Removable Boundaries and Rigidity of Circle DomainsResearch Paper

Motivation

A circle domain is a domain in the Riemann sphere whose complementary components are round disks or points. Koebe asked in 1908 whether every domain is conformally equivalent to a circle domain (existence). A second question is rigidity: when is that circle-domain model unique up to Möbius transformations? For finitely and countably connected domains the model is unique, but for domains with uncountably many boundary components uniqueness can fail, and the boundary geometry decides. He and Schramm conjectured that a circle domain is rigid exactly when its boundary is conformally removable. Rigidity is what makes the circle-domain model canonical, and it connects conformal geometry with removability questions for quasiconformal and Sobolev maps.

Timeline

  • 1993. He and Schramm prove uniformization and rigidity for countably connected circle domains (doi:10.2307/2946541).
  • 1994. He and Schramm prove rigidity when the boundary has σ\sigma-finite linear measure, and conjecture that rigidity is equivalent to conformal removability of the boundary (doi:10.1007/BF01231761).
  • 2000. Jones and Smirnov relate removability for continuous Sobolev functions to quasiconformal removability (doi:10.1007/BF02384320).
  • 2016. Younsi proves that conformal rigidity is equivalent to quasiconformal rigidity and studies the removability formulations (doi:10.1016/j.aim.2016.08.039).
  • 2020. Ntalampekos and Younsi prove rigidity under square integrability of the quasihyperbolic distance, covering Hölder and John circle domains (doi:10.1007/s00222-019-00921-1).
  • 2023–2024. Ntalampekos proves rigidity when point components are countably negligible for extremal distance (CNED) and continuous Sobolev extension across closed CNED sets (doi:10.1090/tran/8923, doi:10.1007/s00029-024-00951-5).
  • 2025. Rajala constructs a rigid circle domain with non-removable boundary, so rigidity does not imply removability (doi:10.1112/plms.70081).

The source of this mission, an OpenAI preprint dated September 23, 2026, claims the remaining implication: removability implies rigidity.

Setting

The Riemann sphere C^=C∪{∞}\widehat{\mathbb C}=\mathbb C\cup\{\infty\} has local coordinates zz and 1/z1/z. A map is conformal at pp if it is continuous there and complex differentiable with nonzero derivative in these coordinates; a conformal equivalence f:Ω→Ω′f:\Omega\to\Omega' is a bijection, conformal on Ω\Omega, with conformal inverse. A Möbius transformation is z↦(az+b)/(cz+d)z\mapsto(az+b)/(cz+d) with ad−bc≠0ad-bc\neq0. A closed round disk is the Möbius image of the closed unit disk. A circle domain is a nonempty connected open set whose complementary components are closed round disks or points.

A compact E⊂C^E\subset\widehat{\mathbb C} is conformally removable if every orientation-preserving homeomorphism of C^\widehat{\mathbb C} that is conformal on C^∖E\widehat{\mathbb C}\setminus E is Möbius. A circle domain Ω\Omega is conformally rigid if every conformal equivalence from Ω\Omega onto another circle domain is the restriction of a Möbius transformation.

Formalization targets

Goal: Theorem 1.1

Ω,Ω′ circle domains,  ∂Ω conformally removable,  f:Ω→Ω′ conformal equivalence ⟹ ∃M Mo¨bius: f=M∣Ω.\Omega,\Omega'\ \text{circle domains},\ \ \partial\Omega\ \text{conformally removable},\ \ f:\Omega\to\Omega'\ \text{conformal equivalence}\ \Longrightarrow\ \exists M\ \text{Möbius}:\ f=M|_\Omega.

Lean: OAI.Problem047.removability_implies_rigidity, open on the platform. The complement may have any cardinality, and no boundary extension of ff is assumed.

Significance

Together with Rajala's counterexample to the converse, the theorem would settle the He–Schramm rigidity conjecture: removability is sufficient but not necessary. It subsumes the earlier sufficient conditions (σ\sigma-finite length, Hölder/John domains, CNED point sets) whenever those boundaries are removable. The intermediate Theorem 5.1, a continuous Sobolev extension theorem across compact totally disconnected conformally removable sets, is of independent interest. The result is claimed in an OpenAI preprint that has not been peer reviewed, and no machine-checked proof exists.

Difficulty

Removability is a statement about homeomorphisms of the whole sphere, while rigidity starts from a map defined only on the domain. The obvious route, extending ff to a homeomorphism of the sphere and then invoking removability, fails: a point component of the complement of Ω\Omega may correspond to a disk component of Ω′\Omega' and vice versa, so the coordinates of ff need not extend continuously, and nothing a priori controls boundary behaviour at uncountably many point components whose union can have positive area.

Formalization scope

  • Sphere := OnePoint ℂ, Möbius maps are Matrix.GeneralLinearGroup (Fin 2) ℂ acting on it; conformality uses the charts zz and 1/z1/z with HasDerivAt and a nonzero derivative.
  • IsCircleDomain: open, IsConnected, and every connectedComponentIn of the complement is a singleton or a Möbius image of the closed unit disk.
  • IsConformallyRemovable E: IsCompact E and every homeomorphism h : Sphere ≃ₜ Sphere that is homotopic to the identity (orientation preserving) and conformal on Eᶜ equals some Möbius map everywhere.
  • The boundary is frontier U; the conclusion is ∃ M, ∀ p ∈ U, f p = M • p.
  • The shared definitions are those of the Koebe circle-domain mission of the same family.

A complete development needs the theory of conformal maps on the sphere, Sobolev functions and Dirichlet energy in the plane, the measurable Riemann mapping theorem (used for the conductivity deformation), and component correspondence. Contributions formalizing Theorem 5.1 (continuous Sobolev extension), Proposition 6.2 (common point traces), or the He–Schramm countable case are welcome.

Selected references

2 thms1 active userReviewed
Algebraic GeometryDifferential Geometry·Captain: wurtle

Symmetry of semialgebraic bounded domains with compact quotientResearch Paper

Motivation: which bounded domains cover compact spaces?

A bounded symmetric domain is a bounded connected open set in Cm\mathbb C^m with, at every point, a holomorphic involution having that point as an isolated fixed point. Examples are the ball, the polydisc and the Siegel upper half-spaces in their bounded realizations. They are the universal covers of compact locally symmetric varieties, such as compact quotients of the ball, and play a central role in algebraic geometry and number theory. A classical theme in several complex variables is that a bounded domain with a large automorphism group must be very special: Wong and Rosay showed that an automorphism orbit accumulating at a strongly pseudoconvex boundary point forces the ball, and Frankel showed that convex domains with compact quotients are symmetric.

Kollár and Pardon, studying algebraic varieties whose universal cover is semialgebraic, asked the following bounded-domain question: if a bounded semialgebraic open subset of a complex affine variety admits a properly discontinuous cocompact group of biholomorphisms, must it be a bounded symmetric domain? Semialgebraicity is a finiteness condition on the shape of the domain. It does not make the boundary smooth or convex, and it imposes nothing on the group.

Timeline

  • 1970 — Vey proves that a divisible generalized Siegel domain is symmetric (Ann. Sci. ÉNS 3).
  • 1977 — Wong characterizes the ball by its automorphism group among strongly pseudoconvex domains (Invent. Math. 41).
  • 1979 — Rosay localizes Wong's theorem to a single C2C^2 strongly pseudoconvex boundary point (Ann. Inst. Fourier 29).
  • 1989 — Frankel proves that a convex hyperbolic domain with compact quotient is a bounded symmetric domain, including non-free actions (Acta Math. 163).
  • 2012 — Kollár and Pardon pose the bounded semialgebraic domain question (arXiv v2, Question 25) in Algebraic varieties with semialgebraic universal cover (J. Topol. 5; arXiv:1104.2309v2).
  • 2021 — Zimmer shows that a C1,1C^{1,1}-bounded domain covering a compact manifold is a ball (Indiana Univ. Math. J. 70).
  • 2026 — An OpenAI preprint, Symmetry of semialgebraic bounded domains with compact quotient (OpenAI Math Release, September 24, 2026), claims an affirmative answer to the Kollár–Pardon question. It has not been peer reviewed, and its proof is not formally verified.

Setting

An affine variety is a reduced complex algebraic set V⊂CnV\subset\mathbb C^n, the common zero locus of a set of polynomials. A subset of Cn\mathbb C^n is semialgebraic if it is a finite Boolean combination of sets {p=0}\{p=0\} and {p>0}\{p>0\}, with pp a real polynomial in the real and imaginary parts of the coordinates. Let U⊆VU\subseteq V be open in VV, connected, semialgebraic and bounded. A map on UU is holomorphic if near each point it is the restriction of a holomorphic map on an open subset of Cn\mathbb C^n; a biholomorphism is a homeomorphism that is holomorphic in both directions. A group Γ\Gamma acts properly discontinuously if the action is proper for the discrete topology on Γ\Gamma (finite stabilizers are allowed), and the action is cocompact if U/ΓU/\Gamma is compact. UU is smooth if each point has a neighbourhood in UU biholomorphic to an open subset of some Cm\mathbb C^m.

Formalization targets

Goal: semialgebraic bounded domains with compact quotient are symmetric (Theorem 1.1)

Let UU be a nonempty connected semialgebraic bounded open subset of a complex affine variety V⊂CnV\subset\mathbb C^n, and let a group Γ\Gamma act on UU by biholomorphisms, properly discontinuously and with U/ΓU/\Gamma compact. Then

U is smooth, andU≅D biholomorphically for some bounded symmetric domain D⊂Cm.U\ \text{is smooth, and}\quad U\cong D\ \text{biholomorphically for some bounded symmetric domain } D\subset\mathbb C^m .

The goal statement is published on the platform with status Open.

Significance

The result itself. The theorem answers the Kollár–Pardon question affirmatively. The ambient variety may be singular and nonnormal, the quotient may have finite quotient singularities, and no convexity, boundary regularity or homogeneity is assumed. It shows that semialgebraicity of a single affine realization forces the classical picture: a compact quotient of a semialgebraic bounded domain is a compact quotient of a bounded symmetric domain. This complements the universal-cover classification of the companion preprint on semialgebraic universal covers of normal projective varieties.

Formalizing it. The statement only uses polynomials, real-analytic Boolean combinations, holomorphic maps on subsets of Cn\mathbb C^n and group actions, all available in Mathlib. The proof, however, draws on Nash cell decompositions, analytic discs, scaling limits of automorphisms and Vey's theorem on divisible Siegel domains, none of which is formalized. A formal development would provide reusable semialgebraic geometry and several-complex-variables infrastructure.

Difficulty

The classical rigidity arguments (Wong–Rosay, Frankel, Zimmer) need a smooth strongly pseudoconvex or convex boundary point at which rescaled automorphisms converge to a model domain. A semialgebraic boundary can have corners with several complex-normal directions, and the normal fibres can shrink at rates that depend on tangential parameters, so the naive rescaling limit can collapse to a degenerate set. Moreover UU is not known to be a manifold at the start, so smoothness must be proved from the group action before any differential geometry is available. The heart of the proof is a noncollapse estimate that yields a Siegel-type quadratic model {Im⁡w−H(z,z)∈C}\{\operatorname{Im}w-H(z,z)\in C\} to which Vey's theorem applies.

Formalization scope

  • VV is IsAffineAlgebraic, the zero set of a set of complex polynomials in Fin n → ℂ; U⊆VU\subseteq V is open in the subspace topology of VV, IsConnected (hence nonempty), bounded, and semialgebraic through an inductive predicate on real polynomials in (Re⁡z,Im⁡z)(\operatorname{Re}z,\operatorname{Im}z), closed under complement and union.
  • Γ\Gamma is an arbitrary group with the discrete topology acting on the subtype UU, with ProperSMul and a compact orbit space. Each γ\gamma acts holomorphically in the sense of local ambient analytic extension; since γ−1\gamma^{-1} also acts, the elements act by biholomorphisms. A non-faithful action is allowed and is harmless, since properness forces finite stabilizers.
  • IsSmooth U asks for local biholomorphisms of neighbourhoods in UU onto open subsets of some Cm\mathbb C^m. IsBoundedSymmetricDomain D asks that DD be open, connected and bounded, and have at each point an involutive biholomorphism fixing it with that point isolated among its fixed points.
  • The zero-dimensional case (a point) is included and is trivial, matching the source convention.
  • Needed infrastructure: semialgebraic cell decomposition and selection, Montel-type compactness on singular analytic sets, analytic discs, Kobayashi/Carathéodory-type distance estimates and the structure theory of Siegel domains. Each would be reusable.

Selected references

2 thms1 active userReviewed
Operations ResearchProbabilityStochastic Systems·Captain: mikedeng1

Law of Large Numbers Limits for Many-Server Queues 1: The Fluid Equations Have at Most One Solution, Given Explicitly by the Age Representation (3.11)Research Paper

Motivation

Large service systems such as call centers and hospital wards are modelled as many-server queues: NN identical servers, customers arriving according to a general process, service requirements drawn independently from a general distribution GG, and a single first-come-first-served queue. When GG is not exponential the number of customers in system is not Markov, and a tractable state must keep track of how long each customer in service has been served. Kaspi and Ramanan (Ann. Appl. Probab. 21 (2011)) take as state the number in system together with the age measure, the point measure of the ages of the customers in service, and prove a functional law of large numbers: scaled by NN, these processes converge to the unique solution of a deterministic system, the fluid equations. Earlier fluid and diffusion analyses of the G/GI/NG/GI/N queue worked with other state descriptors (Reed, Ann. Appl. Probab. 19 (2009); Whitt, Oper. Res. 54 (2006)); the measure-valued description records the elapsed service time of every customer in service, which is the information a non-exponential service distribution requires.

This mission covers the deterministic half of that result: the fluid equations are well posed, and their solution is given in closed form.

Setting

Service requirements have a density gg that vanishes on (−∞,0)(-\infty,0), G(x)=∫(−∞,x]gG(x)=\int_{(-\infty,x]}g, and the mean is normalized to one, ∫x g(x) dx=1\int x\,g(x)\,dx=1. Let M=sup⁡{x≥0:G(x)<1}∈(0,∞]M=\sup\{x\ge0: G(x)<1\}\in(0,\infty] and let h=g/(1−G)h=g/(1-G) be the hazard rate on [0,M)[0,M); hh is locally integrable on [0,M)[0,M) but not integrable on it. For a measure μ\mu and a function ff write ⟨f,μ⟩=∫f dμ\langle f,\mu\rangle=\int f\,d\mu, and 1\mathbf 1 for the constant one.

The data are a triple (Eˉ,Xˉ(0),νˉ0)(\bar E,\bar X(0),\bar\nu_0) in

S0={(f,x,μ):f nondecreasing caˋdlaˋg,f(0)=0; x≥0; μ a measure on [0,M), ⟨1,μ⟩≤1, 1−⟨1,μ⟩=[1−x]+},\mathcal S_0=\{(f,x,\mu): f \text{ nondecreasing càdlàg}, f(0)=0;\ x\ge0;\ \mu \text{ a measure on }[0,M),\ \langle\mathbf 1,\mu\rangle\le1,\ 1-\langle\mathbf 1,\mu\rangle=[1-x]^+\},

where Eˉ\bar E is the cumulative arrival process, Xˉ(0)\bar X(0) the initial number in system and νˉ0\bar\nu_0 the initial age measure (per server, so the total capacity is one). A càdlàg pair (Xˉ,νˉ)(\bar X,\bar\nu), with νˉt\bar\nu_t a sub-probability measure on [0,M)[0,M) in the weak topology, solves the fluid equations if for every t≥0t\ge0: ∫0t⟨h,νˉs⟩ds<∞\int_0^t\langle h,\bar\nu_s\rangle ds<\infty (3.4); for every test function φ∈Cc1,1([0,M)×R+)\varphi\in\mathcal C_c^{1,1}([0,M)\times\mathbb R_+)

⟨φ(⋅,t),νˉt⟩=⟨φ(⋅,0),νˉ0⟩+∫0t⟨φx+φs,νˉs⟩ds−∫0t⟨hφ(⋅,s),νˉs⟩ds+∫[0,t]φ(0,s) dKˉ(s)(3.5);\langle\varphi(\cdot,t),\bar\nu_t\rangle=\langle\varphi(\cdot,0),\bar\nu_0\rangle+\int_0^t\langle\varphi_x+\varphi_s,\bar\nu_s\rangle ds-\int_0^t\langle h\varphi(\cdot,s),\bar\nu_s\rangle ds+\int_{[0,t]}\varphi(0,s)\,d\bar K(s)\quad(3.5);

Xˉ(t)=Xˉ(0)+Eˉ(t)−Dˉ(t)\bar X(t)=\bar X(0)+\bar E(t)-\bar D(t) (3.6); and the nonidling condition 1−⟨1,νˉt⟩=[1−Xˉ(t)]+1-\langle\mathbf 1,\bar\nu_t\rangle=[1-\bar X(t)]^+ (3.7). Here Dˉ(t)=∫0t⟨h,νˉs⟩ds\bar D(t)=\int_0^t\langle h,\bar\nu_s\rangle ds is the cumulative departure process and Kˉ(t)=⟨1,νˉt⟩−⟨1,νˉ0⟩+Dˉ(t)\bar K(t)=\langle\mathbf 1,\bar\nu_t\rangle-\langle\mathbf 1,\bar\nu_0\rangle+\bar D(t) the cumulative entry into service. Equation (3.5) is a weak form of a transport equation: mass moves to the right at unit speed, is killed at rate hh, and enters at age 00 at rate dKˉd\bar K.

Formalization targets

Goal: Theorem 3.5

For every (Eˉ,Xˉ(0),νˉ0)∈S0(\bar E,\bar X(0),\bar\nu_0)\in\mathcal S_0:

  1. the fluid equations have at most one solution;
  2. under (3.4) and the path conditions, (Xˉ,νˉ)(\bar X,\bar\nu) is a solution if and only if it satisfies (3.6), (3.7) and, for every bounded continuous ff and t≥0t\ge0,
⟨f,νˉt⟩=∫[0,M)f(x+t)1−G(x+t)1−G(x) νˉ0(dx)+∫[0,t]f(t−s)(1−G(t−s)) dKˉ(s);(3.11)\langle f,\bar\nu_t\rangle=\int_{[0,M)}f(x+t)\frac{1-G(x+t)}{1-G(x)}\,\bar\nu_0(dx)+\int_{[0,t]}f(t-s)\big(1-G(t-s)\big)\,d\bar K(s);\quad(3.11)
  1. if Eˉ\bar E has a density λˉ\bar\lambda, then Kˉ\bar K has a density κˉ\bar\kappa equal a.e. to λˉ\bar\lambda where Xˉ<1\bar X<1, to λˉ∧⟨h,νˉt⟩\bar\lambda\wedge\langle h,\bar\nu_t\rangle where Xˉ=1\bar X=1, and to ⟨h,νˉt⟩\langle h,\bar\nu_t\rangle where Xˉ>1\bar X>1 (3.12);
  2. if moreover νˉ0\bar\nu_0 is absolutely continuous, so is every νˉt\bar\nu_t.

Milestones

  • Remark 4.3, (4.4): integration by parts for the entry term of (4.3).
  • (4.55): the integrated hazard in closed form, ψh(x,t)=(1−G(x))/(1−G(x−t))\psi_h(x,t)=(1-G(x))/(1-G(x-t)) or 1−G(x)1-G(x).
  • Theorem 4.1: for a Radon-measure-valued path satisfying the hazard bound (4.1), the age equation (4.2), which is (3.5) with an arbitrary Radon measure υ0\upsilon_0 and an arbitrary ZZ of bounded variation in place of νˉ0\bar\nu_0 and Kˉ\bar K, holds if and only if the representation (4.3) holds.
  • Proof of Corollary 4.4: Kˉ\bar K is nondecreasing.
  • Corollary 4.4, (4.5): Kˉ(t)=⟨1,νˉt⟩−⟨1,νˉ0⟩+∫G(x+t)−G(x)1−G(x)νˉ0(dx)+∫0tg(t−s)Kˉ(s)ds\bar K(t)=\langle\mathbf 1,\bar\nu_t\rangle-\langle\mathbf 1,\bar\nu_0\rangle+\int\frac{G(x+t)-G(x)}{1-G(x)}\bar\nu_0(dx)+\int_0^tg(t-s)\bar K(s)ds.
  • Lemma 4.5: ∥⟨f,νˉs2⟩−⟨f,νˉs1⟩∥T≤∥f∥M∣Δυ0∣TV+(2∥f∥T+∥f′∥T)∥ΔZ∥T\|\langle f,\bar\nu^2_s\rangle-\langle f,\bar\nu^1_s\rangle\|_T\le\|f\|_M|\Delta\upsilon_0|_{TV}+(2\|f\|_T+\|f'\|_T)\|\Delta Z\|_T.
  • Theorem 4.6: with equal initial measures, ∥ΔKˉ∥T∨∥ΔDˉ∥T≤∣ΔXˉ(0)∣+∥ΔEˉ∥T\|\Delta\bar K\|_T\vee\|\Delta\bar D\|_T\le|\Delta\bar X(0)|+\|\Delta\bar E\|_T, together with (4.8) and (4.10).

Significance

Uniqueness of the fluid solution is what turns tightness of the scaled NN-server processes into convergence: every subsequential limit solves the fluid equations, so all coincide (the paper's Theorem 3.7). The representation (3.11) reduces the measure-valued equation to the scalar process Kˉ\bar K, and the continuity estimate of Theorem 4.6 says the fluid solution is a Lipschitz function of the arrival process. Both are used in the paper's study of long-time behaviour, where νˉt\bar\nu_t converges to the measure with density 1−G1-G, and (3.12) is the form of the entry rate used there.

The results are proved in the paper. None of them, and no part of the measure-valued fluid model, has a machine-checked proof. Formalizing them produces a checked weak-solution theory for a transport equation with an unbounded killing rate and a measure-valued boundary input, which is a reusable piece of infrastructure for other age- and residual-time-based queueing models.

Difficulty

The central step is Theorem 4.1. The naive approach treats (4.2) as a first-order PDE and integrates along characteristics, but the solution is only a càdlàg path of measures, hh is merely locally integrable and blows up near MM, and ZZ may jump, so classical characteristics are not available; the test functions must not vanish on the boundary x=0x=0, since that is where the entry term lives. The second difficulty is in Theorem 4.6: the entry process Kˉ\bar K is defined implicitly through the nonidling condition, and comparing two solutions requires a first-crossing argument that distinguishes whether the system is below, at or above capacity at that time.

Formalization scope

The service law is its density gg (ServiceLaw), with g=0g=0 below 00, ∫g=1\int g=1 and mean one. Time is R\mathbb R read on [0,∞)[0,\infty); every condition is stated for t≥0t\ge0. Measures of the fluid model are FiniteMeasure ℝ carried by [0,M)[0,M), whose topology is weak convergence, so càdlàg paths are càdlàg in MF[0,M)\mathcal M_F[0,M) with the weak topology. The paths of Theorem 4.1 and Lemma 4.5 are ℝ → Measure ℝ with values Radon on [0,M)[0,M) (possibly infinite) and càdlàg in the vague topology. M∈[0,∞]M\in[0,\infty] is an extended number. The integral in (3.4) is a lower integral in [0,∞][0,\infty], and Dˉ\bar D, Kˉ\bar K are its real value. dKˉd\bar K is the Lebesgue–Stieltjes measure of Kˉ\bar K, with no atom at 00. A function ZZ of bounded variation is a difference Z1−Z2Z_1-Z_2 of nondecreasing càdlàg functions vanishing at 00.

Explicit choices: compact support of test functions is relative to [0,M)×R+[0,M)\times\mathbb R_+, so φ(0,s)\varphi(0,s) need not vanish (with supports taken in R2\mathbb R^2 the entry term of (3.5) would vanish identically); νˉ(0)=νˉ0\bar\nu(0)=\bar\nu_0 and Xˉ(0)\bar X(0) equal to the datum are clauses of the fluid equations, but not of the age equation, where υ0\upsilon_0 is arbitrary; functions in Cb(R+)\mathcal C_b(\mathbb R_+), Cc(R+)\mathcal C_c(\mathbb R_+) and Cb1(R+)\mathcal C^1_b(\mathbb R_+) are represented by functions on R\mathbb R of the same class, of which only values on [0,∞)[0,\infty) are read; norms in Lemma 4.5 are computed in [0,∞][0,\infty], since ∣Δυ0∣TV|\Delta\upsilon_0|_{TV} may be infinite. Two printed statements are corrected: in Theorem 3.5 the paper's right-hand side of the equivalence lists (3.6) and (3.11); the nonidling condition (3.7), part of the fluid equations on the left, is kept on the right, as the proof requires. In (4.10), ΔXˉ(0)\Delta\bar X(0) is replaced by ∣ΔXˉ(0)∣|\Delta\bar X(0)|, which is what Lemma 4.5 and (4.9) give.

A fluid solution is defined by the weak transport equation (3.5), never by the representation (3.11) or by a formula for νˉ\bar\nu in terms of Kˉ\bar K; with such a definition the equivalence of the goal would be an unfolding of definitions.

A complete development needs Lebesgue–Stieltjes integration by parts for càdlàg functions of bounded variation, the Riesz description of the vague topology, and uniqueness for weak solutions of transport equations; these are reusable beyond this mission. Proofs of any milestone, and of the parts of Theorem 3.5 separately, are welcome. The paper's Section 4.3 machinery (the abstract and simplified age equations, Lemmas 4.12–4.13, Propositions 4.15–4.16) is not posed here and may be formalized as supporting lemmas.

Selected references

10 thms1 active userReviewed
ProbabilityRandom Matrix Theory·Captain: mikedeng1

Phase Transition of the Largest Eigenvalue for Nonnull Complex Sample Covariance Matrices 2: Spikes above 1+γ⁻¹ Give √M Fluctuations of the Largest Eigenvalue with Limit G_k, the k×k GUE LawResearch Paper

Motivation

Sample covariance matrices are the basic object of multivariate statistics: principal component analysis, signal detection and factor models all start from the eigenvalues of S=1M∑k=1My⃗ky⃗k ∗S = \frac1M\sum_{k=1}^M \vec y_k \vec y_k^{\,*} computed from MM samples of an NN-dimensional vector. When NN is comparable to MM, the eigenvalues of SS no longer approximate those of the population covariance Σ\Sigma. The question is then whether a few large population eigenvalues ("spikes") are visible in the sample spectrum at all, and how the top sample eigenvalue fluctuates when they are.

Baik, Ben Arous and Péché (Ann. Probab. 33 (2005) 1643–1697) answered this for complex Gaussian samples. They found a sharp threshold 1+γ−11+\gamma^{-1}, where γ2=M/N\gamma^2 = M/N, now called the BBP phase transition. This mission formalizes the supercritical half of the answer, Theorem 1.1(b).

Timeline.

  • 2000–2001: Johansson (Comm. Math. Phys. 209, 2000) and Johnstone (Ann. Statist. 29) proved that for Σ=I\Sigma = I the largest eigenvalue, centred at (1+γ−1)2(1+\gamma^{-1})^2 and scaled by M2/3M^{2/3}, has the Tracy–Widom law. Johansson treated the complex case, Johnstone the real case.
  • 2005: Baik, Ben Arous and Péché treated Σ\Sigma with finitely many eigenvalues different from 11. Spikes at or below 1+γ−11+\gamma^{-1} give M2/3M^{2/3} fluctuations with limit laws FkF_k (part (a), a separate mission of this series). Spikes above 1+γ−11+\gamma^{-1} give M\sqrt M fluctuations with limit GkG_k (part (b)).
  • 2006: Baik and Silverstein (J. Multivariate Anal. 97) located the outlying eigenvalue for general, non-Gaussian samples. Bai and Yao (Ann. IHP 44, 2008) obtained Gaussian fluctuations of the outliers for general samples.

Setting

Let gkjg_{kj}, 1≤k≤M1 \le k \le M, 1≤j≤N1 \le j \le N, be independent standard complex Gaussians: g=a+ibg = a + ib with a,ba, b independent real normal variables of mean 00 and variance 1/21/2. Fix a unitary matrix UU and positive population eigenvalues ℓ1,…,ℓN\ell_1, \dots, \ell_N. The samples are

y⃗k=U diag(ℓ1,…,ℓN) g⃗k,\vec y_k = U\,\mathrm{diag}(\sqrt{\ell_1},\dots,\sqrt{\ell_N})\,\vec g_k,

which are independent mean-zero complex Gaussian vectors with covariance Σ=U diag(ℓ) U∗\Sigma = U\,\mathrm{diag}(\ell)\,U^*. The sample covariance matrix is S=1M∑ky⃗ky⃗k ∗S = \frac1M\sum_k \vec y_k\vec y_k^{\,*}, and λ1\lambda_1 is its largest eigenvalue.

The regime has M,N→∞M, N \to \infty with M/N=γ2M/N = \gamma^2 and γ\gamma in a compact subset of [1,∞)[1,\infty). A fixed number rr of the ℓj\ell_j differ from 11. For some 1≤k≤r1 \le k \le r the top kk coincide, ℓ1=⋯=ℓk\ell_1 = \cdots = \ell_k, with common value in a compact subset of (1+γ−1,∞)(1+\gamma^{-1},\infty). The others, ℓk+1,…,ℓr\ell_{k+1},\dots,\ell_r, lie in a compact subset of (0,ℓ1)(0,\ell_1).

The limit law is the finite GUE distribution. Let Zk=∫Rk∏i<j∣ξi−ξj∣2∏ie−ξi2/2 dξZ_k = \int_{\mathbb R^k}\prod_{i<j}|\xi_i-\xi_j|^2\prod_i e^{-\xi_i^2/2}\,d\xi. Then

Gk(x)=1Zk∫(−∞,x]k∏1≤i<j≤k∣ξi−ξj∣2∏i=1ke−ξi2/2 dξ1⋯dξk,G_k(x) = \frac1{Z_k}\int_{(-\infty,x]^k}\prod_{1\le i<j\le k}|\xi_i-\xi_j|^2\prod_{i=1}^k e^{-\xi_i^2/2}\,d\xi_1\cdots d\xi_k,

which is the law of the largest eigenvalue of a k×kk\times k Gaussian unitary ensemble matrix (Definition 1.2).

Formalization targets

Goal: Theorem 1.1(b)

P((λ1−(ℓ1+ℓ1γ−2ℓ1−1))⋅Mℓ12−ℓ12γ−2/(ℓ1−1)2≤x)⟶Gk(x)for every x∈R.\mathbb P\left(\Big(\lambda_1 - \Big(\ell_1 + \frac{\ell_1\gamma^{-2}}{\ell_1-1}\Big)\Big)\cdot\frac{\sqrt M}{\sqrt{\ell_1^2 - \ell_1^2\gamma^{-2}/(\ell_1-1)^2}} \le x\right) \longrightarrow G_k(x)\qquad\text{for every } x \in \mathbb R.

Companion: Corollary 1.1(b)

λ1−ℓ1(1+γ−2ℓ1−1)⟶0in probability.\lambda_1 - \ell_1\Big(1 + \frac{\gamma^{-2}}{\ell_1-1}\Big) \longrightarrow 0 \quad\text{in probability.}

Milestones

The milestones follow the proof in §4, in attack order:

  • the critical points of the phase ff, (218)–(219);
  • the contour estimates, Lemmas 4.1 and 4.2;
  • the uniform kernel asymptotics, Proposition 4.1;
  • the Hermite-polynomial identities (287), (295), (288) and (292);
  • the closed form (299) of the limiting kernel K2K_2;
  • the Fredholm-determinant representation of GkG_k, Lemma 1.1:
Gk(x)=det⁡(1−Hx(k)),H(k)(u,v)=ck−1ck pk(u)pk−1(v)−pk−1(u)pk(v)u−v e−(u2+v2)/4.G_k(x) = \det\big(1 - \mathbf H^{(k)}_x\big),\qquad H^{(k)}(u,v) = \frac{c_{k-1}}{c_k}\,\frac{p_k(u)p_{k-1}(v) - p_{k-1}(u)p_k(v)}{u-v}\,e^{-(u^2+v^2)/4}.

Here pnp_n are the orthonormal polynomials for the weight e−x2/2e^{-x^2/2} and cnc_n their leading coefficients.

Significance

The result. Below the threshold the top eigenvalue sticks to the bulk edge (1+γ−1)2(1+\gamma^{-1})^2. Above it, Theorem 1.1(b) and Corollary 1.1(b) show that λ1\lambda_1 separates from the bulk to the explicit location ℓ1(1+γ−2/(ℓ1−1))\ell_1(1+\gamma^{-2}/(\ell_1-1)). Its fluctuations shrink from order M−2/3M^{-2/3} to order M−1/2M^{-1/2}, and their law is the top eigenvalue of a k×kk\times k GUE, with kk the multiplicity of the spike. This gives:

  • a detection threshold for spiked signals in high dimension;
  • the centring and scaling of tests based on the top sample eigenvalue;
  • the first instance of a kk-dependent family of finite-GUE limits in a spiked model.

Formalizing it. The result is proved in the paper and is not open. Nothing in this mission has a machine-checked proof yet. A complete development would include:

  • the first formal statements of the spiked complex Wishart model;
  • the GUE law GkG_k and its Fredholm representation;
  • a uniform steepest-descent analysis with explicit contours.

The two contour lemmas (4.1, 4.2) and the Hermite identities are elementary and are footholds. Proposition 4.1 and Lemma 1.1 are substantial. The paper does not prove Lemma 1.1 but cites it as a standard result of random matrix theory (its references [28, 41]).

Difficulty

The obvious route is to diagonalise the sample matrix, write down the eigenvalue density and take a limit. That density involves the Harish-Chandra–Itzykson–Zuber integral. Its large-NN limit is not accessible directly, because the spike enters through a determinant with NN nearly coincident columns.

The paper instead starts from an exact Fredholm-determinant formula (Proposition 2.1, posed in mission 1 of this series). In it the kernel factors into two contour integrals H\mathcal H and J\mathcal J with phase f(z)=−μ(z−q)+log⁡z−γ−2log⁡(1−z)f(z) = -\mu(z-q) + \log z - \gamma^{-2}\log(1-z). Above the threshold the two factors are governed by different points. J\mathcal J has a nondegenerate saddle at π1=ℓ1−1\pi_1 = \ell_1^{-1}. For H\mathcal H the natural saddle 1/(μπ1)1/(\mu\pi_1) lies beyond the pole at π1\pi_1, so the contour must be deformed through a pole of order kk, and the leading term is a residue rather than a saddle contribution. The estimates must hold uniformly in γ\gamma and in the remaining spikes, and the convergence must be strong enough (Hilbert–Schmidt) to pass to Fredholm determinants.

Formalization scope

Model. Complex Gaussian samples with mean zero and no centring. S=1M∑ky⃗ky⃗k ∗S = \frac1M\sum_k\vec y_k\vec y_k^{\,*}, with the factor 1/M1/M. Σ=U diag(ℓ) U∗\Sigma = U\,\mathrm{diag}(\ell)\,U^* for every unitary UU. This is the model of the paper's (59), (61) and Proposition 2.1; the introduction's mentions of 1/N1/N, of centring and of the real density (1) are inconsistent with those formulas. λ1\lambda_1 is the supremum of the eigenvalues of the Hermitian matrix SS, and probabilities are measures of sets of sample arrays.

Regime. The regime is in sequence form:

  • Nn→∞N_n \to \infty and γn=Mn/Nn∈[1,γ0]\gamma_n = \sqrt{M_n/N_n} \in [1,\gamma_0];
  • 1+γn−1+c≤ℓ1=⋯=ℓk≤C1+\gamma_n^{-1}+c \le \ell_1 = \cdots = \ell_k \le C;
  • c≤ℓj≤ℓ1−cc \le \ell_j \le \ell_1 - c for k<j≤rk < j \le r;
  • ℓj=1\ell_j = 1 for j>rj > r.

The fixed margins c,Cc, C encode the compact subsets whose open ends move with γ\gamma. Convergence is pointwise in xx.

Analytic conventions.

  • The Fredholm determinant is the Fredholm series ∑n(−1)nn!∫(x,∞)ndet⁡[K(ui,uj)]\sum_n\frac{(-1)^n}{n!}\int_{(x,\infty)^n}\det[K(u_i,u_j)].
  • H(k)H^{(k)} takes its continuous diagonal value.
  • pn=Hen/((2π)1/4n!)p_n = \mathrm{He}_n/((2\pi)^{1/4}\sqrt{n!}) with Mathlib's probabilists' Hermite polynomials, equal to the paper's (31).
  • The closed contours Γ\Gamma, Σ\Sigma in H\mathcal H, J\mathcal J are explicit circles satisfying the paper's constraints.
  • Σ∞\Sigma_\infty is the imaginary axis.
  • Residues of a−kφ(a)a^{-k}\varphi(a) are Taylor coefficients.

Ruled-out trivialisations. Five shortcuts would make the statements trivial, and none is available:

  • division by zero on the kernel diagonal is replaced by the diagonal value;
  • the Fredholm series is shown to be 11 on the zero kernel, so it is not identically junk;
  • the conditionally convergent real form of contour integrals is not used;
  • Σ\Sigma is not specialised to a diagonal matrix;
  • the regime is shown satisfiable in a sorry-free check.

Infrastructure. The needed infrastructure is the complex Wishart model, eigenvalues of random Hermitian matrices, Fredholm determinants of integral operators, and contour integrals with uniform estimates. The Hermite and Fredholm layers can be reused for any orthogonal-polynomial ensemble. Contributions welcome:

  • proofs of the elementary milestones ((218)–(219), (287), (295), (288), (292), (299), Lemmas 4.1, 4.2);
  • Lemma 1.1 via Christoffel–Darboux and Andréief;
  • the operator-theoretic step from Hilbert–Schmidt convergence of kernels to convergence of Fredholm series.

Selected references

15 thms1 active userReviewed
ProbabilityRandom Matrix Theory·Captain: mikedeng1

Phase Transition of the Largest Eigenvalue for Nonnull Complex Sample Covariance Matrices 1: Spikes at or below 1+γ⁻¹ Give M^{2/3} Fluctuations of the Largest Eigenvalue with Limit F_kResearch Paper

Motivation

Sample covariance matrices are the basic object of multivariate statistics: principal component analysis, factor models and signal detection all start from the eigenvalues of S=1M∑k=1My⃗ky⃗k ∗S=\frac1M\sum_{k=1}^M\vec y_k\vec y_k^{\,*} built from MM observations of NN variables. When NN is comparable to MM, the largest eigenvalue λ1\lambda_1 of SS is no longer a consistent estimate of the largest population eigenvalue, and the question of when a "spike" in the population covariance is visible in λ1\lambda_1 becomes a question about the law of λ1\lambda_1 at large M,NM,N.

Timeline.

  • 2000–2001: for null covariance Σ=I\Sigma=I, Johansson (complex samples, arXiv:math/9903134) and Johnstone (real samples, doi:10.1214/aos/1009210544) showed that λ1\lambda_1, centred at (1+γ−1)2(1+\gamma^{-1})^2 and scaled by M2/3M^{2/3}, converges to a Tracy–Widom law.
  • 2003: Péché (reference [31] of the 2005 paper) showed that finitely many population eigenvalues below 22 (at M=NM=N) leave this limit unchanged.
  • 2005: Baik, Ben Arous and Péché (doi:10.1214/009117905000000233), for complex Gaussian samples, located the threshold exactly at 1+γ−11+\gamma^{-1} and identified the limit laws on both sides and at the threshold. This transition is now called the BBP phase transition.

This mission formalizes the critical and subcritical side of that transition, Theorem 1.1(a) of the 2005 paper.

Setting

Let g=a+ibg=a+ib with a,ba,b independent real normal variables of mean 00 and variance 1/21/2: a standard complex Gaussian. Let G=(gkj)G=(g_{kj}), 1≤k≤M1\le k\le M, 1≤j≤N1\le j\le N, be i.i.d. standard complex Gaussians. Fix an N×NN\times N unitary matrix UU and positive reals ℓ1,…,ℓN\ell_1,\dots,\ell_N, the population eigenvalues, and put Σ=U diag(ℓ) U∗\Sigma=U\,\mathrm{diag}(\ell)\,U^*. The samples are y⃗k=U diag(ℓj) g⃗k\vec y_k=U\,\mathrm{diag}(\sqrt{\ell_j})\,\vec g_k, mean-zero complex Gaussian vectors with covariance Σ\Sigma. The sample covariance matrix is S=1M∑ky⃗ky⃗k ∗S=\frac1M\sum_k\vec y_k\vec y_k^{\,*} and λ1\lambda_1 is its largest eigenvalue. Write γ=M/N≥1\gamma=\sqrt{M/N}\ge1.

The limit laws are built from the Airy function Ai(u)=12π∫eiua+ia3/3 da\mathrm{Ai}(u)=\frac1{2\pi}\int e^{iua+ia^3/3}\,da, integrated along a contour from ∞e5iπ/6\infty e^{5i\pi/6} to ∞eiπ/6\infty e^{i\pi/6}, and the Airy kernel

A(u,v)=∫0∞Ai(u+z) Ai(z+v) dz.A(u,v)=\int_0^\infty\mathrm{Ai}(u+z)\,\mathrm{Ai}(z+v)\,dz .

For m≥1m\ge1, s(m)(u)=12π∫eiua+ia3/3(ia)−m das^{(m)}(u)=\frac1{2\pi}\int e^{iua+ia^3/3}(ia)^{-m}\,da (with the pole a=0a=0 above the contour) and t(m)(v)=12π∫eiva+ia3/3(−ia)m−1 dat^{(m)}(v)=\frac1{2\pi}\int e^{iva+ia^3/3}(-ia)^{m-1}\,da. The Fredholm determinant of a kernel KK on L2((x,∞))L^2((x,\infty)) is its Fredholm series

det⁡(1−K)=∑n≥0(−1)nn!∫(x,∞)ndet⁡[K(ui,uj)]i,j=1n du,\det(1-K)=\sum_{n\ge0}\frac{(-1)^n}{n!}\int_{(x,\infty)^n}\det[K(u_i,u_j)]_{i,j=1}^n\,du ,

and

Fk(x)=det⁡(1−A−∑m=1ks(m)⊗t(m))L2((x,∞)).F_k(x)=\det\Big(1-A-\sum_{m=1}^k s^{(m)}\otimes t^{(m)}\Big)_{L^2((x,\infty))}.

F0F_0 is the GUE Tracy–Widom distribution and F1=FGOE2F_1=F_{\rm GOE}^2.

Formalization targets

Goal: Theorem 1.1(a)

Fix integers 0≤k≤r0\le k\le r. Let M,N→∞M,N\to\infty with γ∈[1,γ0]\gamma\in[1,\gamma_0], and suppose ℓr+1=⋯=ℓN=1\ell_{r+1}=\dots=\ell_N=1, ℓ1=⋯=ℓk=1+γ−1\ell_1=\dots=\ell_k=1+\gamma^{-1} and ℓk+1,…,ℓr\ell_{k+1},\dots,\ell_r stay in a compact subset of (0,1+γ−1)(0,1+\gamma^{-1}). Then for every real xx,

P((λ1−(1+γ−1)2)γ(1+γ)4/3M2/3≤x)→Fk(x).\mathbb P\Big(\big(\lambda_1-(1+\gamma^{-1})^2\big)\frac{\gamma}{(1+\gamma)^{4/3}}M^{2/3}\le x\Big)\to F_k(x).

The goal leaves UU arbitrary and allows γ\gamma to vary inside [1,γ0][1,\gamma_0] along the sequence. A companion item states Corollary 1.1(a): λ1−(1+γ−1)2→0\lambda_1-(1+\gamma^{-1})^2\to0 in probability.

Milestones

  1. The Airy equation and the identity of the two forms (11), (12) of the Airy kernel.
  2. Lemma 3.3: FkF_k is well defined, and s(m)s^{(m)} has the closed form (203).
  3. The eigenvalue density (61) and Andréief's identity (65).
  4. Hankel's formula (75).
  5. Proposition 2.1: the exact identity P(λ1≤ξ)=det⁡(1−KM,N)L2((ξ,∞))\mathbb P(\lambda_1\le\xi)=\det(1-K_{M,N})_{L^2((\xi,\infty))} for a double contour integral kernel.
  6. The double critical point (109), (111) of the phase function f(z)=−μ(z−q)+log⁡z−γ−2log⁡(1−z)f(z)=-\mu(z-q)+\log z-\gamma^{-2}\log(1-z).
  7. The descent Lemmas 3.1 and 3.2 along explicit contour pieces.
  8. Proposition 3.1: convergence of the rescaled contour integrals H,J\mathcal H,\mathcal J at rate M−1/3M^{-1/3} with exponential tails.
  9. The kernel identity (200).

Significance

Theorem 1.1(a) shows that 1+γ−11+\gamma^{-1} is the exact threshold. Spikes strictly below it do not change the Tracy–Widom limit of λ1\lambda_1. kk spikes exactly at it produce a new family of limit laws FkF_k on the same M2/3M^{2/3} scale. Together with part (b), where λ1\lambda_1 separates and fluctuates on the scale M−1/2M^{-1/2}, it gives the first complete description of the transition. It is the reference point for spiked-model results on detection limits in PCA, for the real case (Bloemendal–Virág, Mo) and for finite-rank perturbations of Wigner matrices (Péché, Féral–Péché).

The paper's proof is complete and has been in the literature since 2005. No part of it is machine-checked. The mission produces:

  • a formal statement of the theorem;
  • formal definitions of the Airy function by its contour integral, of the Airy kernel and of Fredholm determinants as Fredholm series;
  • the exact finite-NN determinantal formula of Proposition 2.1;
  • the uniform steepest-descent estimates;
  • formal statements of the classical identities used along the way (Andréief, Hankel).

Difficulty

The obvious approach is to compute the law of λ1\lambda_1 from the eigenvalue density, which is explicit (61). It fails because the density is an NN-fold integral whose integrand is a signed determinant, so no direct limit exists. The paper converts it into a Fredholm determinant of a double contour integral kernel. Two steps then carry the difficulty.

First, the steepest-descent analysis. With kk spikes at 1+γ−11+\gamma^{-1}, the poles of the integrand sit exactly at the double critical point pc=γ/(γ+1)p_c=\gamma/(\gamma+1) of the phase function. The contour cannot pass through the critical point and must enclose these poles, so it has to be routed at distance of order M−1/3M^{-1/3} to the left of pcp_c. All estimates must be uniform in γ\gamma and in the remaining spikes.

Second, the passage from kernel convergence to convergence of Fredholm determinants. It needs bounds strong enough to control every term of the Fredholm series, which is what the exponential tails in Proposition 3.1 provide. The functions s(m)s^{(m)} grow polynomially, so even the finiteness of FkF_k (Lemma 3.3) needs an argument.

Formalization scope

Lean encoding:

  • Samples are mean-zero with E y⃗y⃗ ∗=Σ\mathbb E\,\vec y\vec y^{\,*}=\Sigma, S=1M∑ky⃗ky⃗k ∗S=\frac1M\sum_k\vec y_k\vec y_k^{\,*}, and there is no centring by the sample mean. This is the model of the paper's (59) and Proposition 2.1. The printed text on p. 1645 differs in three slips.
  • Σ=U diag(ℓ) U∗\Sigma=U\,\mathrm{diag}(\ell)\,U^* ranges over every unitary UU.
  • λ1\lambda_1 is the largest eigenvalue of the Hermitian matrix SS.
  • The asymptotic regime is written with sequences Mn,NnM_n,N_n, Nn→∞N_n\to\infty and γn∈[1,γ0]\gamma_n\in[1,\gamma_0]. "In a compact subset of (0,1+γ−1)(0,1+\gamma^{-1})" is read with a fixed margin cc: c≤ℓj≤1+γn−1−cc\le\ell_j\le1+\gamma_n^{-1}-c.
  • Indices are 00-based.
  • Exponents 2/32/3, 4/34/3, 1/31/3 are real powers of positive reals.
  • FkF_k is defined as the Fredholm series of the kernel A+∑ms(m)⊗t(m)A+\sum_m s^{(m)}\otimes t^{(m)}, the paper's (201). The paper proves that this equals its Definition 1.1.
  • Contour integrals are Bochner integrals along two-ray broken lines, where the integrands decay like e−t3/3e^{-t^3/3}. Closed contours are circles with real centres.

Trivializing formalizations ruled out:

  • The Airy kernel is defined by (12), never by the divided difference (11), whose diagonal would be the junk value 00.
  • Ai is never written as the real integral 1π∫0∞cos⁡(t3/3+ut) dt\frac1\pi\int_0^\infty\cos(t^3/3+ut)\,dt, which is not Lebesgue integrable and would be 00.
  • A non-summable Fredholm series would be 00, so summability is a milestone.
  • The goal quantifies over every unitary UU and every admissible sequence, so it does not specialize Σ\Sigma. Its hypotheses are satisfiable, for example by Mn=NnM_n=N_n, ℓ≡1\ell\equiv1, r=k=0r=k=0.

Infrastructure needed and reusable:

  • the Airy function and its decay;
  • trace-class or Hadamard-bound control of Fredholm series;
  • the complex Wishart eigenvalue density, which needs the Harish-Chandra–Itzykson–Zuber integral;
  • Andréief's identity;
  • steepest-descent estimates for contour integrals.

The Fredholm-determinant layer and the Airy function are reusable in any Tracy–Widom result. Andréief's identity and Hankel's formula are reusable well beyond random matrices.

Contributions welcome: proofs of any milestone, and lemmas that bound Fredholm series by Hadamard's inequality.

Selected references

  • J. Baik, G. Ben Arous, S. Péché, Phase transition of the largest eigenvalue for nonnull complex sample covariance matrices, Ann. Probab. 33(5) (2005), 1643–1697. https://doi.org/10.1214/009117905000000233
  • K. Johansson, Shape fluctuations and random matrices, Comm. Math. Phys. 209 (2000), 437–476. https://arxiv.org/abs/math/9903134
  • I. M. Johnstone, On the distribution of the largest eigenvalue in principal components analysis, Ann. Statist. 29 (2001), 295–327. https://doi.org/10.1214/aos/1009210544
  • C. A. Tracy, H. Widom, Level-spacing distributions and the Airy kernel, Comm. Math. Phys. 159 (1994), 151–174. https://arxiv.org/abs/hep-th/9211141
  • C. Andréief, Note sur une relation entre les intégrales définies des produits des fonctions, Mém. Soc. Sci. Phys. Nat. Bordeaux 2 (1883), 1–14.
15 thms1 active userReviewed
Control TheoryOperations Research·Captain: mikedeng1

On Minimizing the Ruin Probability by Investment and Reinsurance II: Equation (5) for g = f′ Has a Unique Strictly Decreasing Solution on [0, ∞)Research Paper

Motivation

An insurance company whose surplus falls below zero is ruined. The probability of ruin is the classical measure of solvency risk in actuarial mathematics. A company can lower it in two ways: it can invest part of its surplus in a risky asset, and it can pass part of each claim to a reinsurer in exchange for part of the premium. Which mix of investment and reinsurance minimises the probability of ruin is a stochastic control problem. It is studied in risk theory and in applied probability, and it is a model case for control problems with jumps.

Hipp and Plum (2000) solved the problem with investment alone. They wrote down the Hamilton–Jacobi–Bellman (HJB) equation and showed that it has a smooth solution. H. Schmidli (2002) added proportional reinsurance. He proved a verification theorem (his Theorem 1) and an existence theorem (his Theorem 2) for the combined problem. This mission formalizes the existence theorem and the analytic statements it rests on.

Setting

Claims arrive as a Poisson process with rate λ>0\lambda>0. The claim sizes YY are independent with distribution function GG, where G(0)=0G(0)=0 and GG is continuous. The insurer collects premiums at rate c>0c>0. A risky asset follows a geometric Brownian motion with drift μ>0\mu>0 and volatility σ>0\sigma>0. Under proportional reinsurance with retention level b∈[0,1]b\in[0,1], the insurer pays the fraction bYbY of each claim and pays the reinsurer a premium at rate c(b)c(b). The function c(b)c(b) is decreasing and continuous, c(1)=0c(1)=0, lim inf⁡b↑1c(b)/(1−b)>0\liminf_{b\uparrow1}c(b)/(1-b)>0, and there is b‾>0\underline b>0 with c(b)>cc(b)>c for b<b‾b<\underline b and c(b)≤cc(b)\le c for b≥b‾b\ge\underline b. In particular, full reinsurance costs more than the premium income.

Write ff for an unnormalised survival probability, with f(u)=0f(u)=0 for u<0u<0. The HJB equation (1) of the problem is

sup⁡b∈[0,1]sup⁡A≥0[12σ2A2f′′(u)+(c−c(b)+μA)f′(u)+λ(E[f(u−bY)]−f(u))]=0,\sup_{b\in[0,1]}\sup_{A\ge0}\Big[\tfrac12\sigma^2A^2f''(u)+\big(c-c(b)+\mu A\big)f'(u)+\lambda\big(\mathbb E[f(u-bY)]-f(u)\big)\Big]=0 ,

where AA is the amount invested. Eliminating AA and substituting g=f′g=f' turns (1) into the integral equation (5):

g(u)=1μ22σ2∫0udxDg(x)+cλ,g(u)=\frac{1}{\dfrac{\mu^2}{2\sigma^2}\displaystyle\int_0^u\frac{dx}{D_g(x)}+\dfrac{c}{\lambda}}, Dg(x)=inf⁡b∈[0,1][λ(1−G(x/b)+∫0x(1−G((x−z)/b))g(z) dz)−(c−c(b))g(x)].D_g(x)=\inf_{b\in[0,1]}\Big[\lambda\Big(1-G(x/b)+\int_0^x\big(1-G((x-z)/b)\big)g(z)\,dz\Big)-\big(c-c(b)\big)g(x)\Big].

Condition (6) at uu is Dg(u)>0D_g(u)>0. In Lean, ReinsPremium, ClaimLaw, tail, den (=Dg=D_g), SolvesEq5On, H and SolvesHJB (equation (1)) live in the shared module SchmidliRuin.Verif.Setting; HasBoundedDensity, Cond6, SolvesEq3At and SolvesHJBAtZero live in SchmidliRuin.Exist.Setting.

Formalization targets

Goal: Theorem 2 (p. 900)

If GG has a bounded density, then

∃! g:[0,∞)→R strictly decreasing, solving (5) on [0,∞).\exists!\ g:[0,\infty)\to\mathbb R\ \text{strictly decreasing, solving (5) on }[0,\infty).

Lean states this as two conjuncts: existence, and equality on [0,∞)[0,\infty) of any two strictly decreasing solutions.

Milestones, in attack order

  1. Lemma 3 (p. 894). For a solution ff of (3) on [0,η)[0,\eta), the optimal retention is b∗(u)=1b^*(u)=1 for small uu: it is optimal not to reinsure small capital.
  2. Lemma 4 (p. 898). Under a bounded density, (5) has a solution on some [0,ε)[0,\varepsilon), with g(u)=λ/c−αu+o(u)g(u)=\lambda/c-\alpha\sqrt u+o(\sqrt u) and α=λμ/(σc3/2)\alpha=\lambda\mu/(\sigma c^{3/2}).
  3. Condition (6) near 00 (pp. 898–899): such a local solution satisfies Dg(u)>0D_g(u)>0 for small u>0u>0.
  4. Lemma 5 (p. 899). A decreasing solution on [0,u0)[0,u_0) with (6) on (0,u0)(0,u_0) extends to [0,u0][0,u_0], and (6) holds at u0u_0.
  5. Continuation (proof of Theorem 2, p. 901). A solution with (6) on (0,u0](0,u_0] continues to [0,u0+η)[0,u_0+\eta) with (6).
  6. Theorem 1, second sentence (p. 896). For a decreasing solution gg of (5), f(x)=1+∫0xgf(x)=1+\int_0^xg is a strictly increasing solution of (1), twice continuously differentiable on (0,∞)(0,\infty).
  7. Theorem 1, last sentence (p. 896). There is at most one strictly increasing, twice continuously differentiable solution of (1) with f(0)=1f(0)=1.

Significance

The existence theorem completes the dynamic-programming solution of the problem. By the verification theorem, f=1+∫0⋅gf=1+\int_0^\cdot g divided by f(∞)f(\infty) is the maximal survival probability δ(u)\delta(u). The maximisers of the HJB equation define the optimal feedback strategy: the investment A∗(u)=−μf′(u)/(σ2f′′(u))A^*(u)=-\mu f'(u)/(\sigma^2f''(u)) and the retention level b∗(u)b^*(u). Without Theorem 2 the verification theorem would be a statement about a function that might not exist. Equation (5) is also the basis of the paper's numerical scheme (§5), which iterates (5) to compute δ\delta and the optimal strategies.

Theorem 2 has a published proof. As far as is known, none of the results above has a machine-checked proof, and nothing on Prove2Me states them. The work is to formalize the published argument. This takes the local existence result of Hipp and Plum, which the paper cites rather than reproves, and a continuation argument for a nonlinear Volterra-type equation whose kernel is an infimum over a control parameter. Milestones 6 and 7 are the purely analytic content of the verification theorem that the uniqueness part of Theorem 2 uses. The paper derives milestone 7 stochastically, and an analytic proof is equally welcome.

Difficulty

The denominator Dg(x)D_g(x) vanishes at x=0x=0: Dg(0)=λ−c g(0)=0D_g(0)=\lambda-c\,g(0)=0, because g(0)=λ/cg(0)=\lambda/c. The integral in (5) is therefore improper at the origin. A Picard iteration started from a constant does not work, because it does not control ∫0udx/Dg(x)\int_0^u dx/D_g(x). One needs the exact square-root rate Dg(x)≍xD_g(x)\asymp\sqrt x, and Lemma 4 obtains it only through Lemma 3 (no reinsurance near 00) and the Hipp–Plum analysis of the reinsurance-free equation. Lemma 4's proof in the paper is a two-line citation, so a solver must formalize that local existence result.

The second difficulty is continuation. A solution can be continued as long as condition (6) holds, and Lemma 5 has to exclude that (6) degenerates at a finite endpoint. There the infimum over bb interacts with the vanishing of gg. The paper's argument uses a Gronwall estimate and the shape of c(b)c(b) around b‾\underline b, and the minimiser bb in DgD_g need not be unique or continuous.

Formalization scope

  • Model data. c,λ,μ,σc,\lambda,\mu,\sigma are real parameters, all strictly positive. The claim law is a probability measure ν\nu on R\mathbb R, with G=G= cdf ν, ν((−∞,0])=0\nu((-\infty,0])=0 and GG continuous. "Bounded density" means ν\nu has a measurable density with values in [0,C][0,C]. E[h(u−bY)]\mathbb E[h(u-bY)] is ∫h(u−by) dν(y)\int h(u-by)\,d\nu(y).

  • Premium. c(b)c(b) is a real function, used on [0,1][0,1]. The condition lim inf⁡b↑1c(b)/(1−b)>0\liminf_{b\uparrow1}c(b)/(1-b)>0 is the lower bound c(b)≥κ(1−b)c(b)\ge\kappa(1-b) near 11, which is equivalent. A real-valued cc excludes the case c(0)=∞c(0)=\infty that the paper allows when E[Y]<∞\mathbb E[Y]<\infty.

  • Conventions.

    • 1−G(x/b)1-G(x/b) at b=0b=0 is P[0⋅Y>x]=0\mathbb P[0\cdot Y>x]=0; it is computed by tail, never by Lean's x/0=0x/0=0.
    • "gg solves (5) at uu" includes that the integral exists: gg is integrable on [0,u][0,u], Dg≠0D_g\ne0 on (0,u)(0,u), and 1/Dg1/D_g is integrable on [0,u][0,u].
    • Every supremum of the paper is a least upper bound (IsLUB … 0). Lean's sSup would return 00 on an unbounded family, for example when f′′≥0f''\ge0, and that would make "ff solves (1)" true by accident.
    • Uniqueness is equality on [0,∞)[0,\infty). The values of gg off [0,∞)[0,\infty) are free, so a unique-existence quantifier over R→R\mathbb R\to\mathbb R would be false.
    • "Twice continuously differentiable" is read on (0,∞)(0,\infty), since f′′(0+)=−∞f''(0+)=-\infty (p. 895). At u=0u=0, (1) and (3) are taken in the boundary form sup⁡b[(c−c(b))f′(0)+λ(Ef(−bY)−f(0))]=0\sup_b[(c-c(b))f'(0)+\lambda(\mathbb E f(-bY)-f(0))]=0, with the right derivative f′(0)f'(0).
    • λ\lambda and cc are general. §4 sets λ=c=1\lambda=c=1 by a change of units.

  • Trivialising readings ruled out.

    • Encoding (5) with an unguarded 1/Dg1/D_g would let a function with a vanishing denominator "solve" (5).
    • Dropping the boundary equation at u=0u=0 from Lemma 3 makes it false: a premium flat near b=0b=0 admits local solutions with b∗≡0b^*\equiv0.

  • Infrastructure needed.

    • existence of the minimiser in DgD_g and continuity of DgD_g in xx;
    • a local existence theorem for singular integral equations in the style of Hipp–Plum;
    • Gronwall's inequality (Mathlib has versions);
    • Banach's fixed-point theorem (ContractingWith).

    The continuation and closure lemmas (milestones 3–5) are reusable for other HJB equations of risk theory with a jump term. Contributions that state and prove intermediate claims of the paper's proofs are welcome as sub-results.

Selected references

10 thms1 active userReviewed
Control TheoryDynamical Systems·Captain: mikedeng1

Small Gain Theorems for Large Scale Systems and Construction of ISS Lyapunov Functions 2: Under the Small Gain Condition Γ_μ ≱ id, an Ω-Path ExistsResearch Paper

Why paths in the positive orthant matter for networks

A large control system is often built from many subsystems Σ1,…,Σn\Sigma_1,\dots,\Sigma_n, each of which is input-to-state stable (ISS) with respect to the states of the others. Whether the interconnection is again ISS is decided by a small gain condition on the matrix of interconnection gains. For two subsystems this goes back to Jiang, Teel and Praly (1994) and to the Lyapunov version of Jiang, Mareels and Wang (1996). For nn subsystems, Dashkovskiy, Rüffer and Wirth formulated the condition as a property Γμ≱id\Gamma_\mu\not\ge\mathrm{id} of a monotone operator on R+n\mathbb R^n_+ (2007). Rüffer's thesis (2007) and the paper on which this mission is based (arXiv:0901.1842, SIAM J. Control Optim. 2010) turned it into a Lyapunov construction.

The construction needs a geometric object: a path σ\sigma in the positive orthant, unbounded in every coordinate, along which the gain operator strictly decreases every component. For a linear gain matrix this is a Perron vector. For nonlinear gains, its existence is the first of the paper's two main results (Theorem 5.2). This mission formalizes that theorem and the lemmas of §8 that prove it. The companion mission formalizes the second main result, the Lyapunov function built from such a path.

Setting

Write R+=[0,∞)\mathbb R_+=[0,\infty). Vectors in R+n\mathbb R^n_+ are compared componentwise: v≤wv\le w means vi≤wiv_i\le w_i for all ii, and v<wv<w means vi<wiv_i<w_i for all ii. A function γ:R+→R+\gamma:\mathbb R_+\to\mathbb R_+ is of class K\mathcal K if it is continuous, strictly increasing and γ(0)=0\gamma(0)=0, and of class K∞\mathcal K_\infty if it is moreover unbounded.

A gain matrix is Γ=(γij)i,j=1n\Gamma=(\gamma_{ij})_{i,j=1}^n with γij∈K∪{0}\gamma_{ij}\in\mathcal K\cup\{0\} and γii≡0\gamma_{ii}\equiv0. A monotone aggregation function (MAF) is a continuous μ:R+n→R+\mu:\mathbb R^n_+\to\mathbb R_+ with μ(s)>0\mu(s)>0 for s≠0s\ne0, μ(x)<μ(y)\mu(x)<\mu(y) whenever x<yx<y, and μ(x)→∞\mu(x)\to\infty as ∥x∥→∞\|x\|\to\infty. Typical examples are sums and maxima. Given MAFs μ1,…,μn\mu_1,\dots,\mu_n, the gain operator is

Γμ(s)i=μi(γi1(s1),…,γin(sn)),s∈R+n.\Gamma_\mu(s)_i=\mu_i\big(\gamma_{i1}(s_1),\dots,\gamma_{in}(s_n)\big),\qquad s\in\mathbb R^n_+ .

The paper assumes from p. 8 on that μi\mu_i, restricted to the coordinates of the nonzero entries of row ii, still has the strict monotonicity (Remark 2.6). The small gain condition (SGC) is Γμ≱id\Gamma_\mu\not\ge\mathrm{id}: for every s≠0s\ne0, at least one component of Γμ(s)\Gamma_\mu(s) is strictly smaller than the corresponding component of ss. The set

Ω(Γμ)={s∈R+n:Γμ(s)<s}\Omega(\Gamma_\mu)=\{s\in\mathbb R^n_+:\Gamma_\mu(s)<s\}

collects the points that every component of Γμ\Gamma_\mu strictly decreases.

An Ω\Omega-path (Definition 5.1) is a continuous σ:R+→R+n\sigma:\mathbb R_+\to\mathbb R^n_+ with every component σi∈K∞\sigma_i\in\mathcal K_\infty such that (i) each σi−1\sigma_i^{-1} is locally Lipschitz on (0,∞)(0,\infty); (ii) on every compact K⊂(0,∞)K\subset(0,\infty) the derivatives of all σi−1\sigma_i^{-1}, where they exist, lie in [c,C][c,C] for constants 0<c<C0<c<C depending on KK only; and (iii) σ(r)∈Ω(Γμ)\sigma(r)\in\Omega(\Gamma_\mu) for all r>0r>0.

Formalization targets

Goal: Theorem 5.2

Let Γ\Gamma be a gain matrix and μ\mu a compatible vector of MAFs. Assume one of: (i) Γμ\Gamma_\mu is linear with spectral radius less than one; (ii) Γ\Gamma is irreducible and Γμ≱id\Gamma_\mu\not\ge\mathrm{id}; (iii) μ=max⁡\mu=\max and Γμ≱id\Gamma_\mu\not\ge\mathrm{id}; (iv) the entries of Γ\Gamma are bounded and Γμ≱id\Gamma_\mu\not\ge\mathrm{id}. Then

∃ σ an Ω-path withΓμ(σ(r))<σ(r)∀r>0.\exists\,\sigma\ \text{an }\Omega\text{-path with}\quad\Gamma_\mu(\sigma(r))<\sigma(r)\quad\forall r>0 .

In cases (i)–(iii) the entries are in K∞∪{0}\mathcal K_\infty\cup\{0\}, and in case (iv) they are in (K∖K∞)∪{0}(\mathcal K\setminus\mathcal K_\infty)\cup\{0\}.

Milestones

The milestones follow §8 in the order the proof uses them.

  • Bounded gains: Lemmas 8.1–8.3, where iterates of a point of Ω\Omega tend to 00 and the polygon through them stays in Ω\Omega; and Proposition 8.4, which is case (iv).
  • Technical lemmas: Lemmas 8.5–8.7 on diagonal operators diag(ρ)\mathrm{diag}(\rho) and the decay set Ψ={s:Γμ(s)≤s}\Psi=\{s:\Gamma_\mu(s)\le s\}.
  • Topological statements: Proposition 8.8, path-connectedness of Ψ\Psi; Proposition 8.10, where Ω\Omega meets every simplex Sr={s:∑si=r}S_r=\{s:\sum s_i=r\}; and Proposition 8.9, where Ψ∞=⋂kΓμk(Ψ)\Psi_\infty=\bigcap_k\Gamma_\mu^k(\Psi) is unbounded.
  • Irreducible case: the scaling step quoted from Rüffer's earlier work, and Theorem 8.11, which is case (ii).
  • Maximum case: Theorem 8.14, case (iii) in its cycle-condition form.
  • Linear case: the Perron step of §8.5, case (i).

Significance

An Ω\Omega-path turns a small gain condition into a Lyapunov function. If each ViV_i is an ISS Lyapunov function of Σi\Sigma_i, then V(x)=max⁡iσi−1(Vi(xi))V(x)=\max_i\sigma_i^{-1}(V_i(x_i)) is one for the network (Theorem 5.3). So Theorem 5.2 is the step that makes the small gain condition a certificate of network stability, and the corollaries of §5–§7 (sums, maxima, neural networks) all pass through it.

The results are published and proved on paper. None is machine-checked: no proof assistant library contains MAFs, gain operators, the sets Ω\Omega and Ψ\Psi, or Ω\Omega-paths. The paper cites three ingredients without proof: Lemma 8.6, Proposition 8.9 and the scaling step of Theorem 8.11. It also gives Theorem 8.14 only as a sketch. Formalizing them closes those gaps in one place.

Difficulty

For bounded gains the problem is easy: far out, every point of a large ray lies in Ω\Omega, and the only work is the descent to the origin. With K∞\mathcal K_\infty entries, Γμ\Gamma_\mu is unbounded and no ray need stay in Ω\Omega. Following the image of a single point fails, because forward iterates go to 00, not to infinity. The paper instead uses backward orbits inside Ψ∞\Psi_\infty. That this set is nonempty and unbounded is a fixed-point argument of Knaster–Kuratowski–Mazurkiewicz type (Propositions 8.9 and 8.10), not a monotonicity argument. A second obstacle is strictness. A backward orbit is only ≤\le-increasing, while Definition 5.1 needs strictly increasing components with derivative bounds. This is where the diagonal scalings of Lemmas 8.6–8.7 enter.

Formalization scope

R+\mathbb R_+ is ℝ≥0 and R+n\mathbb R^n_+ is Fin n → ℝ≥0, with subsystems indexed from 00. The strict order << is a named predicate (SLt), never Lean's < on functions, which means "≤\le and ≠\ne". The small gain condition is ∀ s ≠ 0, ¬ s ≤ T s. The inverses σi−1\sigma_i^{-1} are carried as explicit two-sided inverses, and derivatives are ordinary real derivatives at points r>0r>0 where they exist. Compatibility (Remark 2.6) and γii≡0\gamma_{ii}\equiv0 are hypotheses of every statement about Γμ\Gamma_\mu. Irreducibility is the matrix-power form of p. 12, which Mathlib's Matrix.isIrreducible_iff_exists_pow_pos connects to Matrix.IsIrreducible. The spectral-radius hypothesis says that every complex eigenvalue has modulus <1<1. The 1-norm defines SrS_r.

Hypotheses made explicit or corrected:

  • Theorem 5.2's header types Γ\Gamma in K∞∪{0}\mathcal K_\infty\cup\{0\} while (iv) needs bounded entries, so each case carries its own entry class.
  • Case (iv) is stated as printed, without "no zero rows".
  • Proposition 8.10 prints "T(s)≱sT(s)\not\ge s for all s∈R+ns\in\mathbb R^n_+". No map satisfies this at s=0s=0, so it is stated for s≠0s\ne0.
  • Propositions 8.9 and 8.10 assume n≥1n\ge1.

A path with Γμ(σ(r))≤σ(r)\Gamma_\mu(\sigma(r))\le\sigma(r), or with Lean's < on functions, is not an Ω\Omega-path. Such a reading would make the goal follow from the origin alone, and it is ruled out.

Needed infrastructure: comparison-function calculus (inverses and compositions of K∞\mathcal K_\infty functions), piecewise linear interpolation in R+n\mathbb R^n_+ with Lipschitz inverse bounds, and a KKM-type argument on the simplex. The first two are reusable well beyond this mission. Contributions of any milestone, proofs of the cited ingredients (Lemma 8.6, Proposition 8.9, Proposition 8.10, the scaling step of Theorem 8.11) and a full proof of Theorem 8.14 are welcome.

Selected references

  • S. N. Dashkovskiy, B. S. Rüffer, F. R. Wirth, Small Gain Theorems for Large Scale Systems and Construction of ISS Lyapunov Functions, arXiv:0901.1842v2, 2009; SIAM J. Control Optim. 48(6), 2010. https://arxiv.org/abs/0901.1842 , https://doi.org/10.1137/090746483
  • S. Dashkovskiy, B. S. Rüffer, F. R. Wirth, An ISS small gain theorem for general networks, Math. Control Signals Systems 19 (2007), pp. 93–122.
  • B. S. Rüffer, Monotone dynamical systems, graphs, and stability of large-scale interconnected systems, PhD thesis, Universität Bremen, 2007. http://nbn-resolving.de/urn:nbn:de:gbv:46-diss000109058
  • B. S. Rüffer, Monotone inequalities, dynamical systems, and paths in the positive orthant of Euclidean n-space, Positivity, 2009/2010. https://doi.org/10.1007/s11117-009-0016-5
  • Z.-P. Jiang, I. M. Y. Mareels, Y. Wang, A Lyapunov formulation of the nonlinear small-gain theorem for interconnected ISS systems, Automatica 32 (1996), pp. 1211–1215.
18 thms1 active userReviewed
Control TheoryDynamical Systems·Captain: mikedeng1

Small Gain Theorems for Large Scale Systems and Construction of ISS Lyapunov Functions 1: Rescaling Along an Ω-Path Gives the Network ISS Lyapunov Function maxᵢ σᵢ⁻¹(Vᵢ(xᵢ))Research Paper

Motivation

Large engineered systems — power grids, chemical plants, logistics and communication networks — are usually modelled as many interacting subsystems. A stability certificate for the whole network is rarely available directly, but each subsystem can often be analysed on its own, treating the states of its neighbours as disturbances. Input-to-state stability (ISS), introduced by Sontag (Sontag 1989), is the robustness notion that makes this decomposition work: it bounds the state by a decaying function of the initial condition plus a gain of the input. A small-gain theorem states that if the gains by which the subsystems influence each other are "small" in a suitable sense, the interconnection is again ISS.

Timeline. Jiang, Teel and Praly proved a nonlinear small-gain theorem for two ISS systems in trajectory form (1994), and Jiang, Mareels and Wang gave its Lyapunov version for two subsystems (1996). Dashkovskiy, Rüffer and Wirth extended the trajectory version to nn subsystems with the condition Γ≱id\Gamma\not\ge\mathrm{id} on a nonlinear gain operator (2007). The paper of this mission (arXiv:0901.1842, SIAM J. Control Optim. 48(6), 2010) gives the Lyapunov version for nn subsystems with general monotone aggregation of the gains, and constructs the network's ISS Lyapunov function explicitly.

Setting

The network consists of n≥1n\ge 1 subsystems

Σi: x˙i=fi(x1,…,xn,u),xi∈RNi, u∈RM,\Sigma_i:\ \dot x_i=f_i(x_1,\dots,x_n,u),\qquad x_i\in\mathbb R^{N_i},\ u\in\mathbb R^M,

with overall state x=(x1T,…,xnT)T∈RNx=(x_1^T,\dots,x_n^T)^T\in\mathbb R^N and dynamics x˙=f(x,u)\dot x=f(x,u), f=(f1,…,fn)f=(f_1,\dots,f_n). ∥⋅∥\|\cdot\| is the Euclidean norm.

A function γ:R+→R+\gamma:\mathbb R_+\to\mathbb R_+ is of class K\mathcal K if it is continuous, strictly increasing and γ(0)=0\gamma(0)=0, and of class K∞\mathcal K_\infty if moreover unbounded. A positive definite function α:R+→R+\alpha:\mathbb R_+\to\mathbb R_+ is continuous with α(r)=0\alpha(r)=0 only at r=0r=0. A Lyapunov function candidate V:Rd→R+V:\mathbb R^d\to\mathbb R_+ is continuous, satisfies ψ1(∥x∥)≤V(x)≤ψ2(∥x∥)\psi_1(\|x\|)\le V(x)\le\psi_2(\|x\|) for some ψ1,ψ2∈K∞\psi_1,\psi_2\in\mathcal K_\infty, and is locally Lipschitz away from the origin.

A candidate VV is an ISS Lyapunov function for x˙=f(x,u)\dot x=f(x,u) if there are γ∈K\gamma\in\mathcal K and a positive definite α\alpha with

V(x)≥γ(∥u∥) ⟹ ∇V(x)f(x,u)≤−α(∥x∥)V(x)\ge\gamma(\|u\|)\ \Longrightarrow\ \nabla V(x)f(x,u)\le-\alpha(\|x\|)

at every point of differentiability of VV.

On R+n\mathbb R^n_+, v<wv<w means vi<wiv_i<w_i for every ii. A monotone aggregation function (MAF) μ:R+m→R+\mu:\mathbb R^m_+\to\mathbb R_+ is continuous, positive off the origin, strictly increasing for this strict order, and unbounded as ∥s∥→∞\|s\|\to\infty. Subsystem Σi\Sigma_i has an ISS Lyapunov function ViV_i with gains γij∈K∞∪{0}\gamma_{ij}\in\mathcal K_\infty\cup\{0\}, γiu∈K∪{0}\gamma_{iu}\in\mathcal K\cup\{0\} and MAF μi\mu_i on R+n+1\mathbb R^{n+1}_+ if, wherever ViV_i is differentiable,

Vi(xi)≥μi(γi1(V1(x1)),…,γin(Vn(xn)),γiu(∥u∥)) ⟹ ∇Vi(xi)fi(x,u)≤−αi(∥xi∥).V_i(x_i)\ge\mu_i\big(\gamma_{i1}(V_1(x_1)),\dots,\gamma_{in}(V_n(x_n)),\gamma_{iu}(\|u\|)\big)\ \Longrightarrow\ \nabla V_i(x_i)f_i(x,u)\le-\alpha_i(\|x_i\|).

The diagonal gains vanish, γii≡0\gamma_{ii}\equiv0. The gain operators are

Γ‾μ(s,r)i=μi(γi1(s1),…,γin(sn),γiu(r)),Γμ(s)=Γ‾μ(s,0).\overline\Gamma_\mu(s,r)_i=\mu_i\big(\gamma_{i1}(s_1),\dots,\gamma_{in}(s_n),\gamma_{iu}(r)\big),\qquad\Gamma_\mu(s)=\overline\Gamma_\mu(s,0).

An Ω-path with respect to Γμ\Gamma_\mu is a continuous σ:R+→R+n\sigma:\mathbb R_+\to\mathbb R^n_+ with every σi∈K∞\sigma_i\in\mathcal K_\infty, such that each σi−1\sigma_i^{-1} is locally Lipschitz on (0,∞)(0,\infty), its derivative lies in [c,C][c,C], 0<c<C0<c<C, at its points of differentiability in any compact K⊂(0,∞)K\subset(0,\infty) (constants depending on KK only), and Γμ(σ(r))<σ(r)\Gamma_\mu(\sigma(r))<\sigma(r) for all r>0r>0.

Formalization targets

Goal: Theorem 5.3

Assume each ViV_i is an ISS Lyapunov function for Σi\Sigma_i with gains Γ\Gamma, γiu\gamma_{iu} and MAFs μi\mu_i; σ\sigma is an Ω-path with respect to Γμ\Gamma_\mu; φ∈K∞\varphi\in\mathcal K_\infty satisfies

Γ‾μ(σ(r),φ(r))<σ(r)∀r>0;\overline\Gamma_\mu(\sigma(r),\varphi(r))<\sigma(r)\qquad\forall r>0;

and each fif_i is continuous. Then

V(x)=max⁡i=1,…,nσi−1(Vi(xi))V(x)=\max_{i=1,\dots,n}\sigma_i^{-1}(V_i(x_i))

is an ISS Lyapunov function for the network, with gain φ−1\varphi^{-1}:

V(x)≥φ−1(∥u∥) ⟹ ∇V(x)f(x,u)≤−α(∥x∥)V(x)\ge\varphi^{-1}(\|u\|)\ \Longrightarrow\ \nabla V(x)f(x,u)\le-\alpha(\|x\|)

for a positive definite α\alpha. The rate α\alpha is existential and is not fixed by the statement.

Milestones

The milestones follow the proof on pp. 14–15:

  1. VV is a Lyapunov function candidate.
  2. The maximum rule (5.7) for Clarke generalized gradients.
  3. The chain of inequalities showing that the subsystem trigger holds strictly at every active index.
  4. The Clarke-gradient form (5.8) of the subsystem decrease.
  5. The chain rule for σi−1∘Vi\sigma_i^{-1}\circ V_i, with multipliers bounded away from zero.
  6. Positivity of the rate: active blocks on a sphere stay away from the origin.
  7. The uniform decrease (5.9).

Significance

The result. Theorem 5.3 converts a small-gain condition into an explicit Lyapunov function for the network. Combined with the converse ISS Lyapunov theorem, it gives ISS of the interconnection, and with zero input it gives global asymptotic stability. It covers additive, maximum-type and multiplicative aggregation of gains, and it handles nn subsystems without iterating a two-system result. A second main result of the paper (Theorem 5.2, a separate mission) supplies the Ω-path from the condition Γμ≱id\Gamma_\mu\not\ge\mathrm{id}. Together they reduce the stability of a network to a property of its gain operator.

Formalizing it. The result is proved on paper. As far as we know, no ISS notion, small-gain theorem or monotone aggregation framework has been machine-checked in Lean. This mission produces a Lean statement of the construction, and of its nonsmooth-analysis steps, against which a complete proof can be checked. It also corrects a misprint in the theorem's implication (see Formalization scope).

Difficulty

The function VV is a maximum of rescaled functions and is not differentiable on the set where two indices are active, even when every ViV_i is smooth. The subsystem hypotheses only control derivatives at points where the corresponding ViV_i is differentiable. At a point where VV is differentiable, the active ViV_i may not be. So the obvious argument — differentiate the active branch and apply (2.7) — fails, and the decrease must be transported through generalized gradients. A second obstacle is uniformity: the rate α\alpha must depend on ∥x∥\|x\| alone. This requires the lower derivative bound in the Ω-path definition and a compactness argument on spheres. Dropping the lower bound breaks the theorem, because σi−1\sigma_i^{-1} could flatten and remove the decrease.

Formalization scope

Blocks are EuclideanSpace ℝ (Fin (N i)). The network state is the L2L^2 product PiLp 2 (the Euclidean norm, not the sup norm), and the input is EuclideanSpace ℝ (Fin M). Subsystems are indexed by Fin n (0-based) with n≥1n\ge1. Gains, MAFs, Ω-paths and rates live on ℝ≥0. Lyapunov functions are real-valued with an explicit nonnegativity clause. The strict order on R+n\mathbb R^n_+ is a named predicate, not Lean's Pi <. The inverses σi−1\sigma_i^{-1} and φ−1\varphi^{-1} are explicit arguments with both compositions the identity. Every derivative is guarded by a differentiability hypothesis. Clarke's generalized gradient (2.5) is the published ClarkeGradients.Shared.generalizedGradient on the blocks, and the same definition restated on a general Hilbert space for RN\mathbb R^N and R\mathbb R.

Implicit hypotheses made explicit:

  • Continuity of every fif_i. It is the regularity behind the equivalence of the derivative form (2.4) and the Clarke form (2.6) of the decrease condition, which the proof uses.
  • γii≡0\gamma_{ii}\equiv0. The paper's convention.
  • Compatibility of Γ\Gamma and μ\mu. Remark 2.6, the standing assumption from p. 8 on; it imposes nothing on a zero row of Γ\Gamma.

Corrected statement. The printed implication (5.5) has the trigger V(x)≥max⁡iφ−1(γiu(∥u∥))V(x)\ge\max_i\varphi^{-1}(\gamma_{iu}(\|u\|)). With Γ‾μ\overline\Gamma_\mu as defined in (2.9), and as the paper's corollaries use it, that implication is false. A counterexample is one subsystem x˙=−x+u/6\dot x=-x+u/6 with V1=∣x∣V_1=|x|, γ1u(s)=s/10\gamma_{1u}(s)=s/10, μ1(a,b)=a+2b\mu_1(a,b)=a+2b and σ=φ=id\sigma=\varphi=\mathrm{id}, at x=1x=1, u=10u=10. The proof's chain of inequalities writes φ(r)\varphi(r) where (2.9) gives γiu(φ(r))\gamma_{iu}(\varphi(r)). The goal keeps (2.9) and uses the trigger V(x)≥φ−1(∥u∥)V(x)\ge\varphi^{-1}(\|u\|), under which the proof closes.

The hypotheses are jointly satisfiable. An example is n=2n=2 with Vi(xi)=∥xi∥V_i(x_i)=\|x_i\|, μi=max⁡\mu_i=\max, γ12=γ21=s/4\gamma_{12}=\gamma_{21}=s/4, γiu=s/2\gamma_{iu}=s/2, σ(r)=(r,r)\sigma(r)=(r,r), φ=id\varphi=\mathrm{id} and dynamics fi=−xif_i=-x_i. The conclusion is a decrease inequality at the points of differentiability of VV for an existential positive definite rate, so it cannot be met by a vacuous choice: α\alpha must be positive away from zero. Trajectory-level ISS (Theorem 2.3, cited by the paper) and the corollaries that conclude ISS are out of scope.

Reusable infrastructure: comparison classes, monotone aggregation functions, gain operators and Ω-paths (shared with the Ω-path mission), and the maximum and chain rules for Clarke gradients. Proofs of the nonsmooth calculus milestones are welcome independently of the goal.

Selected references

11 thms1 active userReviewed
Operations ResearchProbabilityStochastic Systems·Captain: mikedeng1

Some Useful Functions for Functional Limit Theorems 2: Addition, Supremum and the Reflecting Barrier Preserve J₁ Convergence of Linearly Centered PathsResearch Paper

Motivation

Queueing models often represent work arriving to and leaving a server by a real-valued input path. The resulting workload cannot fall below a barrier. Functional limit theorems describe what happens to such paths under scaling, but a limit for the input path is useful only when it can be carried through the workload transformation. Ward Whitt’s 1980 paper studies several path transformations that occur in stochastic-process limits and states conditions under which their limits can be computed in Skorohod topologies. Section 6 treats the running supremum and a reflecting barrier, including paths with a linear drift that changes with the scaling index. This mission formalizes the three-regime reflection result, Theorem 6.4, and the source results on its dependency path. Whitt (1980)

The result is already proved in the paper. Its formal Lean statement remains an open proof target here. The mission is therefore concerned with formalizing the known theorem, including its exact jump conditions and convergence modes, rather than proposing a new queueing claim. Whitt (1980), pp. 80–81

Setting

A càdlàg path on a real interval TT is right-continuous and has a limit from the left wherever TT approaches a time from the left. The collection of such real-valued paths is D(T,R)D(T,\mathbb R). For a compact interval [a,b][a,b], the J1J_1 distance between xx and yy allows an increasing homeomorphism λ\lambda of time and measures the larger of its distance from the identity and the uniform distance between xx and y∘λy\circ\lambda. On a general interval, J1J_1 convergence is specified by restrictions to compact subintervals whose endpoints are continuity points of the limit or endpoints of TT. The paper uses complete separable metric spaces for general path-space results; Section 6 specializes to real-valued paths and intervals with 00 as a closed left endpoint. Whitt (1980), pp. 70, 80

For x∈D(T,R)x\in D(T,\mathbb R) and t∈Tt\in T, define the running supremum x↑(t)=sup⁡0≤s≤tx(s)x^{\uparrow}(t)=\sup_{0\le s\le t}x(s) and running infimum x↓(t)=inf⁡0≤s≤tx(s)x^{\downarrow}(t)=\inf_{0\le s\le t}x(s). The reflecting-barrier map is f(x)(t)=x(t)−x↓(t)f(x)(t)=x(t)-x^{\downarrow}(t). This is the paper’s definition: it subtracts the full running infimum. The identity path is e(t)=te(t)=t, and θ\theta denotes the zero path. A path has no positive jumps if x(t)≤x(t−)x(t)\le x(t-) for each t>0t>0 in TT; no negative jumps reverses that inequality. Whitt (1980), pp. 80–81

Formalization targets

The goal is Theorem 6.4. Suppose xn−cne→xx_n-c_ne\to x in J1J_1 and x(0)=0x(0)=0. Its three conclusions are

cn→c  ⟹  f(xn)→f(x+ce)(J1),cn→+∞  ⟹  f(xn)−cne→x(J1),cn→−∞ and x has no positive jumps  ⟹  f(xn)→θ(U).\begin{aligned} c_n\to c &\implies f(x_n)\to f(x+ce) &&(J_1),\\ c_n\to+\infty &\implies f(x_n)-c_ne\to x &&(J_1),\\ c_n\to-\infty\ \text{and }x\text{ has no positive jumps} &\implies f(x_n)\to\theta &&(U). \end{aligned}

Here UU means uniform convergence on every compact subinterval. The goal keeps all three drift regimes together, as the printed theorem does. Its milestones are the finite-partition fact cited from Billingsley, the interval-splitting Lemma 2.2, continuity of addition at limits without shared discontinuities in Theorem 4.1, the running-supremum inequality in Theorem 6.1, the three-regime supremum theorem 6.2, and the paper’s explicit claim that ff is J1J_1-continuous. Whitt (1980), pp. 71, 79–81

Significance

The theorem specifies which output path appears after reflection as the linear centering changes. Finite drift leaves a reflected limit with drift included; large positive drift leaves the centered input limit; large negative drift drives the reflected path uniformly to zero when upward jumps of the limit are excluded. The distinction between J1J_1 and the stronger compact-uniform mode in the last case is part of the result. These statements make the paper’s barrier transformation usable when an input-process limit is already known. Whitt (1980), Theorem 6.4

A completed formal development would establish reusable path-space components: a precise J1J_1 convergence interface for real intervals, a theorem about addition with disjoint discontinuities, and continuity properties of running extrema and reflection. The present Lean items state these results and compile with proof placeholders. No machine-checked proof of these mission theorems is claimed here. The milestone list follows the claims Whitt states or cites, so later proofs can be attached to the same mathematical targets. Whitt (1980), §§2, 4, 6

Difficulty

A uniform estimate alone does not establish a J1J_1 limit: separate paths may converge using different changes of time, and addition can fail when the limiting paths jump together. Whitt’s Theorem 4.1 gives continuity precisely at pairs with disjoint discontinuity sets. In the reflection theorem, a linearly growing drift also changes which extrema matter, and the sign of a jump decides whether the large-drift conclusion can hold. The negative-drift conclusion asks for compact-uniform convergence, which is stronger than merely retaining J1J_1 convergence. These are real constraints on the statement; dropping a jump condition or replacing UU by J1J_1 changes the theorem. Whitt (1980), pp. 78–81

Formalization scope

Paths are total functions R→S\mathbb R\to S, but only their values on the stated interval count. The Lean definitions require càdlàg membership of both prelimit and limit paths in each J1J_1 convergence claim. A time change on [a,b][a,b] is strictly increasing, continuous, and onto; this represents the paper’s increasing homeomorphism. Uniform and J1J_1 distances take values in the extended nonnegative reals, so an unbounded supremum cannot silently become zero. Continuity points use continuity within TT, and the discontinuity set likewise contains only points of TT. Sequential convergence is used because the paper’s J1J_1 spaces are metrizable. These choices encode the paper’s path-space conventions rather than imposing conditions on values outside TT. Whitt (1980), §§2, 4, 6

The compact form of Theorem 6.1 uses metric (2.1); the noncompact metric (2.2) is outside this mission’s definition layer. Theorem 4.1 retains the paper’s complete separable metric-space setting and metric compatibility of addition. Its measurability clause is omitted: this mission does not construct the Borel measurable space of D(T,S)D(T,S), and a product measurable structure on all total functions would express a different claim. The source’s f(x)=x−x↓f(x)=x-x^{\downarrow} is used on both prelimit and limit paths; it is not replaced by a clipped running infimum. Whitt (1980), pp. 70, 78–81

The definition layer, the addition theorem, the running-extremum results, and the barrier continuity statement are welcome proof targets. The theorem’s centered-path hypothesis remains a genuine J1J_1 convergence assertion, and the jump conditions apply to the limit path only. A vacuous convergence predicate or an independently assumed conclusion would not represent this mission’s goal.

Selected references

  • Ward Whitt, Some Useful Functions for Functional Limit Theorems, Mathematics of Operations Research 5(1), 1980, pp. 67–85. DOI: 10.1287/moor.5.1.67
9 thms1 active userReviewed
Operations ResearchProbabilityStochastic Systems·Captain: mikedeng1

Some Useful Functions for Functional Limit Theorems 4: Time Reversal Is a J₁ Isometry and Reversal from the Origin Is 2-LipschitzResearch Paper

Why time reversal matters

Functional limit theorems describe the behavior of entire time-indexed paths under scaling. In queueing and other stochastic models, a path of departures, workload, or accumulated input may be related to another path by reversing a finite observation window. To carry a limit theorem through that change of viewpoint, one needs to know how reversal acts on the topology of the path space. Ward Whitt's 1980 paper studies composition, reflection, first passage, and time reversal as maps that transfer functional limit theorems to derived processes (Whitt 1980).

The time-reversal result is a precise metric statement. Ordinary reversal preserves the Skorohod J1J_1 distance exactly. A version shifted to begin at the group identity satisfies a bound with constant two. These facts give continuity and, when the random paths satisfy the hypotheses, make reversal available to the continuous mapping theorem. Whitt's introduction explains how deterministic path continuity connects to stochastic-process limits (Whitt 1980, pp. 67–69).

Paths, distances, and reversal

Let SS be a complete separable metric group, written additively, with identity 00 and metric mm. The metric is translation invariant: moving both points by the same group element leaves their distance unchanged. Let DD contain the càdlàg paths x:[0,1]→Sx:[0,1]\to S, meaning paths that are right continuous and possess left limits. Section 8 additionally requires x(1)=x(1−)x(1)=x(1-), so the terminal value agrees with the value approached from earlier times. Let Dθ={x∈D:x(0)=0}D_\theta=\{x\in D:x(0)=0\}. These are the spaces Whitt fixes for time reversal (Whitt 1980, p. 83).

The uniform distance is ρ(x,y)=sup⁡0≤t≤1m(x(t),y(t))\rho(x,y)=\sup_{0\le t\le1}m(x(t),y(t)). A time change λ∈Λ\lambda\in\Lambda is an increasing homeomorphism of [0,1][0,1] onto itself; e(t)=te(t)=t is the identity time change. The J1J_1 distance used in the paper is

d(x,y)=inf⁡λ∈Λmax⁡{ρ(λ,e),ρ(x,y∘λ)}.d(x,y)=\inf_{\lambda\in\Lambda} \max\{\rho(\lambda,e),\rho(x,y\circ\lambda)\}.

Two paths may be close when their values can be matched after a small distortion of time. This is the paper's equation (2.1), rather than an unspecified equivalent J1J_1 metric (Whitt 1980, p. 70).

The reverse-time map reads the left limit at the reflected time:

R(x)(t)={x((1−t)−),0≤t<1,x(0),t=1,r(x)(t)=R(x)(t)−x(1).R(x)(t)= \begin{cases} x((1-t)-),&0\le t<1,\\ x(0),&t=1, \end{cases} \qquad r(x)(t)=R(x)(t)-x(1).

The left limit is essential: the direct value x(1−t)x(1-t) places jumps on the wrong side and generally does not give a right-continuous reverse path. The terminal convention gives R(x)(0)=x(1)R(x)(0)=x(1), so r(x)(0)=0r(x)(0)=0. Whitt also uses the reflected time change (−r)(λ)(t)=1−λ(1−t)(-r)(\lambda)(t)=1-\lambda(1-t) in the proof (Whitt 1980, pp. 83–84).

Formalization targets

The goal is Whitt's Theorem 8.1. For every x,y∈Dx,y\in D,

d(Rx,Ry)=d(x,y),d(rx,ry)≤2d(x,y).d(Rx,Ry)=d(x,y),\qquad d(rx,ry)\le 2d(x,y).

The second inequality also applies when both paths lie in DθD_\theta, since Dθ⊆DD_\theta\subseteq D. The constant is the paper's printed constant, not a parameter to optimize in this mission (Whitt 1980, Theorem 8.1, p. 83).

The milestones record four claims from the theorem's proof: reversal preserves its path spaces and has inverse behavior on its natural domains; reflected time changes stay in Λ\Lambda; reversal obeys exact and bounded uniform-distance relations; and reversal interacts with time changes through (−r)(λ)(-r)(\lambda). Their descriptions reproduce the printed proof sentences. The proof calls the time-change cost a “minimum” once, although equation (2.1) and the displayed calculation use a maximum. The formal target follows equation (2.1) (Whitt 1980, pp. 70, 84).

What the result gives

An isometry preserves every J1J_1 distance, so ordinary reversal preserves convergent and Cauchy sequences in this metric. The bound for rr makes shifted reversal Lipschitz and therefore continuous. A functional limit theorem for input paths can then be translated into one for the corresponding reversed paths whenever the path-space hypotheses hold. The result is already proved in Whitt's paper; the open work here is a machine-checked development of its definitions, supporting claims, and metric theorem.

Formalizing the result also creates reusable interfaces for endpoint-constrained càdlàg paths, left-limit reversal, uniform path distance, and reflected time changes. Those interfaces may support later statements about reversed stochastic models. This mission does not assert weak convergence of probability laws or Borel measurability; those would require a separate measurable-space development for DD.

Mathematical difficulty

The immediate idea t↦x(1−t)t\mapsto x(1-t) does not preserve càdlàg paths at jumps: a right-continuous jump becomes left-continuous. The correction uses left limits, but endpoint behavior then matters. Without x(1)=x(1−)x(1)=x(1-), the shifted reverse path need not start at the identity. The J1J_1 assertion also concerns an infimum over all allowed time changes, so a uniform-distance statement alone does not establish the theorem. These are the points at which reflection of the time axis becomes a claim about the precise path-space topology (Whitt 1980, pp. 83–84).

Formalization scope

Lean represents paths as total functions R→S\mathbb R\to S; all path conditions, metrics, and equality claims read only [0,1][0,1]. Càdlàg membership requires right continuity and left limits within the interval, with x(1)=x(1−)x(1)=x(1-) included in DD. Completeness and separability are explicit because the paper calls SS a complete separable metric space. The additive metric group is represented by an additive commutative group with an explicit translation-invariance hypothesis. This chooses the commutative reading exemplified by S=RkS=\mathbb R^k; the paper uses additive notation but does not separately state commutativity.

The paper's Λ\Lambda is encoded by strict increase, continuity, and surjectivity on [0,1][0,1], which characterize increasing homeomorphisms there. The paper's dd is equation (2.1) on both sides of the goal. Lean uses extended nonnegative distances for ρ\rho and dd, avoiding the default value a real supremum can assign to an empty or unbounded set. The claims do not become trivial by dropping DD membership: it is an explicit hypothesis, and the zero path over R\mathbb R satisfies it. A local, sorry-free check confirms that instance. Two easier statements are excluded on purpose: the goal is stated for the J1J_1 distance dd, not the uniform distance ρ\rho, and RR reads the left limit x((1−t)−)x((1-t)-), not the value x(1−t)x(1-t).

The proof's first sentence says the maps are one-to-one and onto. The map r:D→Dθr:D\to D_\theta forgets an additive offset and is not injective on all of DD; the formal milestone expresses involution for RR on DD and for the restriction of rr to DθD_\theta. One identity printed for rr with x∈Dθx\in D_\theta also holds for every x∈Dx\in D; the formal milestone uses that broader domain and says so in its item description. Contributions are welcome for the left-limit and time-change infrastructure as well as the four listed statements and the goal.

Selected references

  • Ward Whitt, Some Useful Functions for Functional Limit Theorems, Mathematics of Operations Research 5(1), 1980, pp. 67–85. DOI: 10.1287/moor.5.1.67.
7 thms1 active userReviewed
Operations ResearchOptimizationStochastic Systems·Captain: mikedeng1

Dynamic Scheduling with Convex Delay Costs: The Generalized cμ Rule: Policies Equalizing the Indices μ_k c_k(W_k/ρ_k) Attain the Heavy-Traffic Lower Bound on Cumulative Delay CostResearch Paper

Motivation

A single server shared by several classes of jobs must decide, at every moment, which class to work on. When each class kk incurs a linear delay cost ckc_k per unit of waiting time and needs mean service time 1/μk1/\mu_k, the classical cμc\mu rule (serve the waiting class with the largest ckμkc_k\mu_k) minimizes expected cost in many settings, from the M/G/1 queue to discrete-time models (Buyukkoc, Varaiya and Walrand, Adv. Appl. Probab. 1985). Linear costs are a strong restriction: in telecommunications, manufacturing and service systems the penalty for delay often grows faster than linearly, and with convex costs the static priority order of the cμc\mu rule is no longer optimal.

Van Mieghem (Ann. Appl. Probab. 1995) proposed the generalized cμc\mu rule: with nondecreasing convex delay costs CkC_k and marginal costs ck=Ck′c_k = C_k', serve the class with the largest index μkck(⋅)\mu_k c_k(\cdot) evaluated at its current delay or workload. The paper proves that, in heavy traffic, this dynamic index policy is asymptotically optimal among all scheduling policies, including policies whose scaled workloads do not converge. This mission formalizes that result and the chain of propositions it rests on.

Setting

There are dd job classes. In the nnth system, the iith class-kk job arrives after an interarrival time uk,in>0u^n_{k,i}>0 and needs service vk,in≥0v^n_{k,i}\ge 0. Akn(t)A^n_k(t) counts class-kk arrivals in [0,t][0,t] and Skn(x)S^n_k(x) counts class-kk completions within xx units of server time. A policy is an allocation Tn=(Tkn)T^n=(T^n_k), where Tkn(t)T^n_k(t) is the time in [0,t][0,t] spent on class kk. From it come the headcount Nkn=Akn−Skn∘TknN^n_k = A^n_k - S^n_k\circ T^n_k, the workload Wkn(t)=Vkn(Akn(t))−Tkn(t)W^n_k(t) = V^n_k(A^n_k(t)) - T^n_k(t) (work present in class kk), the class-FIFO delay τkn(t)=inf⁡{s≥0:Wkn(t)≤Tkn(t+s)−Tkn(t)}\tau^n_k(t)=\inf\{s\ge0: W^n_k(t)\le T^n_k(t+s)-T^n_k(t)\} of a job arriving at tt, and the cumulative cost Jn(t)=∑k∑i≤Akn(t)Ckn(τk,in)J^n(t)=\sum_k\sum_{i\le A^n_k(t)} C^n_k(\tau^n_{k,i}). Feasible policies are continuous, nondecreasing and work conserving.

The nnth system runs on [0,n][0,n] and is studied at the diffusion scale: W~kn(t)=Wkn(nt)/n\tilde W^n_k(t)=W^n_k(nt)/\sqrt n, N~kn\tilde N^n_k, τ~kn\tilde\tau^n_k likewise, and J~n(t)=Jn(nt)/n\tilde J^n(t)=J^n(nt)/n. Arrival and service processes expand as An(nt)=nAˉn(t)+n A~n(t)+o(n)A^n(nt)=n\bar A^n(t)+\sqrt n\,\tilde A^n(t)+o(\sqrt n) and Sn(nt)=nSˉn(t)+n S~n(t)+o(n)S^n(nt)=n\bar S^n(t)+\sqrt n\,\tilde S^n(t)+o(\sqrt n). Assumption 1 asks that these terms converge, with rates λ=Aˉ∗′>0\lambda=\bar A^{*\prime}>0, μ=Sˉ∗′>0\mu=\bar S^{*\prime}>0, and that the system is in heavy traffic: n(R+n−e)→c~∗\sqrt n(R^n_+-e)\to\tilde c^*, where Rkn=(Sˉkn)−1∘AˉknR^n_k=(\bar S^n_k)^{-1}\circ\bar A^n_k and ρk=λk/μk\rho_k=\lambda_k/\mu_k is the traffic intensity. Assumption 2 asks that the costs scale, Cn(n ⋅)→C∗(⋅)C^n(\sqrt n\,\cdot)\to C^*(\cdot), and Assumption 3 that C∗C^* be strictly convex and C1\mathcal C^1.

The scaled total workload has a policy-independent limit W~+∗=φ(L~+∗+c~∗)\tilde W^*_+=\varphi(\tilde L^*_++\tilde c^*), with φ\varphi the one-dimensional reflection map. The key static problem splits a total yy among classes:

g∘y(t)=arg⁡min⁡x∈R+d, ∑kxk=y(t) ∑kλk(t) Ck∗(xkρk(t)).(43)g\circ y(t)=\arg\min_{x\in\mathbb R^d_+,\ \sum_k x_k=y(t)}\ \sum_k\lambda_k(t)\,C^*_k\Big(\frac{x_k}{\rho_k(t)}\Big). \tag{43}

Formalization targets

Goal: Proposition 7

Under Assumptions 1–3, for feasible policies with

max⁡k,l∥μkck∗(W~knρk)−μlcl∗(W~lnρl)∥→0,(51)\max_{k,l}\Big\|\mu_kc^*_k\Big(\frac{\tilde W^n_k}{\rho_k}\Big)-\mu_lc^*_l\Big(\frac{\tilde W^n_l}{\rho_l}\Big)\Big\|\to0, \tag{51}

the costs and delays converge,

J~n→J~∗=∑k∫λkCk∗([g∘W~+∗]kρk)dt,τ~n→g∘W~+∗ρ.(52–53)\tilde J^n\to\tilde J^*=\sum_k\int\lambda_kC^*_k\Big(\frac{[g\circ\tilde W^*_+]_k}{\rho_k}\Big)dt,\qquad \tilde\tau^n\to\frac{g\circ\tilde W^*_+}{\rho}. \tag{52–53}

Milestones

Lemma 1 and Proposition 2 (jumps (33)–(34), first-order allocation (27), total workload (32), boundedness, equivalences (35)); Proposition 3 (μkW~kn−N~kn→0\mu_k\tilde W^n_k-\tilde N^n_k\to0); Proposition 4 (Little's law); Proposition 5 (converging policies); uniqueness and continuity of gg (§4.1); the Kuhn–Tucker characterization (46)–(50); and Proposition 6, the lower bound

lim inf⁡nJ~n(t)≥J~∗(t)for every feasible policy sequence.(44)\liminf_n\tilde J^n(t)\ge\tilde J^*(t)\qquad\text{for every feasible policy sequence.}\tag{44}

Proposition 6 is what makes Proposition 7 an optimality statement; it is a separate milestone and not part of the goal.

Significance

The result. Proposition 7 identifies a simple, myopic index rule that is optimal at the diffusion scale for every time simultaneously, for arbitrary convex delay costs and nonstationary rates. It extends the cμc\mu rule beyond linear costs, links it to the "hug the optimal workload curve" policies of heavy-traffic control, and shows that the instantaneous allocation problem (43) is all that matters asymptotically. Later work on Brownian control of multiclass queues and on convex-cost scheduling (Mandelbaum and Stolyar 2004) builds on this.

Formalizing it. The paper's proofs are short and informal at several points, and the formalization makes these points explicit: the domain of every uniform limit, the policy class, and the reading of μ\mu. No part of this paper has a machine-checked proof. A completed mission would give a verified heavy-traffic analysis of a multiclass single-server queue at the sample-path level, the first on the platform with a deterministic diffusion scaling and an explicit reflection map.

Difficulty

The obvious route is to show that W~n\tilde W^n converges and then pass to the limit in the cost. That fails for the lower bound: Proposition 6 must cover policies whose class workloads never converge (polling-type policies), so it cannot use compactness of W~n\tilde W^n and must instead compare the cost of an arbitrary split of W~+n\tilde W^n_+ with the optimal split, locally in time. For the goal, (51) controls only the indices, so the convergence of W~n\tilde W^n must be extracted from (51) through the inverse marginal costs, the convergence of the total workload, and the Kuhn–Tucker conditions of (43). Delay convergence then needs a uniform control of T~n\tilde T^n over windows of length O(n−1/2)O(n^{-1/2}), and cost convergence needs the convergence of the costs CnC^n applied to delays of order n\sqrt n.

Formalization scope

Lean namespace GenCMu.HeavyTraffic. The development is deterministic and works one sample path at a time; the stochastic version (Proposition 8) is not part of this mission. Conventions committed to:

  • Classes are Fin d; job indices start at 11; every "→" between functions is uniform convergence ((11)), on [0,1][0,1] unless stated; lim inf⁡\liminf is written as "eventually ≥\ge bound −ε-\varepsilon".
  • The scaled processes are defined exactly, with Tˉn=Lˉn=Rn\bar T^n=\bar L^n=R^n ((69), (75)); the inverse in (14) is the generalized inverse on [0,1][0,1].
  • The o(n1/2)o(n^{1/2}) terms of (12)–(13) are uniform in tt. The trends converge in C1\mathcal C^1, not only in C\mathcal C. Without this, Aˉn,Sˉn\bar A^n,\bar S^n can oscillate on the n−1/2n^{-1/2} scale and (33)–(34) and Proposition 3 fail. The service expansion holds on server time [0,2n][0,2n], so that for d=1d=1 in heavy traffic the service times of jobs arriving before nn are covered.
  • μk\mu_k in (20), (36), (41), (46)–(51) is μk(Rk∗(t))\mu_k(R^*_k(t)), the service rate in real time, so ρk=λk/μk(Rk∗)\rho_k=\lambda_k/\mu_k(R^*_k).
  • (38) is uniform on compacts. Assumption 3's interior clause is imposed where W~+∗(t)>0\tilde W^*_+(t)>0. At W~+∗(t)=0\tilde W^*_+(t)=0 no point of Ω={0}\Omega=\{0\} is interior, and the literal clause would make the goal vacuous.
  • For the heavy-traffic limit and goal, feasible policies satisfy F1 (without adaptedness), F2–F4, Wk≥0W_k\ge0, work conservation (used by W+n=φ(Xn)W^n_+=\varphi(X^n)), and every job finishes. Proposition 6 uses a broader cost-admissible class that permits idleness with work waiting. Class-FIFO is built into the delay (9).
  • The delays of jobs arriving near the horizon depend on post-horizon service. We require the allocation on every bounded diffusion-scale window after nn to advance at the first-order rates ρk(1)\rho_k(1). This explicit boundary hypothesis keeps Propositions 2, 4, 5, and 7 on the paper's full [0,1][0,1].
  • Lemma 1 additionally assumes a common Lipschitz bound on the first-order partial-sum trends. Uniform convergence alone permits jumps of order n\sqrt n; the bound repairs that omission. Uniqueness of the solution of (43) is stated under strict convexity: "convex increasing" (p. 820) does not give it. (35) is stated without the implication from τ~n\tilde\tau^n back to W~n\tilde W^n, which fails in the uniform topology.
  • J~∗\tilde J^* integrates the optimal value of (43), so Proposition 6 needs no choice of minimizer.

A trivializing formalization is ruled out: no theorem assumes the convergence of W~n\tilde W^n or W~+n\tilde W^n_+, the uniqueness of minimizers, or the lower bound, and the joint satisfiability of all hypotheses has been checked in Lean for d=1d=1.

Needed infrastructure: sample-path reflection-map estimates, counting/partial-sum inversion with uniform o(n)o(\sqrt n) errors, parametric convex optimization (Berge's theorem for (43)), and Riemann-sum arguments for the lower bound. The reflection-map and inversion lemmas are reusable beyond this mission. Contributions to any milestone are welcome. The definitions are frozen, so a proof that needs a different definition should be raised in the discussion.

Selected references

  • J. A. Van Mieghem, Dynamic Scheduling with Convex Delay Costs: The Generalized cμ Rule, Ann. Appl. Probab. 5(3) (1995) 809–833. https://doi.org/10.1214/aoap/1177004706
  • C. Buyukkoc, P. Varaiya, J. Walrand, The cμ rule revisited, Adv. Appl. Probab. 17 (1985) 237–238.
  • J. M. Harrison, Brownian Motion and Stochastic Flow Systems, Wiley, 1985 (reflection map).
  • D. L. Iglehart, W. Whitt, Multiple channel queues in heavy traffic. I, Adv. Appl. Probab. 2 (1970) 150–177.
  • A. Mandelbaum, A. L. Stolyar, Scheduling flexible servers with convex delay costs: heavy-traffic optimality of the generalized cμ-rule, Oper. Res. 52(6) (2004) 836–855. https://doi.org/10.1287/opre.1040.0156
16 thms1 active userReviewed