OAI/NumberTheory/Ostmann/Preliminaries/FixedShiftRootCutoff.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Integer-root cutoffs for fixed-shift sieving on arbitrary intervals

  1. theorem OAI.Ostmann.nthRoot_tendsto line 14
  2. theorem OAI.Ostmann.nthRoot_log_comparison line 21
  3. theorem OAI.Ostmann.fixedShiftRoot_square_cutoff line 42