OAI/NumberTheory/Ostmann/ZeroDensity/DirichletGraphFactor.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.dirichlet_zpow_apply_nonzero line 13

   Source documentation

   Nonzero powers commute with evaluation also at nonunits. This permits the same bounded extension convention after large coprimalities are removed.

   theorem dirichlet_zpow_apply_nonzero {p : ℕ} (χ : DirichletCharacter ℂ p)
       (e : ℤ) (he : e ≠ 0) (x : ZMod p) : (χ ^ e) x = χ x ^ e := by
   …

2. def OAI.Ostmann.dirichletGraphEdge line 25
3. theorem OAI.Ostmann.dirichletGraphEdge_norm line 29
4. theorem OAI.Ostmann.dirichlet_one_sided_graph_factorization line 36

   Source documentation

   A zero reverse edge leaves exactly one short-modulus character of the long prime. All other factors depend on at most one of the two variables.

   theorem dirichlet_one_sided_graph_factorization {J : Type*} [Fintype J]
       (χ : (Bool ⊕ J) → ∀ p : ℕ, DirichletCharacter ℂ p)
       (b : (Bool ⊕ J) → (Bool ⊕ J) → ℤ)
       (ν : (Bool ⊕ J) → ℕ → ℂ) (fixed : J → ℕ)
       (hν : ∀ i x, ‖ν i x‖ ≤ 1)
       (hself : b (.inl true) (.inl true) = 0 ∧ b (.inl false) (.inl false) = 0)
       (hreverse : b (.inl false) (.inl true) = 0)
       (hforward : b (.inl true) (.inl false) ≠ 0) :
       ∃ U V : ℕ → ℂ, (∀ p, ‖U p‖ ≤ 1) ∧ (∀ q, ‖V q‖ ≤ 1) ∧
         ∀ q p, finiteEdgeWeight (dirichletGraphEdge χ b) ν (twoVertexLabels fixed q p) =
           U p * V q * (χ (.inl true) q ^ b (.inl true) (.inl false)) (p : ZMod q) := by
   …

   Mentions: OAI.Ostmann.finiteEdgeWeight, OAI.Ostmann.dirichletGraphEdge, OAI.Ostmann.twoVertexLabels