OAI/MeasureTheory/Falconer/Graphs/GraphTorusArcLength.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PlanarFalconer.sourceArcLength_pair_integral_period line 10
2. theorem OAI.PlanarFalconer.arctan_interval_integral line 21
3. theorem OAI.PlanarFalconer.sourceArcLength_pair_graph_angles line 34
4. theorem OAI.PlanarFalconer.sourceArcLength_pair_rotate_right line 52
5. theorem OAI.PlanarFalconer.sourceArcLength_pair_graph_angles_rotated line 60