OAI/Analysis/CoulombIonization/Localization/CoreHistoryAverageBarrier.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.coreLawAverage line 19
  2. lemma OAI.CoulombAtom.coreLawAverage_mass line 22
  3. lemma OAI.CoulombAtom.nextCoreObservation_statistic_integrable line 25
  4. theorem OAI.CoulombAtom.coreLawAverage_next line 38
  5. lemma OAI.CoulombAtom.coreLawAverage_next_mass line 59
  6. lemma OAI.CoulombAtom.nextCoreObservation_mass_statistic_integrable line 73
  7. lemma OAI.CoulombAtom.coreLawAverage_excess line 82
  8. lemma OAI.CoulombAtom.coreLawAverage_ordered_excess line 102
  9. lemma OAI.CoulombAtom.coreLawAverage_next_excess line 109
  10. lemma OAI.CoulombAtom.nextCoreObservation_excess_statistic_integrable line 123
  11. def OAI.CoulombAtom.rawFormPair line 136
  12. lemma OAI.CoulombAtom.rawFormPair_eq_integral line 139
  13. lemma OAI.CoulombAtom.leftList_measurable line 144
  14. lemma OAI.CoulombAtom.rawFormPair_coreSlice_integrable line 147
  15. lemma OAI.CoulombAtom.coreLawAverage_rawFormPair line 158
  16. def OAI.CoulombAtom.cutCorePositions line 180
  17. lemma OAI.CoulombAtom.cutCorePositions_reindex line 184
  18. lemma OAI.CoulombAtom.cutCorePositions_measurable line 190
  19. lemma OAI.CoulombAtom.cutCore_rawFormPair line 195
  20. lemma OAI.CoulombAtom.sum_cutCorePositions line 215