OAI/NumberTheory/Jacobsthal/Primes/PaperMissingPrimeWindow.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.NumberTheoryLean.MovingPrimeWindowProbability.source_missing_window_probability line 22
2. theorem OAI.Erdos970.NumberTheoryLean.WeightedMissingPrimeWindow.weighted_missing_prime_window line 116
3. def OAI.Erdos970.NumberTheoryLean.MissingWindowPrimeMass.missingWindowPrefixes line 188
4. theorem OAI.Erdos970.NumberTheoryLean.MissingWindowPrimeMass.moving_missing_prefix_mass line 193
5. theorem OAI.Erdos970.NumberTheoryLean.PaperMissingPrimeWindow.sourceW_le_sourceB_eventually line 240
6. theorem OAI.Erdos970.NumberTheoryLean.PaperMissingPrimeWindow.paper_missing_prime_window_mass line 250