OAI/NumberTheory/Ostmann/Arithmetic/PeriodicWeightPoisson.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Poisson summation gives the exact total amplification weight

  1. theorem OAI.Ostmann.scaled_periodic_poisson line 12
  2. theorem OAI.Ostmann.periodic_poisson_single_frequency line 30
  3. theorem OAI.Ostmann.amplification_total_weight line 53

    Source documentation

    Exact form of the total-weight identity for the manuscript's original positive periodic weight.

    theorem amplification_total_weight (Q : Finset ℕ) (hQ : ∀ p ∈ Q, p.Prime)
    (D : ∀ p : ℕ, Finset (ZMod p)) (ψ : 𝓢(ℝ, ℂ)) (X H : ℝ) (hX : 0 < X)
    (hH : H < X / Q.toList.prod) (hsupp : ∀ x : ℝ, H < |x| → 𝓕 ψ x = 0) :
    (∑' n : ℤ, physicalWeight Q D ψ X n) = X * (𝓕 ψ 0).re := by
…

    Mentions: OAI.Ostmann.physicalWeight