OAI/NumberTheory/Jacobsthal/Renewal/FlaggedOccupationBound.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.FlaggedOccupationBound.selected line 18
2. theorem OAI.Erdos970.NumberTheoryLean.FlaggedOccupationBound.selected_measurable line 21
3. theorem OAI.Erdos970.NumberTheoryLean.FlaggedOccupationBound.selected_false line 25
4. theorem OAI.Erdos970.NumberTheoryLean.FlaggedOccupationBound.selected_true line 29
5. theorem OAI.Erdos970.NumberTheoryLean.FlaggedOccupationBound.selected_integral_le line 32
6. theorem OAI.Erdos970.NumberTheoryLean.FlaggedOccupationBound.selected_true_integral line 43
7. theorem OAI.Erdos970.NumberTheoryLean.FlaggedOccupationBound.selected_row line 50
8. theorem OAI.Erdos970.NumberTheoryLean.FlaggedOccupationBound.law_selected_step line 65
9. theorem OAI.Erdos970.NumberTheoryLean.FlaggedOccupationBound.finite_selected_occupation line 91