OAI/Analysis/CoulombIonization/RadialBounds/UnshiftedCellCountBarrier.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.universalCellCountConstant line 19
  2. lemma OAI.CoulombAtom.universalCellCountConstant_one_le line 20
  3. theorem OAI.CoulombAtom.priced_local_cell_count line 23
  4. lemma OAI.CoulombAtom.localOffsetMass_mono line 32
  5. lemma OAI.CoulombAtom.quantum_unpriced_le_price line 38
  6. lemma OAI.CoulombAtom.unshifted_priced_excess_bound line 46
  7. theorem OAI.CoulombAtom.unshifted_local_cell_count line 54
  8. theorem OAI.CoulombAtom.unshifted_local_count_supremum line 79
  9. lemma OAI.CoulombBarrier.masterKernel_amplitude line 98
  10. lemma OAI.CoulombBarrier.masterWidth_radius_lower line 127
  11. lemma OAI.CoulombBarrier.masterWidth_radius_upper line 138
  12. def OAI.CoulombBarrier.rawAnnularCount line 151
  13. lemma OAI.CoulombBarrier.rawAnnularCount_nonneg line 154
  14. lemma OAI.CoulombBarrier.rawAnnularCount_le line 160
  15. lemma OAI.CoulombBarrier.rawAnnularCount_measurable line 166
  16. lemma OAI.CoulombBarrier.rawBallCount_le_annular line 174