OAI/Analysis/CoulombIonization/RadialBounds/CellCountSupremumBarrier.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.rawCountMoment_le_number line 16
  2. def OAI.CoulombAtom.localCountRatioSet line 30
  3. def OAI.CoulombAtom.localCountSupremum line 33
  4. lemma OAI.CoulombAtom.localCountRatioSet_nonempty line 36
  5. lemma OAI.CoulombAtom.localCountRatioSet_bddAbove line 41
  6. lemma OAI.CoulombAtom.localCountSupremum_one_le line 49
  7. lemma OAI.CoulombAtom.localCountMoment_le_supremum line 52
  8. lemma OAI.CoulombAtom.localCountSupremum_le line 61
  9. def OAI.CoulombAtom.localCountCoverConstant line 71
  10. lemma OAI.CoulombAtom.localCountCoverConstant_one_le line 72
  11. theorem OAI.CoulombAtom.enlarged_cell_count_le line 76