OAI/NumberTheory/Ostmann/Characters/NormalizedCharacterPoisson.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.jacobiGaussPhase line 13
2. theorem OAI.Ostmann.jacobiGaussPhase_norm line 16
3. theorem OAI.Ostmann.poisson_sqrt_normalizer line 27
4. theorem OAI.Ostmann.normalized_jacobi_poisson line 47

   Source documentation

   The scalar outside the signed frequency sum has modulus sqrt(X). The translation is the actual CRT lift, not an independent phase parameter.

   theorem normalized_jacobi_poisson {d M : ℕ} [NeZero d] [NeZero M]
       (hcop : d.Coprime M) (hM : Squarefree M) (hodd : Odd M)
       (f : ZMod d → ℂ) (t : ZMod M) (h₀ : ℕ)
       (hlift : (d : ℤ) ∣ (t.val : ℤ) + (M : ℤ) * h₀)
       (ψ : 𝓢(ℝ, ℂ)) (X : ℝ) (hX : 0 < X) :
       (∑' n : ℤ, f (n : ZMod d) * (jacobiSym ((n : ℤ) - t.val) M : ℂ) *
           ψ ((n : ℝ) / X)) =
         (Real.sqrt X : ℂ) * jacobiGaussPhase M * (realJacobi d M : ℂ) *
           ((Real.sqrt ((M : ℝ) / X * d) : ℂ)⁻¹ *
             ∑' u : ℤ, integerQuadraticFrequency (densityFourier f)
               (-(M : ZMod d)⁻¹) ((h₀ : ℝ) + (t.val : ℝ) / M)
               (𝓕 ψ) ((M : ℝ) / X) M u) := by
   …

   Mentions: OAI.Ostmann.jacobiGaussPhase, OAI.Ostmann.realJacobi, OAI.Ostmann.integerQuadraticFrequency, OAI.Ostmann.densityFourier