OAI/NumberTheory/Jacobsthal/Paths/FullPathCompactSelection.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.FullPathCompactSelection.fullCompactReward line 21
2. theorem OAI.Erdos970.NumberTheoryLean.FullPathCompactSelection.fullCompactReward_measurable line 25
3. theorem OAI.Erdos970.NumberTheoryLean.FullPathCompactSelection.fullCompactReward_envelope line 33
4. theorem OAI.Erdos970.NumberTheoryLean.FullPathCompactSelection.selected_compact_history_bound line 48