OAI/Analysis/CoulombRadii/FieldAnalysis/UniformBall.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Coulomb.uniformBall line 14
  2. def OAI.Coulomb.ballCloud line 17
  3. lemma OAI.Coulomb.uniformBall_nonneg line 19
  4. lemma OAI.Coulomb.uniformBall_le line 25
  5. lemma OAI.Coulomb.uniformBall_measurable line 29
  6. lemma OAI.Coulomb.uniformBall_integrable line 32
  7. lemma OAI.Coulomb.uniformBall_mass line 35
  8. lemma OAI.Coulomb.uniformBall_power_integrable line 42
  9. lemma OAI.Coulomb.uniformBall_power line 52
  10. lemma OAI.Coulomb.uniformBall_radial line 62
  11. lemma OAI.Coulomb.uniformBall_support line 67
  12. lemma OAI.Coulomb.ballCloud_mass line 72
  13. lemma OAI.Coulomb.ballCloud_integrable line 77
  14. lemma OAI.Coulomb.ballCloud_measurable line 80
  15. lemma OAI.Coulomb.ballCloud_coulomb line 83
  16. lemma OAI.Coulomb.ballCloud_coulomb_bound line 100
  17. lemma OAI.Coulomb.ballCloud_coulombBilinear_bound line 109
  18. lemma OAI.Coulomb.coreCoulombPotential_ballCloud line 140
  19. lemma OAI.Coulomb.attraction_ballCloud line 159
  20. lemma OAI.Coulomb.coreScreenedField_ballCloud line 174