Sharp finite-matrix Lieb–Thirring inequalities and all equality cases

3 papersLean

Proves the sharp one-dimensional Lieb–Thirring inequality for \(1/2\lt \gamma\lt 3/2\) and arbitrary finite-matrix potentials W ≥ 0 with \(\int\mathop{\mathrm{tr}}\nolimits (W^{\gamma+1/2})\lt \infty\): the optimal constant is the scalar one-bound-state value, independent of matrix size. All equality cases are direct sums, in one constant unitary basis, of scalar sech² solitons with independent scales and centers, and zero channels.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 3

Equality cases in the sharp one-dimensional matrix Lieb–Thirring inequality

OpenAI · October 5, 2026

We classify all equality cases in the sharp one-dimensional Lieb–Thirring inequality for every finite matrix size and \(1/2\lt \gamma\lt 3/2\). For measurable Hermitian positive semidefinite potentials W with \(\int_\mathbb R\mathop{\mathrm{tr}}\nolimits (W^{\gamma+1/2})\lt \infty\), equality holds precisely for direct sums, in one constant unitary basis, of scalar one-bound-state solitons and zero channels. The nonzero solitons may have independent scales and centers.

Read PDF Download Source

Cite

@misc{OAI:Equality-cases-in-the-sharp-one-dimensional-matrix-Lieb-Thirring-inequality-October-5-2026,
  author = {{OpenAI}},
  title = {{Equality cases in the sharp one-dimensional matrix Lieb--Thirring inequality}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Equality-cases-in-the-sharp-one-dimensional-matrix-Lieb-Thirring-inequality-October-5-2026/sharp-one-dimensional-lieb-thirring-inequalities-matrix-potentials.pdf}{OAI:Equality-cases-in-the-sharp-one-dimensional-matrix-Lieb-Thirring-inequality-October-5-2026}},
  year = {2026}
}

Sharp one-dimensional Lieb–Thirring inequalities for matrix potentials

OpenAI · October 5, 2026

We prove the sharp one-dimensional Lieb–Thirring inequality for every finite matrix size and every exponent \(1/2\lt \gamma\lt 3/2\). The optimal constant is the scalar one-bound-state constant, independently of the matrix size. The inequality bounds the full sum of negative eigenvalue moments for every measurable Hermitian positive semidefinite potential W satisfying \(\int_\mathbb R\mathop{\mathrm{tr}}\nolimits (W^{\gamma+1/2})\lt \infty\). The matrices may have arbitrary rank and need not commute at different points.

Read PDF Download Source

Cite

@misc{OAI:Sharp-one-dimensional-Lieb-Thirring-inequalities-for-matrix-potentials-October-5-2026,
  author = {{OpenAI}},
  title = {{Sharp one-dimensional Lieb--Thirring inequalities for matrix potentials}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Sharp-one-dimensional-Lieb-Thirring-inequalities-for-matrix-potentials-October-5-2026/sharp-matrix-lieb-thirring.pdf}{OAI:Sharp-one-dimensional-Lieb-Thirring-inequalities-for-matrix-potentials-October-5-2026}},
  year = {2026}
}

Sharp one-dimensional Lieb–Thirring constants

OpenAI · September 23, 2026

We resolve affirmatively the remaining cases of the scalar one-dimensional Lieb–Thirring conjecture: for every \(\frac12\lt \gamma\lt \frac32\), the optimal constant is the one-bound-state constant. The estimate holds for every nonnegative potential in \(L^{\gamma+1/2}(\mathbb R)\), with all negative eigenvalues included.

Read PDF Download Source

Cite

@misc{OAI:Sharp-One-Dimensional-Lieb-Thirring-Constants-September-23-2026,
  author = {{OpenAI}},
  title = {{Sharp one-dimensional Lieb--Thirring constants}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Sharp-One-Dimensional-Lieb-Thirring-Constants-September-23-2026/paper.pdf}{OAI:Sharp-One-Dimensional-Lieb-Thirring-Constants-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Sharp one-dimensional Lieb–Thirring constants

Scope

The formalized result determines the sharp one-dimensional Lieb–Thirring constant for \(1/2<\gamma<3/2\). For every nonnegative \(W\in L^{\gamma+1/2}(\mathbb R)\), it bounds the full negative-eigenvalue moment of \(-d^2/dx^2-W\) by the one-bound-state constant times the potential integral. This constant is optimal and is attained by \((r+1)\mathrm{sech}^2(rx)\), where \(r=(\gamma-1/2)^{-1}\). No finite spectral cutoff is imposed.

Comparator links

Result	Comparator statement
Sharp one-dimensional Lieb–Thirring inequality	LiebThirring.lean

Scope note on GitHub →