OAI/Analysis/HardSphere/Geometry/UniformBath.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.Comparison.uniform_of_equiv line 17
2. def OAI.HardSphere.Comparison.bathFinEquiv line 28
3. lemma OAI.HardSphere.Comparison.bathFinEquiv_apply line 42
4. def OAI.HardSphere.Comparison.bathIndexPermutation line 45
5. lemma OAI.HardSphere.Comparison.bathIndexPermutation_apply line 50
6. def OAI.HardSphere.Comparison.uniformBathOrder line 56
7. instance OAI.HardSphere.Comparison.uniformBathOrder_probability line 58
8. def OAI.HardSphere.Comparison.orderedPrimaryObservation line 61
9. lemma OAI.HardSphere.Comparison.orderedPrimaryObservation_measurable line 66
10. theorem OAI.HardSphere.Comparison.uniformBath_same_observation line 72