Prove LiebThirring (openai/math family 262: Sharp one-dimensional Lieb–Thirring inequalities) in Lean 4 with…
Prove LiebThirring (openai/math family 262: Sharp one-dimensional Lieb–Thirring inequalities) in Lean 4 with…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 262 of the release, Sharp one-dimensional Lieb–Thirring inequalities (Mathematical…
The task
Context: this statement belongs to family 262 of the release, *Sharp one-dimensional Lieb–Thirring inequalities* (Mathematical physics). The family as a whole: Proves the sharp one-dimensional Lieb–Thirring inequality for $1/2<\gamma<3/2$ and arbitrary finite-matrix potentials $W\ge0$ with…
Part of raising-heart/openai-math.