OAI/NumberTheory/Ostmann/Characters/NormalizedResidueFamily.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A single family of normalized transforms for varying sampled primes

  1. def OAI.Ostmann.normalizedResidueFamily line 12

    Source documentation

    The zero modulus is unused by prime samples. This total definition lets both histories evaluate the same transform at their actual sampled prime.

    noncomputable def normalizedResidueFamily (sets : ∀ q : ℕ, Finset (ZMod q))
    (q : ℕ) : ZMod q → ℂ :=
…
  2. theorem OAI.Ostmann.normalizedResidueFamily_eq line 18
  3. theorem OAI.Ostmann.normalizedResidueFamily_zero line 23
  4. theorem OAI.Ostmann.normalizedResidueFamily_energy line 28