OAI/Analysis/CoulombIonization/ThomasFermi/Lp.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CoulombAnalysis.TFLp line 35
  2. def OAI.CoulombAnalysis.NonnegDensity line 37
  3. def OAI.CoulombAnalysis.densityWeight line 39
  4. lemma OAI.CoulombAnalysis.tfLp_norm_rpow line 41
  5. lemma OAI.CoulombAnalysis.tfLp_norm_rpow_nonneg line 50
  6. lemma OAI.CoulombAnalysis.nonnegDensity_add line 55
  7. lemma OAI.CoulombAnalysis.densityWeight_nonneg line 61
  8. lemma OAI.CoulombAnalysis.tfLp_interpolation line 67
  9. lemma OAI.CoulombAnalysis.isClosed_nonnegDensity line 81
  10. theorem OAI.CoulombAnalysis.exists_minimizer_of_tf_gap line 90
  11. abbrev OAI.CoulombAnalysis.TFSpace line 149
  12. def OAI.CoulombAnalysis.ballMeasure line 150
  13. instance OAI.CoulombAnalysis.(instance at line 151) line 151
  14. lemma OAI.CoulombAnalysis.norm_inv_power_integrable_ball line 156
  15. lemma OAI.CoulombAnalysis.coulomb_power_integrable line 164
  16. lemma OAI.CoulombAnalysis.coulomb_memLp line 190
  17. lemma OAI.CoulombAnalysis.nuclear_memLp line 200