OAI/Analysis/CoulombIonization/RadialBounds/SharpFreshPatchBarrier.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.sharpPatchRemainder line 19
  2. lemma OAI.CoulombAtom.count_two_thirds_scale line 27
  3. theorem OAI.CoulombAtom.sharp_selected_fresh_patch line 35
  4. def OAI.CoulombAtom.smoothMultiplyL2 line 101
  5. lemma OAI.CoulombAtom.smoothMultiplyL2_ae line 105
  6. lemma OAI.CoulombAtom.smoothMultiplyL2_norm_le line 110
  7. lemma OAI.CoulombAtom.smoothMultiplyL2_inner line 118
  8. def OAI.CoulombAtom.smoothDerivativeProductL2 line 130
  9. lemma OAI.CoulombAtom.smoothDerivativeProductL2_ae line 135
  10. lemma OAI.CoulombAtom.smoothMultiplyL2_weak line 142
  11. lemma OAI.CoulombLT.BesselFamily.smoothMultiply line 154
  12. lemma OAI.CoulombLT.infiniteDensity_smoothMultiply line 163
  13. theorem OAI.CoulombLT.localized_family_lieb_thirring line 172