OAI/NumberTheory/TwoPointCorrelations/RoughSieveProbability.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The finite sieve applied to the actual one- and four-form rough events. Only the classical reciprocal-prime estimates remain in the quantitative bounds; all finite local and intersection calculations are proved.

  1. def OAI.TwoPointCorrelations.avoidsPrimeSet line 15

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

  2. def OAI.TwoPointCorrelations.fourFormsAvoidPrimeSet line 17

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/RoughSieveProbability.lean:17 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.primeSet_pairwise_coprime line 21

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/RoughSieveProbability.lean:21 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.avoidsPrimeSet_iff_residues line 27

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/RoughSieveProbability.lean:27 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.fourFormsAvoidPrimeSet_iff_residues line 31

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/RoughSieveProbability.lean:31 (same declaration text).

  6. theorem OAI.TwoPointCorrelations.rough_interval_probability line 44

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/RoughSieveProbability.lean:44 (same declaration text).

  7. theorem OAI.TwoPointCorrelations.rough_cube_probability line 73

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/RoughSieveProbability.lean:73 (same declaration text).