OAI/NumberTheory/JointDickman/Arithmetic/SieveRectangleCRT.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.crt_rectangle_period_sum line 13

   Source documentation

   Complete residue squares factor by two applications of the CRT.

   theorem crt_rectangle_period_sum {ι : Type*} [Fintype ι] [DecidableEq ι]
       (m : ι → ℕ) [∀ i, NeZero (m i)] (hm : ∀ i, 0 < m i)
       (hcop : Pairwise (fun i j => (m i).Coprime (m j)))
       (F : ∀ i, ZMod (m i) → ZMod (m i) → ℝ) :
       (∑ r ∈ range (∏ i, m i), ∑ s ∈ range (∏ i, m i),
         ∏ i, F i (r : ZMod (m i)) (s : ZMod (m i))) =
         ∏ i, ∑ r : ZMod (m i), ∑ s : ZMod (m i), F i r s := by
   …

2. theorem OAI.JointDickman.crt_pair_period_count line 29

   Source documentation

   A family of prescribed residue-pair sets has exactly the product of its local cardinalities in a complete square.

   theorem crt_pair_period_count {ι : Type*} [Fintype ι] [DecidableEq ι]
       (m : ι → ℕ) (hm : ∀ i, 0 < m i)
       (hcop : Pairwise (fun i j => (m i).Coprime (m j)))
       (A : ∀ i, Finset (ZMod (m i) × ZMod (m i))) :
       (∑ r ∈ range (∏ i, m i), ∑ s ∈ range (∏ i, m i),
         if ∀ i, ((r : ZMod (m i)), (s : ZMod (m i))) ∈ A i then (1 : ℝ) else 0) =
         ∏ i, ((A i).card : ℝ) := by
   …

3. theorem OAI.JointDickman.crt_pair_rectangle_error line 56

   Source documentation

   The two-dimensional CRT remainder retains the exact number of prescribed residue pairs.

   theorem crt_pair_rectangle_error {ι : Type*} [Fintype ι] [DecidableEq ι]
       (m : ι → ℕ) (hm : ∀ i, 0 < m i)
       (hcop : Pairwise (fun i j => (m i).Coprime (m j)))
       (A : ∀ i, Finset (ZMod (m i) × ZMod (m i)))
       {a b c d : ℕ} (hab : a ≤ b) (hcd : c ≤ d) :
       |(∑ r ∈ Ico a b, ∑ s ∈ Ico c d,
           if ∀ i, ((r : ZMod (m i)), (s : ZMod (m i))) ∈ A i then (1 : ℝ) else 0) -
         (((b : ℝ) - a) * ((d : ℝ) - c) / (∏ i, (m i : ℝ)) ^ 2) *
           ∏ i, ((A i).card : ℝ)| ≤
         2 * ((((b : ℝ) - a) + ((d : ℝ) - c)) / (∏ i, (m i : ℝ)) + 2) *
           ∏ i, ((A i).card : ℝ) := by
   …

4. theorem OAI.JointDickman.prime_pair_rectangle_error line 88

   Source documentation

   Prime-set specialization with the local densities already factored.

   theorem prime_pair_rectangle_error (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
       (A : ∀ p : ℕ, Finset (ZMod p × ZMod p))
       {a b c d : ℕ} (hab : a ≤ b) (hcd : c ≤ d) :
       |(∑ r ∈ Ico a b, ∑ s ∈ Ico c d,
           if ∀ p ∈ P, ((r : ZMod p), (s : ZMod p)) ∈ A p then (1 : ℝ) else 0) -
         ((b : ℝ) - a) * ((d : ℝ) - c) *
           ∏ p ∈ P, ((A p).card : ℝ) / (p : ℝ) ^ 2| ≤
         2 * ((((b : ℝ) - a) + ((d : ℝ) - c)) / (∏ p ∈ P, (p : ℝ)) + 2) *
           ∏ p ∈ P, ((A p).card : ℝ) := by
   …