OAI/Analysis/CoulombRadii/RandomFields/ExteriorIMS.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.conditionalOutCost_lower_attraction line 13
2. lemma OAI.Coulomb.outLabelCount_eq_zero_iff line 34
3. lemma OAI.Coulomb.form_binary_cut_global line 50
4. lemma OAI.Coulomb.binary_cut_sector_lower line 74
5. lemma OAI.Coulomb.binary_cut_loss_bound line 109