OAI/NumberTheory/Ostmann/Preliminaries/FixedShiftCount.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Fixed-shift counting, manuscript Lemma 2.1

The proof uses the proved additive sieve, exact missing-class weights, Mertens bounds, and integer-root cutoffs. All removed initial points are restored.

  1. theorem OAI.Ostmann.fixed_shift_count line 17