OAI/NumberTheory/Jacobsthal/Paths/RepresentativeStopGeometry.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.RepresentativeStopGeometry.sourceHeight line 15
2. theorem OAI.Erdos970.NumberTheoryLean.RepresentativeStopGeometry.sourceHeight_mono line 17
3. theorem OAI.Erdos970.NumberTheoryLean.RepresentativeStopGeometry.sourceHeight_error line 20
4. theorem OAI.Erdos970.NumberTheoryLean.RepresentativeStopGeometry.sourceHeight_lipschitz line 30
5. theorem OAI.Erdos970.NumberTheoryLean.RepresentativeStopGeometry.representative_safety_admits line 36
6. theorem OAI.Erdos970.NumberTheoryLean.RepresentativeStopGeometry.regular_margin_to_representative line 42
7. theorem OAI.Erdos970.NumberTheoryLean.RepresentativeStopGeometry.representative_to_actual_window line 49
8. theorem OAI.Erdos970.NumberTheoryLean.RepresentativeStopGeometry.actual_mark_to_representative_window line 65