OAI/Analysis/CoulombIonization/Localization/CoreObservationEnsembleBarrier.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CoulombAtom.CoreObservationEnsemble line 17
  2. def OAI.CoulombAtom.CoreObservationEnsemble.initial line 25
  3. def OAI.CoulombAtom.CoreObservationEnsemble.observe line 30
  4. def OAI.CoulombAtom.CoreObservationEnsemble.mass line 36
  5. def OAI.CoulombAtom.CoreObservationEnsemble.countMoment line 37
  6. def OAI.CoulombAtom.CoreObservationEnsemble.fieldMoment line 39
  7. def OAI.CoulombAtom.CoreObservationEnsemble.excess line 41
  8. def OAI.CoulombAtom.CoreObservationEnsemble.outMoment line 42
  9. lemma OAI.CoulombAtom.CoreObservationEnsemble.mass_nonneg line 45
  10. lemma OAI.CoulombAtom.CoreObservationEnsemble.countMoment_nonneg line 47
  11. lemma OAI.CoulombAtom.CoreObservationEnsemble.fieldMoment_nonneg line 49
  12. lemma OAI.CoulombAtom.CoreObservationEnsemble.outMoment_nonneg line 51
  13. lemma OAI.CoulombAtom.CoreObservationEnsemble.observe_mass line 55
  14. lemma OAI.CoulombAtom.CoreObservationEnsemble.observe_countMoment line 62
  15. lemma OAI.CoulombAtom.CoreObservationEnsemble.fieldMoment_le_nuclear line 70
  16. lemma OAI.CoulombAtom.CoreObservationEnsemble.fieldMoment_ball_integrable line 76
  17. lemma OAI.CoulombAtom.CoreObservationEnsemble.observe_excess_budget line 82
  18. lemma OAI.CoulombAtom.CoreObservationEnsemble.fieldMoment_le_observe_excess line 104
  19. lemma OAI.CoulombAtom.CoreObservationEnsemble.outMoment_spatial line 121