OAI/NumberTheory/Jacobsthal/Paths/TwoSidedThresholdArrival.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.TwoSidedThresholdArrival.reconstructedParent line 16
2. theorem OAI.Erdos970.NumberTheoryLean.TwoSidedThresholdArrival.reconstructedParent_measurable line 18
3. theorem OAI.Erdos970.NumberTheoryLean.TwoSidedThresholdArrival.reconstructedParent_update line 21
4. theorem OAI.Erdos970.NumberTheoryLean.TwoSidedThresholdArrival.reconstructed_geometry line 26
5. def OAI.Erdos970.NumberTheoryLean.TwoSidedThresholdArrival.thickArrival line 36
6. theorem OAI.Erdos970.NumberTheoryLean.TwoSidedThresholdArrival.thickArrival_measurable line 40
7. theorem OAI.Erdos970.NumberTheoryLean.TwoSidedThresholdArrival.thickArrival_update line 52
8. theorem OAI.Erdos970.NumberTheoryLean.TwoSidedThresholdArrival.thickHazard_eq_actual line 58