OAI/Analysis/CoulombRadii/RandomFields/EnsembleCoveredCost.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.sliceExpectation_localCount_le line 15
2. lemma OAI.Coulomb.sliceExpectation_count_cap_addback line 29
3. theorem OAI.Coulomb.conditionalOutCost_ensemble_cover_lower line 60
4. theorem OAI.Coulomb.RecordedEnsemble.atomic_cost_lower line 98
5. lemma OAI.Coulomb.RecordedEnsemble.patches_cover line 133