OAI/NumberTheory/PrimeGaps/DensityBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem344.initialCount_le line 7
  2. theorem OAI.Problem344.initialCount_mono line 15
  3. theorem OAI.Problem344.initialCount_div_le_one line 24
  4. theorem OAI.Problem344.density_witnesses_bddAbove line 32
  5. theorem OAI.Problem344.zero_mem_density_witnesses line 39
  6. theorem OAI.Problem344.lowerAsymptoticDensity_nonneg line 46
  7. theorem OAI.Problem344.lowerAsymptoticDensity_le_one line 50
  8. theorem OAI.Problem344.le_lowerAsymptoticDensity_of_linear_count line 56
  9. theorem OAI.Problem344.positive_lowerAsymptoticDensity_of_linear_count line 69