OAI/Probability/LatticePassage/GeodesicTail.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CompanionFPP.geodesic_tail_split line 10
2. lemma OAI.CompanionFPP.tail_numerics line 45
3. theorem OAI.CompanionFPP.simple_geodesic_length_tail line 68
4. theorem OAI.CompanionFPP.geodesic_length_tail line 76
5. theorem OAI.CompanionFPP.geodesic_length_tail_source line 92