OAI/NumberTheory/TwoPointCorrelations/SieveIntersections.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact selected-modulus intersection estimates on a single fixed interval or cube. These discharge the arithmetic premise of Bonferroni.

  1. lemma OAI.TwoPointCorrelations.selected_pairwise_coprime line 13

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/SieveIntersections.lean:13 (same declaration text).

  2. theorem OAI.TwoPointCorrelations.sieve_one_intersection line 19

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/SieveIntersections.lean:19 (same declaration text).

  3. theorem OAI.TwoPointCorrelations.sieve_cube_intersection line 48

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/SieveIntersections.lean:48 (same declaration text).