OAI/Analysis/HardSphere/Conditioning/SharedRoute.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.Comparison.fiberNormalize_apply_measure line 15
2. def OAI.HardSphere.Comparison.ambientFirst line 26
3. def OAI.HardSphere.Comparison.ambientSecond line 30
4. lemma OAI.HardSphere.Comparison.ambientFirst_measurable line 35
5. lemma OAI.HardSphere.Comparison.ambientSecond_measurable line 41
6. def OAI.HardSphere.Comparison.ambientRefreshEvent line 47
7. lemma OAI.HardSphere.Comparison.ambientRefreshEvent_measurable line 53
8. def OAI.HardSphere.Comparison.ambientRefreshKernel line 61
9. instance OAI.HardSphere.Comparison.ambientRefreshKernel_finite line 66
10. lemma OAI.HardSphere.Comparison.ambientRefreshKernel_apply line 73
11. def OAI.HardSphere.Comparison.ambientSharedKernel line 83
12. instance OAI.HardSphere.Comparison.ambientSharedKernel_finite line 89
13. lemma OAI.HardSphere.Comparison.ambientSharedKernel_mass line 97
14. lemma OAI.HardSphere.Comparison.ambientSharedKernel_support line 114
15. theorem OAI.HardSphere.Comparison.ambient_common_observation line 137