OAI/NumberTheory/Jacobsthal/Primes/ConditionalPrimeBins.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.PrimeCompletedIntervalUpper.closedLiveBin line 18
2. theorem OAI.Erdos970.NumberTheoryLean.PrimeCompletedIntervalUpper.mem_closedLiveBin_some line 23
3. theorem OAI.Erdos970.NumberTheoryLean.PrimeCompletedIntervalUpper.not_mem_closedLiveBin_none line 26
4. theorem OAI.Erdos970.NumberTheoryLean.PrimeCompletedIntervalUpper.chain_closedBin_formula line 31
5. theorem OAI.Erdos970.NumberTheoryLean.PrimeCompletedIntervalUpper.chain_interval_le_tilt line 44
6. theorem OAI.Erdos970.NumberTheoryLean.PrimeCompletedIntervalUpper.prime_completed_interval_upper line 61
7. theorem OAI.Erdos970.NumberTheoryLean.ConditionalPrimeBins.multiplier_valid_antitone line 89
8. theorem OAI.Erdos970.NumberTheoryLean.ConditionalPrimeBins.retained_tilt_le_multiplier line 105
9. theorem OAI.Erdos970.NumberTheoryLean.ConditionalPrimeBins.retained_conditional_bin line 124
10. theorem OAI.Erdos970.NumberTheoryLean.ConditionalPrimeBins.actual_conditional_bin line 162