OAI/NumberTheory/Jacobsthal/Primes/PrimeMarginalRecursion.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.PrimeGridKernel.bin line 19
2. theorem OAI.Erdos970.NumberTheoryLean.PrimeGridKernel.mem_bin line 22
3. theorem OAI.Erdos970.NumberTheoryLean.PrimeGridKernel.bin_measurable line 25
4. theorem OAI.Erdos970.NumberTheoryLean.PrimeGridKernel.row_none line 27
5. theorem OAI.Erdos970.NumberTheoryLean.PrimeGridKernel.row_zero_of_large_parent line 31
6. theorem OAI.Erdos970.NumberTheoryLean.PrimeGridKernel.row_zero_above_grid line 45
7. def OAI.Erdos970.NumberTheoryLean.PrimeGridKernel.weakIndices line 52
8. theorem OAI.Erdos970.NumberTheoryLean.PrimeGridKernel.weak_parent_cover line 56
9. theorem OAI.Erdos970.NumberTheoryLean.PrimeGridKernel.regular_parent_cover line 64
10. def OAI.Erdos970.NumberTheoryLean.PrimeGridKernel.mass line 73
11. theorem OAI.Erdos970.NumberTheoryLean.PrimeGridKernel.mass_step line 76
12. def OAI.Erdos970.NumberTheoryLean.PrimeMarginalRecursion.entry line 99
13. def OAI.Erdos970.NumberTheoryLean.PrimeMarginalRecursion.coveredParents line 103
14. theorem OAI.Erdos970.NumberTheoryLean.PrimeMarginalRecursion.weak_coverage line 109
15. theorem OAI.Erdos970.NumberTheoryLean.PrimeMarginalRecursion.regular_coverage line 124
16. theorem OAI.Erdos970.NumberTheoryLean.PrimeMarginalRecursion.covered_recursion line 138
17. theorem OAI.Erdos970.NumberTheoryLean.PrimeMarginalRecursion.weak_recursion line 190
18. theorem OAI.Erdos970.NumberTheoryLean.PrimeMarginalRecursion.regular_recursion line 209