FiniteWalkNumbering.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A single bounded numbering of all vertices observed in a finite walk family.

theorem OAI.TwoPointCorrelations.finite_walk_family_numbering line 17

Source documentation

The forest code comes with a numbering of the actual observed vertices. It is injective across the whole family, so line numbers encode equality between runs in different segments as well as within each segment.

theorem finite_walk_family_numbering
    (start finish : Fin segments → V) (p : ∀ i, G.Walk (start i) (finish i))
    (hG : G.IsAcyclic) (hp : ∀ i, List.IsChain (· ≠ ·) (p i).edges)
    (hsize : (∑ i, (p i).support.length) ≤ N) (color : V → Bool) :
    ∃ (number : V → ℕ) (code : ForestPathData.Code N segments),
      Set.InjOn number (walkFamilySupport start finish p : Set V) ∧
      (∀ v ∈ walkFamilySupport start finish p, number v < N) ∧
      ∀ i, decodeForestPaths code i = (p i).support.map number := by
…

Mentions: OAI.TwoPointCorrelations.ForestPathData.Code, OAI.TwoPointCorrelations.walkFamilySupport, OAI.TwoPointCorrelations.decodeForestPaths