OAI/Analysis/HardSphere/Conditioning/Sampling.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.Sampling.uniform_map_apply line 14
2. lemma OAI.HardSphere.Sampling.pmf_eq_uniform_of_constant line 19
3. lemma OAI.HardSphere.Sampling.uniform_map_of_equal_fibers line 36
4. lemma OAI.HardSphere.Sampling.embedding_restriction_uniform line 44
5. lemma OAI.HardSphere.Sampling.descFactorial_ratio_le line 66
6. lemma OAI.HardSphere.Sampling.all_bad_card line 92
7. lemma OAI.HardSphere.Sampling.uniform_all_bad line 101
8. lemma OAI.HardSphere.Sampling.uniform_positions_bad line 121
9. lemma OAI.HardSphere.Sampling.uniform_bad_count line 139
10. lemma OAI.HardSphere.Sampling.uniform_half_bad line 164