OAI/NumberTheory/Ostmann/Construction/OriginalFourierCoefficients.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.originalPositiveFourier line 12
2. theorem OAI.Ostmann.quadraticArrayStatistic_finset line 17
3. theorem OAI.Ostmann.originalPositiveFourier_expansion line 28

   Source documentation

   This is the exact finite form of equation (src8). Its coefficients are the same ones whose uniform moments satisfy the stated bounds.

   theorem originalPositiveFourier_expansion (Q : Finset ℕ) (hQ : ∀ p ∈ Q, p.Prime)
       (D : ∀ p : ℕ, Finset (ZMod p)) (M N h₀ : ℕ) [NeZero M]
       (θ R H : ℝ) (Φ : 𝓢(ℝ, ℂ))
       (hR : 0 < R) (hH : 0 ≤ H) (hN : 1 ≤ N)
       (hcut : H * R * Q.toList.prod ≤ N) (hΦ : ∀ x : ℝ, H < x → Φ x = 0) :
       originalPositiveFourier Q hQ D M N h₀ θ R Φ =
         ∑ P ∈ M.divisors, (ArithmeticFunction.moebius P : ℂ) *
           quadraticArrayStatistic (squarefreeKernelSupport Q.toList.prod N) M
             (arithmeticQuadraticCoefficient Q hQ D Φ R P M h₀ θ) := by
   …

   Mentions: OAI.Ostmann.originalPositiveFourier, OAI.Ostmann.quadraticArrayStatistic, OAI.Ostmann.squarefreeKernelSupport, OAI.Ostmann.arithmeticQuadraticCoefficient