OAI/NumberTheory/Ostmann/Construction/SelectedInitialPrimeLower.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Lower endpoints for every live prime in the original initial prior

  1. theorem OAI.Ostmann.initial_selected_centers_lower line 11
  2. theorem OAI.Ostmann.selected_initial_prior_lower line 29
  3. theorem OAI.Ostmann.eventual_initial_selected_centers_lower line 62
  4. theorem OAI.Ostmann.eventual_selected_initial_prime_lower line 91