OAI/NumberTheory/Ostmann/Tree/TwoVertexReindex.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.OtherVertices line 12
2. def OAI.Ostmann.twoVertexEquiv line 14
3. theorem OAI.Ostmann.twoVertexEquiv_short line 33
4. theorem OAI.Ostmann.twoVertexEquiv_long line 36
5. theorem OAI.Ostmann.twoVertexEquiv_other line 39
6. theorem OAI.Ostmann.finiteEdgeWeight_two_vertices line 44

   Source documentation

   Reindexing is exact even when the unary factors contain role membership or counterpart-prior restrictions.

   theorem finiteEdgeWeight_two_vertices {V : Type*} [Fintype V] (a b : V) (hab : a ≠ b)
       (χ : V → ∀ p : ℕ, DirichletCharacter ℂ p) (graph : V → V → ℤ)
       (ν : V → ℕ → ℂ) (p : Bool ⊕ OtherVertices a b → ℕ) :
       finiteEdgeWeight (dirichletGraphEdge (fun i => χ (twoVertexEquiv a b hab i))
           (fun i j => graph (twoVertexEquiv a b hab i) (twoVertexEquiv a b hab j)))
         (fun i => ν (twoVertexEquiv a b hab i)) p =
       finiteEdgeWeight (dirichletGraphEdge χ graph) ν (fun v => p ((twoVertexEquiv a b hab).symm v)) := by
   …

   Mentions: OAI.Ostmann.OtherVertices, OAI.Ostmann.finiteEdgeWeight, OAI.Ostmann.dirichletGraphEdge, OAI.Ostmann.twoVertexEquiv

7. theorem OAI.Ostmann.reindexed_one_sided_conditions line 64
8. theorem OAI.Ostmann.selected_graph_factorization line 74

   Source documentation

   All the unselected vertices are fixed only after the two genuine labels have been isolated. Their factors contribute bounded unary functions.

   theorem selected_graph_factorization {V : Type*} [Fintype V] (a b : V) (hab : a ≠ b)
       (χ : V → ∀ p : ℕ, DirichletCharacter ℂ p) (graph : V → V → ℤ)
       (ν : V → ℕ → ℂ) (outside : OtherVertices a b → ℕ)
       (hν : ∀ v x, ‖ν v x‖ ≤ 1) (hself : graph a a = 0 ∧ graph b b = 0)
       (hreverse : graph b a = 0) (hforward : graph a b ≠ 0) :
       ∃ U W : ℕ → ℂ, (∀ p, ‖U p‖ ≤ 1) ∧ (∀ q, ‖W q‖ ≤ 1) ∧
         ∀ q p, finiteEdgeWeight (dirichletGraphEdge χ graph) ν
           (fun v => twoVertexLabels outside q p ((twoVertexEquiv a b hab).symm v)) =
             U p * W q * (χ a q ^ graph a b) (p : ZMod q) := by
   …

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