OAI/Analysis/CoulombRadii/RandomFields/RecordedStatistic.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Coulomb.arrayStatistic line 13
2. lemma OAI.Coulomb.arrayStatistic_measurable line 16
3. lemma OAI.Coulomb.arrayStatistic_join line 21
4. lemma OAI.Coulomb.arrayStatistic_reindex line 25
5. lemma OAI.Coulomb.arrayStatistic_eq_zero_of_allPositions line 30
6. lemma OAI.Coulomb.potentialForm_statistic_join_of_support line 34
7. lemma OAI.Coulomb.sliceExpectation_statistic_eq line 48
8. lemma OAI.Coulomb.RecordedEnsemble.Conserves.statistic line 67
9. theorem OAI.Coulomb.RecordedEnsemble.Conserves.statistic_event_ae line 78
10. theorem OAI.NeutralAtom.arrayEvent_fresh_statistic_ae line 120
11. theorem OAI.Coulomb.arrayStatistic_local_matching line 157