OAI/Geometry/TranslativeCovering/CylinderProbability.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CylinderProbability.uniform line 38
2. lemma OAI.CylinderProbability.uniform_probability line 41
3. lemma OAI.CylinderProbability.uniform_le line 47
4. lemma OAI.CylinderProbability.uniform_section line 51
5. def OAI.CylinderProbability.pairEvent line 85
6. lemma OAI.CylinderProbability.pairEvent_measurable line 89
7. lemma OAI.CylinderProbability.pair_probability line 101