OAI/Analysis/HardSphere/Conditioning/GlobalExposure.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.Comparison.blockExpose line 15
2. lemma OAI.HardSphere.Comparison.blockExpose_measurable line 19
3. lemma OAI.HardSphere.Comparison.blockExpose_glue line 24
4. lemma OAI.HardSphere.Comparison.exposedLaw_marginal line 32
5. lemma OAI.HardSphere.Comparison.exposedLaw_mass line 45
6. abbrev OAI.HardSphere.Comparison.AllocatedDatum line 56
7. def OAI.HardSphere.Comparison.fillOutside line 59
8. lemma OAI.HardSphere.Comparison.fillOutside_measurable line 63
9. def OAI.HardSphere.Comparison.branchDatum line 72
10. lemma OAI.HardSphere.Comparison.branchDatum_measurable line 77
11. def OAI.HardSphere.Comparison.allocationDatum line 82
12. lemma OAI.HardSphere.Comparison.allocationDatum_measurable line 88
13. lemma OAI.HardSphere.Comparison.allocationDatum_branch line 103
14. def OAI.HardSphere.Comparison.allocatedDatumLaw line 111
15. lemma OAI.HardSphere.Comparison.allocatedDatumLaw_branches line 123
16. lemma OAI.HardSphere.Comparison.allocatedDatumLaw_probability line 152
17. abbrev OAI.HardSphere.Groups.GroupDatum line 168
18. def OAI.HardSphere.Groups.groundDatumLaw line 172
19. lemma OAI.HardSphere.Groups.groundDatumLaw_probability line 181