OAI/Analysis/CoulombIonization/Variational/ClosedInnerStatistic.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.innerParticleWeight line 13
  2. lemma OAI.CoulombAtom.innerParticleWeight_measurable line 14
  3. lemma OAI.CoulombAtom.innerParticleWeight_nonneg line 17
  4. lemma OAI.CoulombAtom.innerParticleWeight_le line 19
  5. lemma OAI.CoulombAtom.sourcePotential_actualInnerSource_raw line 28
  6. def OAI.CoulombAtom.closedRawInnerField line 53
  7. lemma OAI.CoulombAtom.closedRawInnerField_measurable line 56
  8. lemma OAI.CoulombAtom.closedRawInnerField_bound line 65
  9. lemma OAI.CoulombAtom.rawFormPair_closedRawInnerField line 78
  10. lemma OAI.CoulombAtom.rawInnerField_le_closed line 96
  11. lemma OAI.CoulombAtom.rawWeightedCount_reindex line 109
  12. lemma OAI.CoulombAtom.closedRawInnerField_reindex line 113
  13. lemma OAI.CoulombAtom.rawWeightedCount_join line 116
  14. lemma OAI.CoulombAtom.closedRawInnerField_join line 122