OAI/NumberTheory/Ostmann/Construction/ScheduledPrimeRanges.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Live prime ranges of the selected finite schedule

  1. theorem OAI.Ostmann.scheduledSmallCell_property line 10
  2. theorem OAI.Ostmann.mem_initialSmallCellList_of_eq_or_mem line 22
  3. theorem OAI.Ostmann.completedCompensationCell_mem_initial line 29
  4. theorem OAI.Ostmann.scheduledSmallCell_mem_initial line 40
  5. theorem OAI.Ostmann.selected_cell_prime_range line 49
  6. theorem OAI.Ostmann.completedCompensationSets_range line 59
  7. theorem OAI.Ostmann.scheduledRegularPrimeSets_range line 73
  8. theorem OAI.Ostmann.scheduledSmallLower_prime_bound line 98
  9. theorem OAI.Ostmann.scheduledRegularPrimeSets_sub_mass line 110
  10. theorem OAI.Ostmann.scheduledRegularPrior_normalized line 129