OAI/Analysis/HardSphere/Conditioning/SymmetricTag.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.Comparison.tagOrderPerm line 19
2. lemma OAI.HardSphere.Comparison.tagOrderPerm_zero line 21
3. lemma OAI.HardSphere.Comparison.tagOrderPerm_succ line 23
4. def OAI.HardSphere.Comparison.splitFirst line 30
5. lemma OAI.HardSphere.Comparison.splitFirst_measurable line 31
6. def OAI.HardSphere.Comparison.orderedObservation line 35
7. lemma OAI.HardSphere.Comparison.orderedObservation_measurable line 37
8. lemma OAI.HardSphere.Comparison.orderedObservation_eq line 44
9. lemma OAI.HardSphere.Comparison.ordered_symmetric_law line 48
10. lemma OAI.HardSphere.Comparison.ground_ordered_law line 65
11. lemma OAI.HardSphere.Comparison.ground_first_density line 73
12. def OAI.HardSphere.Comparison.orderedKernel line 93
13. instance OAI.HardSphere.Comparison.orderedKernel_markov line 96
14. lemma OAI.HardSphere.Comparison.orderedKernel_comp line 99
15. lemma OAI.HardSphere.Comparison.ground_ordered_bind line 106
16. lemma OAI.HardSphere.Comparison.all_tags_reference line 114
17. lemma OAI.HardSphere.Comparison.comp_comap_map line 137
18. lemma OAI.HardSphere.Comparison.allocation_slice_law line 141
19. lemma OAI.HardSphere.Groups.physical_group_tag_reference line 160