OAI/NumberTheory/JointDickman/Probability/GraphResidueMean.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.coprime_residue_product_mean line 11
2. theorem OAI.JointDickman.prime_residue_product_mean line 27
3. theorem OAI.JointDickman.congruence_three_root_mean line 58

   Source documentation

   The endpoint congruence contributes its exact density; the remaining three-root factors are independent of it by CRT.

   theorem congruence_three_root_mean (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
       {d : ℕ} [NeZero d] [NeZero (∏ p ∈ P, p)] [∀ p : P, NeZero p.val]
       (hcop : d.Coprime (∏ p ∈ P, p)) (r : ZMod d)
       (a b c : ∀ p : P, ZMod p.val)
       (hab : ∀ p, a p ≠ b p) (hac : ∀ p, a p ≠ c p) (hbc : ∀ p, b p ≠ c p) :
       (∑ x : ZMod (d * ∏ p ∈ P, p),
         (if (x.val : ZMod d) = r then (1 : ℝ) else 0) *
         ∏ p : P, residueWeight (1/2) (a p) (x.val : ZMod p.val) *
           residueWeight (1/2) (b p) (x.val : ZMod p.val) *
           residueWeight (1/2) (c p) (x.val : ZMod p.val)) /
           ((d : ℝ) * ∏ p ∈ P, (p : ℝ)) =
         (1/(d : ℝ)) * ∏ p ∈ P, (1 - 3/(2*(p : ℝ))) := by
   …

   Mentions: OAI.JointDickman.residueWeight