OAI/NumberTheory/TwoPoint/Bounds/FourFormLocal.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Exact local density of the four rough-sieve forms. All coefficients needed to solve pairs are units already over every nonzero modulus; there is no exceptional argument at the prime two.

  1. def OAI.TwoPointCorrelations.zeroResidueIndicator line 14

    Also declared: OAI/NumberTheory/TwoPointCorrelations/FourFormLocal.lean:14 (same declaration text).

  2. def OAI.TwoPointCorrelations.fourFormBad line 17

    Also declared: OAI/NumberTheory/TwoPointCorrelations/FourFormLocal.lean:17 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.fourFormBad_indicator line 20

    Also declared: OAI/NumberTheory/TwoPointCorrelations/FourFormLocal.lean:20 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.add_zero_iff_right line 44

    Also declared: OAI/NumberTheory/TwoPointCorrelations/FourFormLocal.lean:44 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.fourFormBad_count line 56

    Source documentation

    The count is exact for every nonzero modulus, not only prime moduli.

    Also declared: OAI/NumberTheory/TwoPointCorrelations/FourFormLocal.lean:56 (same declaration text).

    lemma fourFormBad_count (D : ℕ) [NeZero D] :
    (∑ x : ZMod D, ∑ y : ZMod D, ∑ z : ZMod D,
      if fourFormBad (x, y, z) then (1 : ℝ) else 0) =
        4 * (D : ℝ) ^ 2 - 6 * D + 3 := by
…

    Mentions: OAI.TwoPointCorrelations.fourFormBad

  6. lemma OAI.TwoPointCorrelations.uniformResidueCube_probability line 65

    Also declared: OAI/NumberTheory/TwoPointCorrelations/FourFormLocal.lean:65 (same declaration text).

  7. def OAI.TwoPointCorrelations.fourFormBadDensity line 76

    Also declared: OAI/NumberTheory/TwoPointCorrelations/FourFormLocal.lean:76 (same declaration text).

  8. theorem OAI.TwoPointCorrelations.fourFormBadDensity_exact line 79

    Also declared: OAI/NumberTheory/TwoPointCorrelations/FourFormLocal.lean:79 (same declaration text).

  9. lemma OAI.TwoPointCorrelations.fourFormBadDensity_nonneg line 83

    Also declared: OAI/NumberTheory/TwoPointCorrelations/FourFormLocal.lean:83 (same declaration text).

  10. theorem OAI.TwoPointCorrelations.fourFormBadDensity_bounds line 86

    Also declared: OAI/NumberTheory/TwoPointCorrelations/FourFormLocal.lean:86 (same declaration text).

  11. theorem OAI.TwoPointCorrelations.fourFormBadDensity_lt_one line 100

    Also declared: OAI/NumberTheory/TwoPointCorrelations/FourFormLocal.lean:100 (same declaration text).

  12. lemma OAI.TwoPointCorrelations.oneFormBadDensity line 111

    Also declared: OAI/NumberTheory/TwoPointCorrelations/FourFormLocal.lean:111 (same declaration text).