OAI/Analysis/HardSphere/Allocation/PhysicalRouteAuxiliary.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.HardSphere.Groups.PhysicalRouteAux line 21
2. lemma OAI.HardSphere.Groups.physicalRouteAux_nonempty line 44
3. def OAI.HardSphere.Groups.PhysicalRouteAux.firstDensity line 62
4. def OAI.HardSphere.Groups.PhysicalRouteAux.secondDensity line 72
5. lemma OAI.HardSphere.Groups.PhysicalRouteAux.laws line 82
6. lemma OAI.HardSphere.Groups.PhysicalRouteAux.path_bounds line 94
7. theorem OAI.HardSphere.Groups.physical_first_likelihood_moment line 130
8. theorem OAI.HardSphere.Groups.physical_second_likelihood_moment line 192