OAI/NumberTheory/Ostmann/Characters/FinitePoissonTransform.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Poisson summation with a concrete finite periodic weight

  1. theorem OAI.Ostmann.schwartz_int_norm_summable line 13
  2. theorem OAI.Ostmann.fourier_residue line 18
  3. theorem OAI.Ostmann.schwartz_fourier_residue_summable line 27
  4. theorem OAI.Ostmann.finite_poisson_transform line 36

    Source documentation

    The lattice spacing has been absorbed into the Schwartz function. This exact identity retains the finite Fourier coefficient and all signs.

    theorem finite_poisson_transform {N : ℕ} [NeZero N] (f : 𝓢(ℝ, ℂ)) (F : ZMod N → ℂ) :
    (∑ a : ZMod N, F a * ∑' n : ℤ, f ((a.val : ℝ) / N + n)) =
      (N : ℂ) * ∑' n : ℤ, 𝓕 f (n : ℝ) * additiveFourier F (-(n : ZMod N)) := by
…

    Mentions: OAI.Ostmann.additiveFourier