OAI/Analysis/CoulombIonization/Fermionic/WeightedCoreStatistics.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.rawWeightedCount line 11
  2. lemma OAI.CoulombAtom.rawWeightedCount_nonneg line 12
  3. lemma OAI.CoulombAtom.rawWeightedCount_le line 14
  4. lemma OAI.CoulombAtom.rawWeightedCount_measurable line 18
  5. lemma OAI.CoulombAtom.rawWeightedCount_cutCore_le line 21
  6. def OAI.CoulombAtom.rawWeightedMoment line 31
  7. lemma OAI.CoulombAtom.rawWeightedMoment_nonneg line 33
  8. lemma OAI.CoulombAtom.rawWeightedMoment_eq_integral line 36
  9. lemma OAI.CoulombAtom.rawWeightedMoment_coreSlice_integrable line 41
  10. lemma OAI.CoulombAtom.sum_cutCore_weightedMoment_le line 48
  11. lemma OAI.CoulombAtom.nextCoreObservation_weighted_statistic_integrable line 69
  12. theorem OAI.CoulombAtom.sum_nextCoreObservation_weightedMoment_le line 78
  13. def OAI.CoulombAtom.CoreObservationGraph.weightedMoment line 102
  14. lemma OAI.CoulombAtom.CoreObservationGraph.observe_weightedMoment line 104
  15. def OAI.CoulombAtom.CoreObservationEnsemble.weightedMoment line 111
  16. lemma OAI.CoulombAtom.CoreObservationEnsemble.initial_weightedMoment line 113
  17. lemma OAI.CoulombAtom.CoreObservationEnsemble.observe_weightedMoment line 117
  18. lemma OAI.CoulombAtom.CoreObservationEnsemble.observeCells_weightedMoment line 125