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

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

- [Sharp one-dimensional Lieb–Thirring constants](../../preprints/Sharp-One-Dimensional-Lieb-Thirring-Constants-September-23-2026/paper.pdf)

## 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](../ComparatorChallenges/LiebThirring.lean) |