OAI/NumberTheory/Ostmann/Construction/OriginalSignedFourier.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.primeDivisorSignedFrequency line 12
2. def OAI.Ostmann.originalSignedFourier line 23
3. theorem OAI.Ostmann.primeDivisorSignedFrequency_split line 28
4. theorem OAI.Ostmann.quadraticSymbolCoefficient_conj line 47
5. theorem OAI.Ostmann.originalSignedFourier_split line 53

   Source documentation

   The entire divisor sum has a common conjugation sign. Thus the positive half controls the signed expression before any absolute values are distributed.

   theorem originalSignedFourier_split (Q : Finset ℕ) (hQ : ∀ p ∈ Q, p.Prime)
       (D : ∀ p : ℕ, Finset (ZMod p)) (M N h₀ : ℕ)
       (θ R H : ℝ) (Φ : 𝓢(ℝ, ℂ)) (hM : 1 < M) (hR : 0 < R) (hH : 0 ≤ H)
       (hcut : H * R * Q.toList.prod ≤ N)
       (hΦ : ∀ x, Φ (-x) = conj (Φ x)) (hsupp : ∀ x : ℝ, H < x → Φ x = 0) :
       originalSignedFourier Q hQ D M h₀ θ R Φ =
         originalPositiveFourier Q hQ D M N h₀ θ R Φ +
         (jacobiSym (-1) M : ℂ) * conj (originalPositiveFourier Q hQ D M N h₀ θ R Φ) := by
   …

   Mentions: OAI.Ostmann.originalSignedFourier, OAI.Ostmann.originalPositiveFourier

6. theorem OAI.Ostmann.originalSignedFourier_norm_le line 73