OAI/Analysis/LiebThirring/Main.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpLiebThirring.sharp_times_extremizer_mass line 10
  2. lemma OAI.SharpLiebThirring.optimalConstant_le_sharp line 16
  3. lemma OAI.SharpLiebThirring.sharp_le_oneStateConstant line 22
  4. theorem OAI.SharpLiebThirring.sharp_lieb_thirring line 38

    Source documentation

    Full sharp Lieb–Thirring bound, both optimal constants, and equality at the explicit potential; no finite spectral cutoff is imposed.

    Distinct definitions of this name: ComparatorChallenges/LiebThirring.lean:94 (same statement text; different proof or body). Qualify references as OAI.SharpLiebThirring.sharp_lieb_thirring@path.

    theorem sharp_lieb_thirring : MainClaim := by
…

    Mentions: OAI.SharpLiebThirring.MainClaim