OAI/Analysis/CoulombRadii/ThomasFermi/TfPotential.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Coulomb.tfPotential line 36
  2. lemma OAI.Coulomb.tfPotential_integrand line 39
  3. lemma OAI.Coulomb.tfPotential_measurable line 44
  4. lemma OAI.Coulomb.tfPotential_bound line 49
  5. lemma OAI.Coulomb.tfPotential_memLp line 56
  6. def OAI.Coulomb.tfPotentialField line 60
  7. lemma OAI.Coulomb.tfPotentialField_coe line 62
  8. lemma OAI.Coulomb.tfCoulomb_eq_potential line 64
  9. lemma OAI.Coulomb.tfCoulomb_eq_field line 78
  10. def OAI.Coulomb.tfIndicator line 90
  11. lemma OAI.Coulomb.tfIndicator_coe line 92
  12. lemma OAI.Coulomb.tfIndicator_nonneg line 94
  13. lemma OAI.Coulomb.tfIndicator_bound line 98
  14. lemma OAI.Coulomb.tfField_indicator line 103
  15. lemma OAI.Coulomb.tfDual_nonneg line 110
  16. lemma OAI.Coulomb.tfKineticField_memLp line 118
  17. def OAI.Coulomb.tfKineticField line 127
  18. lemma OAI.Coulomb.tfKineticField_coe line 130
  19. lemma OAI.Coulomb.tfKineticField_pair line 133
  20. lemma OAI.Coulomb.tfKineticField_self line 140
  21. lemma OAI.Coulomb.tfPower_hasDerivAt line 154
  22. lemma OAI.Coulomb.nonneg_deriv_of_min_on_right line 198