OAI/NumberTheory/Jacobsthal/Renewal/NonnegativeOriginalOccupation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.SourceCompactOccupation.compactReward line 20
2. theorem OAI.Erdos970.NumberTheoryLean.SourceCompactOccupation.literal_scaled_weight line 24
3. theorem OAI.Erdos970.NumberTheoryLean.SourceCompactOccupation.compact_reward_envelope line 32
4. theorem OAI.Erdos970.NumberTheoryLean.SourceCompactOccupation.finite_reward_envelope line 44
5. theorem OAI.Erdos970.NumberTheoryLean.SourceCompactOccupation.finite_selected_reward_envelope line 57
6. theorem OAI.Erdos970.NumberTheoryLean.SourceCompactOccupation.source_compact_occupation line 76
7. theorem OAI.Erdos970.NumberTheoryLean.PrimeFamilyOccupation.singleton_off_stage line 140
8. def OAI.Erdos970.NumberTheoryLean.PrimeFamilyOccupation.listReward line 149
9. theorem OAI.Erdos970.NumberTheoryLean.PrimeFamilyOccupation.singleton_scaled_reward line 153
10. theorem OAI.Erdos970.NumberTheoryLean.PrimeFamilyOccupation.finite_signed_original_occupation line 166
11. theorem OAI.Erdos970.NumberTheoryLean.PrimeFamilyOccupation.listReward_nonneg line 210
12. theorem OAI.Erdos970.NumberTheoryLean.PrimeFamilyOccupation.finite_nonnegative_original_occupation line 217