OAI/NumberTheory/Ostmann/Characters/TupleCharacterPoisson.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Poisson summation and the initial graph phase of a character tuple

  1. def OAI.Ostmann.primitiveGaussPhase line 13
  2. theorem OAI.Ostmann.primitiveGaussPhase_norm line 17
  3. theorem OAI.Ostmann.inverse_character_inverse_unit line 28
  4. def OAI.Ostmann.tupleGraphPhase line 35
  5. theorem OAI.Ostmann.tuple_character_fourier line 44

    Source documentation

    Each off-diagonal edge has exponent one at level zero, including the inverse characters assigned to conjugate slots.

    theorem tuple_character_fourier {I : Type*} [Fintype I] (p : I → ℕ)
    [∀ i, NeZero (p i)] [NeZero (∏ i, p i)]
    (hc : Pairwise (fun i j => (p i).Coprime (p j)))
    (χ : ∀ i, DirichletCharacter ℂ (p i)) (hχ : ∀ i, (χ i).IsPrimitive)
    (t : ∀ i, ZMod (p i)) (v : ℤ) :
    additiveFourier (tupleCRTFunction p hc (fun i x => χ i (x - t i))) (-(v : ZMod (∏ i, p i))) =
      (Real.sqrt (∏ i, p i : ℕ) : ℂ)⁻¹ * tupleGraphPhase p χ t v := by
…

    Mentions: OAI.Ostmann.additiveFourier, OAI.Ostmann.tupleCRTFunction, OAI.Ostmann.tupleGraphPhase

  6. theorem OAI.Ostmann.tuple_character_poisson line 85
  7. theorem OAI.Ostmann.tupleGraphPhase_norm_le_one line 100
  8. theorem OAI.Ostmann.tupleGraphPhase_zero line 114
  9. theorem OAI.Ostmann.tuple_character_poisson_normalized line 121