OAI/Analysis/CoulombRadii/Screening/CountMoments.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Coulomb.localCount line 14
  2. lemma OAI.Coulomb.localCount_nonneg line 17
  3. lemma OAI.Coulomb.localCount_le line 19
  4. lemma OAI.Coulomb.localCount_measurable line 24
  5. lemma OAI.Coulomb.localCount_weight_integrable line 28
  6. def OAI.Coulomb.localCountSecondMoment line 39
  7. lemma OAI.Coulomb.localCountSecondMoment_nonneg line 42
  8. lemma OAI.Coulomb.localCountSecondMoment_le line 46
  9. lemma OAI.Coulomb.expectedPopulation_eq line 60
  10. lemma OAI.Coulomb.expectedPopulation_sq_le line 67
  11. def OAI.Coulomb.outLabelCount line 96
  12. lemma OAI.Coulomb.outLabelCount_nonneg line 99
  13. lemma OAI.Coulomb.tensorCut_zero_of_outCount_lt line 102
  14. lemma OAI.Coulomb.tensorCut_outCount_square_le line 116
  15. theorem OAI.Coulomb.labelCut_outCount_secondMoment_le line 129