OAI/Analysis/CoulombRadii/RandomFields/RecordedCount.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.localCount_join line 14
2. lemma OAI.Coulomb.localCount_permute line 18
3. lemma OAI.Coulomb.localCount_reindex line 23
4. lemma OAI.Coulomb.potentialForm_mono_bounded line 28
5. lemma OAI.Coulomb.sliceExpectation_localCount_sq_le line 38
6. lemma OAI.Coulomb.raw_posterior_positive_le_core line 80
7. theorem OAI.Coulomb.radial_raw_gain_step line 96