OAI/Analysis/CoulombRadii/RandomFields/RecordedEnsemble.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Coulomb.RecordedEnsemble line 13
  2. def OAI.Coulomb.RecordedEnsemble.totalMass line 25
  3. def OAI.Coulomb.RecordedEnsemble.totalForm line 26
  4. def OAI.Coulomb.RecordedEnsemble.Conserves line 27
  5. def OAI.Coulomb.RecordedEnsemble.CoreFermionic line 31
  6. def OAI.Coulomb.RecordedEnsemble.OutSupported line 33
  7. def OAI.Coulomb.RecordedEnsemble.rawSquare line 36
  8. lemma OAI.Coulomb.RecordedEnsemble.reindexConfiguration_trans line 41
  9. lemma OAI.Coulomb.RecordedEnsemble.Conserves.population line 47
  10. lemma OAI.Coulomb.RecordedEnsemble.Conserves.secondMoment line 54
  11. lemma OAI.Coulomb.RecordedEnsemble.Conserves.recorded_secondMoment line 63
  12. theorem OAI.Coulomb.RecordedEnsemble.append_radial line 70