OAI/NumberTheory/Ostmann/Construction/PrimeShellIndex.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Whole unit shells fit the integer cell scale

Taking the floor of the lower exponential endpoint retains every prime in the shell, including its two boundary cells.

  1. theorem OAI.Ostmann.prime_shell_log_bounds line 18
  2. theorem OAI.Ostmann.prime_shell_index_bounds line 29
  3. theorem OAI.Ostmann.shell_floor_scale line 52
  4. theorem OAI.Ostmann.PublishedProgressionInput.rich_shell_word_priors line 62