OAI/NumberTheory/Ostmann/Construction/DirectedPrimePhase.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.directedPrimePhase line 11
2. def OAI.Ostmann.initialDirectedGraph line 17
3. theorem OAI.Ostmann.initial_row_product line 20
4. theorem OAI.Ostmann.tupleGraphPhase_eq_directed line 32

   Source documentation

   The graph phase obtained by Poisson summation is the level-zero specialization of the phase maintained through the transfers.

   theorem tupleGraphPhase_eq_directed {I : Type*} [Fintype I] (p : I → ℕ)
       [∀ i, NeZero (p i)] (χ : ∀ i, DirichletCharacter ℂ (p i))
       (t : ∀ i, ZMod (p i)) (v : ℤ) :
       tupleGraphPhase p χ t v = directedPrimePhase p χ t
         (fun i => primitiveGaussPhase (χ i) * (χ i)⁻¹ (v : ZMod (p i))) initialDirectedGraph v := by
   …

   Mentions: OAI.Ostmann.tupleGraphPhase, OAI.Ostmann.directedPrimePhase, OAI.Ostmann.primitiveGaussPhase, OAI.Ostmann.initialDirectedGraph

5. theorem OAI.Ostmann.directedPrimePhase_norm_le_one line 43
6. theorem OAI.Ostmann.initialDirectedGraph_regular line 56