OAI/NumberTheory/Ostmann/Construction/SelectedCellTiers.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Finite tier labels for the actual disjoint compensation cells

  1. theorem OAI.Ostmann.selected_centers_pairwise_separated line 11
  2. theorem OAI.Ostmann.selectedTailCellPrimes_disjoint_of_gap line 31
  3. theorem OAI.Ostmann.selected_cells_pairwiseDisjoint line 44
  4. def OAI.Ostmann.finitePrimeCellTier line 56
  5. theorem OAI.Ostmann.finitePrimeCellTier_of_mem line 60
  6. theorem OAI.Ostmann.finitePrimeCellTier_outside line 71
  7. theorem OAI.Ostmann.selected_top_compensation_gap line 78
  8. theorem OAI.Ostmann.finitePrimeCellTier_rest line 89
  9. theorem OAI.Ostmann.exists_selected_prime_tiers line 96
  10. theorem OAI.Ostmann.mem_drop_index line 110
  11. theorem OAI.Ostmann.exists_scheduled_prime_tiers line 120