OAI/NumberTheory/Ostmann/Preliminaries/FixedShiftInitialSegment.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Restoring the removed initial interval in fixed-shift sieving

  1. theorem OAI.Ostmann.summandPrefix_card_le_initial_add_tail line 13
  2. theorem OAI.Ostmann.sqrt_log_power_initial_small line 24