OAI/NumberTheory/Jacobsthal/Renewal/ContinuousCompletedOccupation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Erdos970.NumberTheoryLean.ContinuousCompletedOccupation.liftReward line 19
2. theorem OAI.Erdos970.NumberTheoryLean.ContinuousCompletedOccupation.liftReward_measurable line 21
3. theorem OAI.Erdos970.NumberTheoryLean.ContinuousCompletedOccupation.completed_power_lift line 24
4. theorem OAI.Erdos970.NumberTheoryLean.ContinuousCompletedOccupation.low_power_integral_le line 30
5. theorem OAI.Erdos970.NumberTheoryLean.ContinuousCompletedOccupation.inclusive_integral_eq_tsum line 46
6. theorem OAI.Erdos970.NumberTheoryLean.ContinuousCompletedOccupation.completed_finite_occupation_le line 55