OAI/Probability/LatticePassage/FiniteProduct.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CompanionFPP.LocalCoordinates line 9
2. def OAI.CompanionFPP.extendLocalCoordinates line 11
3. lemma OAI.CompanionFPP.extendLocalCoordinates_apply line 16
4. lemma OAI.CompanionFPP.measurable_extendLocalCoordinates line 22
5. def OAI.CompanionFPP.finitePassageTime line 31
6. lemma OAI.CompanionFPP.measurable_finitePassageTime line 34
7. theorem OAI.CompanionFPP.finitePassageTime_restrict line 38
8. theorem OAI.CompanionFPP.finitePassageTime_law line 44
9. theorem OAI.CompanionFPP.finitePassageTime_change_squared line 54
10. theorem OAI.CompanionFPP.finitePassageTime_lipschitz line 63