OAI/Analysis/CoulombRadii/ThomasFermi/TFExponent.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Coulomb.TFExponent line 15
  2. instance OAI.Coulomb.(instance at line 16) line 16
  3. abbrev OAI.Coulomb.TFLp line 17
  4. lemma OAI.Coulomb.tfLp_norm line 18
  5. lemma OAI.Coulomb.tfLp_norm_power line 24
  6. lemma OAI.Coulomb.tfLp_integral_norm_le line 28
  7. def OAI.Coulomb.tfExtend line 37
  8. lemma OAI.Coulomb.tfExtend_measurable line 39
  9. lemma OAI.Coulomb.tfExtend_memLp line 41
  10. lemma OAI.Coulomb.tfExtend_integrable line 44
  11. lemma OAI.Coulomb.tfExtend_norm_integral line 49
  12. lemma OAI.Coulomb.tfExtend_norm_power_integral line 52
  13. def OAI.Coulomb.tfCoulomb line 60
  14. lemma OAI.Coulomb.tfCoulomb_integrable line 62
  15. lemma OAI.Coulomb.tfCoulomb_self_nonneg line 67
  16. lemma OAI.Coulomb.tfExtend_convolution_bound line 71
  17. lemma OAI.Coulomb.tf_power_strong_convex line 90
  18. lemma OAI.Coulomb.tf_power_midpoint_gap line 120
  19. lemma OAI.Coulomb.tf_power_difference_factor line 136
  20. lemma OAI.Coulomb.tf_midpoint_gap_nonneg line 149
  21. lemma OAI.Coulomb.integrable_rpow_of_memLp_nonneg line 154
  22. lemma OAI.Coulomb.memLp_rpow_of_integrable_nonneg line 162
  23. lemma OAI.Coulomb.tf_integrated_midpoint_gap line 173