OAI/Analysis/HardSphere/Allocation/CertificateUseful.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HardSphere.Groups.certificate_useful_list line 18
2. lemma OAI.HardSphere.Sampling.allocated_restriction_half_bad line 87
3. lemma OAI.HardSphere.Sampling.enumerated_bad_card line 105
4. lemma OAI.HardSphere.Sampling.enumerated_failure_probability line 112
5. theorem OAI.HardSphere.Groups.certificate_useful_groups line 140