OAI/NumberTheory/TwoPoint/Walks/IncidenceDecoding.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The regular-part decoder recovers the original run labels.

  1. theorem OAI.TwoPointCorrelations.incidenceVertices_length line 12
  2. theorem OAI.TwoPointCorrelations.evenEntries_incidenceVertices line 23

    Source documentation

    Taking even entries removes transition points and retains exactly the line vertex for each run, also after assigning canonical numbers.

    theorem evenEntries_incidenceVertices (f : ι ⊕ V → W) (i : ι) (steps : List (V × ι)) :
    evenEntries ((incidenceVertices i steps).map f) =
      (i :: steps.map Prod.snd).map (fun j => f (.inl j)) := by
…

    Mentions: OAI.TwoPointCorrelations.evenEntries, OAI.TwoPointCorrelations.incidenceVertices

  3. theorem OAI.TwoPointCorrelations.evenEntries_incidenceVertices_length line 33