OAI/Analysis/HardSphere/Conditioning/PhysicalObservation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.Comparison.optionParticle line 15
2. lemma OAI.HardSphere.Comparison.routeEmbedding_natural line 24
3. lemma OAI.HardSphere.Comparison.routePermutation_natural line 31
4. lemma OAI.HardSphere.Comparison.fullRoute_fixed_outside line 50
5. def OAI.HardSphere.Comparison.fillGroup line 57
6. lemma OAI.HardSphere.Comparison.fillGroup_selected line 61
7. lemma OAI.HardSphere.Comparison.fillGroup_permutation line 66
8. lemma OAI.HardSphere.Comparison.fillGroup_measurable line 77
9. lemma OAI.HardSphere.Comparison.ambient_midpoint_permutation line 89
10. lemma OAI.HardSphere.Groups.projectPoint_continuous line 111
11. def OAI.HardSphere.Groups.physicalFullMidpoint line 114
12. lemma OAI.HardSphere.Groups.physicalFullMidpoint_measurable line 120
13. theorem OAI.HardSphere.Groups.physicalPairedRoute_midpoint line 139