OAI/NumberTheory/Ostmann/Construction/MatchedDirectedPhase.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.directedPrimePhase_split line 11
2. theorem OAI.Ostmann.matched_directed_phase_quotient line 25

   Source documentation

   The matching transports the first graph to the second set of slots. The translating centers are indexed by actual primes, as in the construction.

   theorem matched_directed_phase_quotient {I J : Type*} [Fintype I] [Fintype J]
       (e : I ≃ J) (χ : J → ∀ p : ℕ, DirichletCharacter ℂ p)
       (p : J → ℕ) (hp : ∀ j, p j ≠ 0) (t : ∀ p : ℕ, ZMod p)
       (ν : I → ℕ → ℂ) (ω : J → ℕ → ℂ)
       (b : I → I → ℤ) (c : J → J → ℤ) (v : ℤ)
       (hc : Pairwise (fun i j => (p i).Coprime (p j)))
       (hb : ∀ i, b i i = 0) (hcdiag : ∀ i, c i i = 0) :
       let : ∀ j, NeZero (p j) := fun j => ⟨hp j⟩
   …