OAI/NumberTheory/TwoPoint/Walks/ReducedIncidenceWalk.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Concrete alternating run/transition lists give reduced incidence walks.

  1. def OAI.TwoPointCorrelations.NoImmediateReturn line 13
  2. theorem OAI.TwoPointCorrelations.walk_reduced_iff_noImmediateReturn line 17
  3. theorem OAI.TwoPointCorrelations.vertex_list_isPath line 31
  4. def OAI.TwoPointCorrelations.incidenceVertices line 41

    Source documentation

    Each pair records a transition point and the next run label.

    def incidenceVertices (i : ι) : List (V × ι) → List (ι ⊕ V)
  | [] => [.inl i]
  | (x, j) :: rest => .inl i :: .inr x :: incidenceVertices j rest
  5. def OAI.TwoPointCorrelations.IncidenceChain line 45
  6. def OAI.TwoPointCorrelations.IncidenceReduced line 53

    Source documentation

    Adjacent run labels differ, and consecutive transition points differ. The latter is exactly the nonzero run-increment condition.

    def IncidenceReduced (i : ι) : List (V × ι) → Prop
  | [] => True
  | (x, j) :: rest => i ≠ j ∧
      (∀ y k, rest.head? = some (y, k) → x ≠ y) ∧ IncidenceReduced j rest

omit [AddCommGroup V] in
  7. lemma OAI.TwoPointCorrelations.incidenceVertices_ne_nil line 59
  8. theorem OAI.TwoPointCorrelations.incidenceVertices_isChain line 63
  9. theorem OAI.TwoPointCorrelations.incidenceVertices_noImmediateReturn line 77
  10. theorem OAI.TwoPointCorrelations.incidence_vertices_simple line 96

    Source documentation

    The actual alternating incidence walk is simple. In particular, its line sequence is determined by its two endpoints in the forest.

    theorem incidence_vertices_simple (anchor d : ι → V) (hd : LinearIndependent K d)
    (i : ι) (steps : List (V × ι))
    (hc : IncidenceChain (K := K) anchor d i steps) (hr : IncidenceReduced i steps) :
…

    Mentions: OAI.TwoPointCorrelations.IncidenceChain, OAI.TwoPointCorrelations.IncidenceReduced