SieveCRT.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Exact CRT factorization of the one- and three-variable local sieve models. The interval/box errors are kept separate in ResidueBox.

lemma OAI.TwoPointCorrelations.FiniteLaw.probability_equiv line 14
Also declared: OAI/NumberTheory/TwoPointCorrelations/SieveCRT.lean:14 (same declaration text).
def OAI.TwoPointCorrelations.sieveCubeCRT line 22
Also declared: OAI/NumberTheory/TwoPointCorrelations/SieveCRT.lean:22 (same declaration text).
lemma OAI.TwoPointCorrelations.uniformZModLaw_crt_weight line 46
Also declared: OAI/NumberTheory/TwoPointCorrelations/SieveCRT.lean:46 (same declaration text).
lemma OAI.TwoPointCorrelations.uniformCube_crt_weight line 55
Also declared: OAI/NumberTheory/TwoPointCorrelations/SieveCRT.lean:55 (same declaration text).

theorem OAI.TwoPointCorrelations.sieveCRT_one_probability line 66

Source documentation

CRT evaluates an intersection of one-variable local conditions exactly.

Also declared: OAI/NumberTheory/TwoPointCorrelations/SieveCRT.lean:66 (same declaration text).

theorem sieveCRT_one_probability {ι : Type*} [Fintype ι] [DecidableEq ι]
    (s : ι → ℕ) [∀ i, NeZero (s i)]
    (hcop : Pairwise (fun i j => (s i).Coprime (s j)))
    (E : ∀ i, ZMod (s i) → Prop) :
    (uniformZModLaw (∏ i, s i)).probability
      (fun x => ∀ i, E i (ZMod.prodEquivPi s hcop x i)) =
      ∏ i, (uniformZModLaw (s i)).probability (E i) := by
…

Mentions: OAI.TwoPointCorrelations.uniformZModLaw

theorem OAI.TwoPointCorrelations.sieveCRT_cube_probability line 83

Source documentation

CRT evaluates an intersection of local three-variable conditions exactly, retaining the dependence among the forms at each individual prime.

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

theorem sieveCRT_cube_probability {ι : Type*} [Fintype ι] [DecidableEq ι]
    (s : ι → ℕ) [∀ i, NeZero (s i)]
    (hcop : Pairwise (fun i j => (s i).Coprime (s j)))
    (E : ∀ i, (ZMod (s i) × ZMod (s i) × ZMod (s i)) → Prop) :
    (uniformResidueCubeLaw (∏ i, s i)).probability
      (fun x => ∀ i, E i (sieveCubeCRT s hcop x i)) =
      ∏ i, (uniformResidueCubeLaw (s i)).probability (E i) := by
…

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