OAI/NumberTheory/TwoPoint/Bounds/ResidueSampling.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A fixed finite interval sample space for every sieve intersection. The modulus may vary with the selected primes, but the actual sample law in these identities never changes.

  1. def OAI.TwoPointCorrelations.uniformFiniteLaw line 15

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ResidueSampling.lean:15 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.uniformFiniteLaw_average line 20

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

  3. lemma OAI.TwoPointCorrelations.intervalResidueLaw_average_uniform line 25

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ResidueSampling.lean:25 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.uniformCube_average_residues line 35

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ResidueSampling.lean:35 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.uniformCube_probability_residues line 70

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ResidueSampling.lean:70 (same declaration text).

  6. theorem OAI.TwoPointCorrelations.sieveCRT_cube_sample_discrepancy line 81

    Source documentation

    Exact CRT intersections on a fixed uniform interval cube, with their complete finite boundary error.

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ResidueSampling.lean:81 (same declaration text).

    theorem sieveCRT_cube_sample_discrepancy {ι : Type*} [Fintype ι] [DecidableEq ι]
    (s : ι → ℕ) [∀ i, NeZero (s i)]
    (hcop : Pairwise (fun i j => (s i).Coprime (s j)))
    (A : ZMod (∏ i, s i) × ZMod (∏ i, s i) × ZMod (∏ i, s i))
    (N : ℕ) [NeZero N]
    (E : ∀ i, (ZMod (s i) × ZMod (s i) × ZMod (s i)) → Prop) :
    |(uniformFiniteLaw (Fin N × Fin N × Fin N)).probability
        (fun j => ∀ i, E i (sieveCubeCRT s hcop
          (A.1 + (j.1.val : ZMod (∏ i, s i)),
            A.2.1 + (j.2.1.val : ZMod (∏ i, s i)),
            A.2.2 + (j.2.2.val : ZMod (∏ i, s i))) i)) -
      ∏ i, (uniformResidueCubeLaw (s i)).probability (E i)| ≤
…

    Mentions: OAI.TwoPointCorrelations.uniformFiniteLaw, OAI.TwoPointCorrelations.sieveCubeCRT, OAI.TwoPointCorrelations.uniformResidueCubeLaw

  7. lemma OAI.TwoPointCorrelations.uniformInterval_probability_residues line 98

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ResidueSampling.lean:98 (same declaration text).

  8. lemma OAI.TwoPointCorrelations.interval_probability_discrepancy line 105

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ResidueSampling.lean:105 (same declaration text).

  9. theorem OAI.TwoPointCorrelations.sieveCRT_one_sample_discrepancy line 121

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ResidueSampling.lean:121 (same declaration text).

  10. lemma OAI.TwoPointCorrelations.sieveCubeCRT_natCast line 132

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ResidueSampling.lean:132 (same declaration text).