OAI/NumberTheory/Jacobsthal/Primes/PrimeOccupationDensity.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.NumberTheoryLean.OriginalPrimeOccupationLimit.original_prime_continuous_occupation_limit line 20
  2. theorem OAI.Erdos970.NumberTheoryLean.OriginalPrimeOccupationLimit.literal_original_prime_occupation line 54
  3. def OAI.Erdos970.NumberTheoryLean.PrimeOccupationDensity.baseMeasure line 84
  4. def OAI.Erdos970.NumberTheoryLean.PrimeOccupationDensity.density line 86
  5. theorem OAI.Erdos970.NumberTheoryLean.PrimeOccupationDensity.density_nonneg line 89
  6. theorem OAI.Erdos970.NumberTheoryLean.PrimeOccupationDensity.density_measurable line 95
  7. def OAI.Erdos970.NumberTheoryLean.PrimeOccupationDensity.limitingMeasure line 101
  8. theorem OAI.Erdos970.NumberTheoryLean.PrimeOccupationDensity.limiting_absolutelyContinuous line 104
  9. theorem OAI.Erdos970.NumberTheoryLean.PrimeOccupationDensity.invariant_ratio_null line 107
  10. theorem OAI.Erdos970.NumberTheoryLean.PrimeOccupationDensity.invariant_ratio_level_null line 113
  11. theorem OAI.Erdos970.NumberTheoryLean.PrimeOccupationDensity.exponential_level_null line 116
  12. theorem OAI.Erdos970.NumberTheoryLean.PrimeOccupationDensity.gap_boundary_null line 122
  13. theorem OAI.Erdos970.NumberTheoryLean.PrimeOccupationDensity.ratio_boundary_null line 129
  14. def OAI.Erdos970.NumberTheoryLean.PrimeOccupationDensity.rectangleBoundary line 136
  15. theorem OAI.Erdos970.NumberTheoryLean.PrimeOccupationDensity.rectangle_boundary_null line 139