OAI/Analysis/CoulombIonization/RadialBounds/CoreHistoryCountsBarrier.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.rawBallCount_cutCore_le line 17
  2. def OAI.CoulombAtom.rawCountMoment line 24
  3. lemma OAI.CoulombAtom.rawCountMoment_nonneg line 27
  4. lemma OAI.CoulombAtom.rawCountMoment_eq_integral line 31
  5. lemma OAI.CoulombAtom.rawCountMoment_coreSlice_integrable line 36
  6. lemma OAI.CoulombAtom.sum_cutCore_countMoment_le line 42
  7. lemma OAI.CoulombAtom.nextCoreObservation_count_statistic_integrable line 63
  8. lemma OAI.CoulombAtom.sum_nextCoreObservation_count_eq line 72
  9. theorem OAI.CoulombAtom.sum_nextCoreObservation_countMoment_le line 89
  10. def OAI.CoulombAtom.CoreObservationGraph.countMoment line 109
  11. lemma OAI.CoulombAtom.CoreObservationGraph.countMoment_nonneg line 112
  12. lemma OAI.CoulombAtom.CoreObservationGraph.observe_countMoment line 115
  13. lemma OAI.CoulombAtom.rawBallCount_le_of_radius line 125
  14. lemma OAI.CoulombAtom.rawCountMoment_le_of_radius line 140
  15. lemma OAI.CoulombAtom.CoreObservationGraph.countMoment_le_of_radius line 155