OAI/NumberTheory/Jacobsthal/Paths/PairedHitting.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.PairedHitting.pairedOdd line 16
2. instance OAI.Erdos970.NumberTheoryLean.PairedHitting.pairedOdd_isMarkovKernel line 18
3. theorem OAI.Erdos970.NumberTheoryLean.PairedHitting.pairedOdd_map_ratio line 20
4. theorem OAI.Erdos970.NumberTheoryLean.PairedHitting.pairedOdd_progress line 29
5. def OAI.Erdos970.NumberTheoryLean.PairedHitting.pairedRegeneration line 40
6. theorem OAI.Erdos970.NumberTheoryLean.PairedHitting.pairedRegeneration_measurable line 42
7. def OAI.Erdos970.NumberTheoryLean.PairedHitting.pairedKilled line 45
8. instance OAI.Erdos970.NumberTheoryLean.PairedHitting.pairedKilled_isFiniteKernel line 48
9. instance OAI.Erdos970.NumberTheoryLean.PairedHitting.pairedKilled_pow_isFiniteKernel line 50
10. def OAI.Erdos970.NumberTheoryLean.PairedHitting.hitBy line 58
11. theorem OAI.Erdos970.NumberTheoryLean.PairedHitting.hitBy_measurable line 62
12. theorem OAI.Erdos970.NumberTheoryLean.PairedHitting.paired_survival_balance line 68
13. theorem OAI.Erdos970.NumberTheoryLean.PairedHitting.hitBy_le_one line 92
14. theorem OAI.Erdos970.NumberTheoryLean.PairedHitting.hitBy_lower line 97
15. theorem OAI.Erdos970.NumberTheoryLean.PairedHitting.compact_paired_hit line 142
16. theorem OAI.Erdos970.NumberTheoryLean.PairedHitting.paired_survival_le_one line 153
17. theorem OAI.Erdos970.NumberTheoryLean.PairedHitting.paired_survival_antitone line 158
18. theorem OAI.Erdos970.NumberTheoryLean.PairedHitting.compact_paired_survival line 168