OAI/NumberTheory/Ostmann/Characters/SparseAdditiveKernel.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual additive kernel of the sparse spectral projection

  1. def OAI.Ostmann.sparseAdditiveKernel line 10
  2. theorem OAI.Ostmann.sparseAdditiveKernel_formula line 14
  3. theorem OAI.Ostmann.sparseAdditiveKernel_fourier line 21
  4. theorem OAI.Ostmann.sparseAdditiveKernel_real line 30
  5. theorem OAI.Ostmann.sparseAdditiveKernel_norm_le line 46
  6. theorem OAI.Ostmann.sparseAdditiveKernel_action line 58

    Source documentation

    The raw kernel matrix is precisely the scalar multiple of the projection; no normalization or discarded frequency is hidden in the identification.

    theorem sparseAdditiveKernel_action {p : ℕ} [NeZero p]
    (E : Finset (ZMod p)) (t : ℝ) (f : ZMod p → ℂ) (x : ZMod p) :
    (∑ y, f y * sparseAdditiveKernel E t (x - y)) =
      (t : ℂ) * finiteSpectralProjection E f x := by
…

    Mentions: OAI.Ostmann.sparseAdditiveKernel, OAI.Ostmann.finiteSpectralProjection