OAI/Analysis/HardSphere/Conditioning/PermutationObserved.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.Comparison.bathPermutation line 15
2. lemma OAI.HardSphere.Comparison.bathPermutation_apply line 28
3. def OAI.HardSphere.Comparison.permutedFirstObservation line 32
4. def OAI.HardSphere.Comparison.secondPermutationObservation line 35
5. lemma OAI.HardSphere.Comparison.permutedFirstObservation_measurable line 40
6. lemma OAI.HardSphere.Comparison.secondPermutationObservation_measurable line 45
7. lemma OAI.HardSphere.Comparison.permutation_observations_eq line 51
8. lemma OAI.HardSphere.Comparison.permutation_observedMeasures_eq line 59
9. def OAI.HardSphere.Comparison.secondPositions line 81
10. lemma OAI.HardSphere.Comparison.secondPositions_measurable line 86
11. lemma OAI.HardSphere.Comparison.secondPositions_eq line 96
12. def OAI.HardSphere.Comparison.pairedPositions line 106
13. lemma OAI.HardSphere.Comparison.pairedPositions_measurable line 114
14. lemma OAI.HardSphere.Comparison.inserted_common_observed line 129