OAI/Analysis/LiebThirring/MomentBound.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLiebThirring.Admissible.locallyIntegrable line 11
2. lemma OAI.SharpLiebThirring.Admissible.integrable_rpow line 17
3. lemma OAI.SharpLiebThirring.Admissible.mass_eq_ofReal line 27
4. lemma OAI.SharpLiebThirring.Admissible.mass_ne_top line 37
5. lemma OAI.SharpLiebThirring.sharpConstant_pos line 42
6. lemma OAI.SharpLiebThirring.finite_complex_eigenfamily_bound line 51
7. lemma OAI.SharpLiebThirring.negativeMoment_bound line 72

   Source documentation

   The full (unlimited-family-size) negative spectral moment estimate.

   lemma negativeMoment_bound {γ : ℝ} (hγ₀ : 1/2 < γ) (hγ₁ : γ < 3/2)
       {W : ℝ → ℝ} (hW : Admissible γ W) :
       negativeMoment γ W ≤ ENNReal.ofReal (sharpConstant γ)*potentialMass γ W := by
   …

   Mentions: OAI.SharpLiebThirring.Admissible, OAI.SharpLiebThirring.negativeMoment, OAI.SharpLiebThirring.sharpConstant, OAI.SharpLiebThirring.potentialMass