OAI/NumberTheory/JointDickman/Probability/ResidueProductMean.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.residue_divisor_mean line 12
2. theorem OAI.JointDickman.residue_divisor_product_mean line 19

   Source documentation

   Uniform residues give the exact finite Euler-product mean.

   theorem residue_divisor_product_mean (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
       {q : ℕ} [NeZero q] (hdiv : (∏ p ∈ P, p) ∣ q) (b : ℕ → ℝ) :
       (∑ a : ZMod q, ∏ p ∈ P, if p ∣ a.val then 1+b p else 1) / (q : ℝ) =
         ∏ p ∈ P, (1+b p/(p : ℝ)) := by
   …