OAI/NumberTheory/TwoPointCorrelations/FiniteRoughSieve.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite rough-sieve bounds with every intersection error discharged by CRT on the actual interval sample space.

  1. theorem OAI.TwoPointCorrelations.finite_interval_sieve line 15

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/FiniteRoughSieve.lean:15 (same declaration text).

  2. theorem OAI.TwoPointCorrelations.finite_cube_sieve line 36

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/FiniteRoughSieve.lean:36 (same declaration text).