OAI/Analysis/HardSphere/Paths/AcceptedIntegrand.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.DyadicSkeleton.measurable_simpleEncounter line 14
2. lemma OAI.HardSphere.DyadicSkeleton.measurable_simpleEncounter_comp line 19
3. lemma OAI.HardSphere.DyadicSkeleton.measurable_dyadicEncounter line 32
4. def OAI.HardSphere.DyadicSkeleton.acceptedIntegrand line 40
5. lemma OAI.HardSphere.DyadicSkeleton.measurable_acceptedIntegrand line 46
6. lemma OAI.HardSphere.DyadicSkeleton.dyadic_environment_moment line 52
7. lemma OAI.HardSphere.DyadicSkeleton.dyadic_annealed_moment line 87
8. lemma OAI.HardSphere.DyadicSkeleton.small_route_parameters line 117
9. lemma OAI.HardSphere.DyadicSkeleton.dyadic_path_constants line 151
10. lemma OAI.HardSphere.DyadicSkeleton.double_lintegral_map line 170
11. lemma OAI.HardSphere.DyadicSkeleton.dyadicDetour_good_mass line 181
12. lemma OAI.HardSphere.DyadicSkeleton.dyadicDetour_double_moment line 192
13. theorem OAI.HardSphere.DyadicSkeleton.dyadic_good_paths_lift line 204