OAI/NumberTheory/TwoPoint/Bounds/QualitativeSieveParameters.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A small sieve cutoff for the qualitative multiplier. Truncation uses the same proved finite four-form sieve; its cutoff is chosen so that the entire CRT boundary cost lies far below the available interval length.

  1. def OAI.TwoPointCorrelations.qualitativeSieveHalfOrder line 14
  2. def OAI.TwoPointCorrelations.qualitativeSieveLogCutoff line 16
  3. lemma OAI.TwoPointCorrelations.qualitativeSieveLogCutoff_le_power line 19
  4. structure OAI.TwoPointCorrelations.QualitativeSieveParameters line 26
  5. theorem OAI.TwoPointCorrelations.eventually_qualitativeSieveParameters line 37