OAI/NumberTheory/Ostmann/QuadraticCenter/AmplificationWeight.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.amplificationWeight line 11
2. theorem OAI.Ostmann.amplificationWeight_pos line 15
3. theorem OAI.Ostmann.amplificationWeight_le line 24
4. theorem OAI.Ostmann.amplificationWeight_lower line 41
5. theorem OAI.Ostmann.exp_le_amplificationWeight line 53
6. def OAI.Ostmann.primeDivisorDensity line 69
7. theorem OAI.Ostmann.primeDivisorDensity_intCast line 79
8. theorem OAI.Ostmann.amplificationWeight_expansion line 90

   Source documentation

   Exact divisor expansion, with the same CRT density functions as those already used in the Fourier coefficient construction.

   theorem amplificationWeight_expansion (Q : Finset ℕ) (hQ : ∀ p ∈ Q, p.Prime)
       (D : ∀ p : ℕ, Finset (ZMod p)) (n : ℤ) :
       (amplificationWeight Q D n : ℂ) =
         ∑ U ∈ Q.powerset, (1 / 16 : ℂ) ^ U.card *
           primeDivisorDensity Q hQ D U (n : ZMod U.toList.prod) := by
   …

   Mentions: OAI.Ostmann.amplificationWeight, OAI.Ostmann.primeDivisorDensity