OAI/NumberTheory/JointDickman/Analysis/CharacterResidues.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.progressionSum line 14
2. theorem OAI.JointDickman.progressionSum_characters line 18
3. theorem OAI.JointDickman.progressionSum_error_le line 39

   Source documentation

   The normalized character average loses no factor depending on the modulus.

   theorem progressionSum_error_le {q : ℕ} [NeZero q]
       (S : Finset ℕ) (w : ℕ → ℝ) (r : (ZMod q)ˣ) {E : ℝ} (hE : 0 ≤ E)
       (hunit : ∀ n ∈ S, w n ≠ 0 → IsUnit (n : ZMod q))
       (hbound : ∀ χ : DirichletCharacter ℂ q, χ ≠ 1 →
         ‖∑ n ∈ S, (w n : ℂ) * χ (n : ZMod q)‖ ≤ E) :
       |progressionSum S w (r : ZMod q) - (∑ n ∈ S, w n) / (q.totient : ℝ)| ≤ E := by
   …

   Mentions: OAI.JointDickman.progressionSum

4. theorem OAI.JointDickman.roughSquarefreeWeight_coprime line 86