OAI/NumberTheory/Jacobsthal/Partitions/SuccessfulTailTransport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.SuccessfulTailTransport.cleanReward line 22
2. theorem OAI.Erdos970.NumberTheoryLean.SuccessfulTailTransport.cleanReward_measurable line 25
3. theorem OAI.Erdos970.NumberTheoryLean.SuccessfulTailTransport.positive_completed_occupation_le line 30
4. theorem OAI.Erdos970.NumberTheoryLean.SuccessfulTailTransport.actual_clean_tail_transport line 38