OAI/NumberTheory/Ostmann/Characters/CharacterConstructedRanges.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The selected shells give the actual character prime ranges

  1. theorem OAI.Ostmann.prime_of_loglog_lower line 10
  2. theorem OAI.Ostmann.prime_of_loglog_upper line 19
  3. theorem OAI.Ostmann.CharacterAnchorCell.cell_loglog_bounds line 28
  4. theorem OAI.Ostmann.constructed_character_anchor_ranges line 33
  5. theorem OAI.Ostmann.character_top_shell_log_bounds line 54
  6. theorem OAI.Ostmann.eventual_character_top_dominates_bulk line 63