OAI/NumberTheory/TwoPoint/Bounds/FiniteWalkFamily.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Restricting a finite walk family to its observed vertices preserves its code.

  1. def OAI.TwoPointCorrelations.walkFamilySupport line 14
  2. lemma OAI.TwoPointCorrelations.mem_walkFamilySupport line 17
  3. theorem OAI.TwoPointCorrelations.walkFamilySupport_card_le line 21
  4. abbrev OAI.TwoPointCorrelations.walkFamilyGraph line 26
  5. def OAI.TwoPointCorrelations.walkFamilyStart line 28
  6. def OAI.TwoPointCorrelations.walkFamilyFinish line 31
  7. def OAI.TwoPointCorrelations.restrictedFamilyWalk line 34
  8. theorem OAI.TwoPointCorrelations.restrictedFamilyWalk_reduced line 39
  9. theorem OAI.TwoPointCorrelations.finite_walk_family_realizable line 54

    Source documentation

    No finiteness hypothesis on the ambient graph is needed: the observed support alone suffices for the universal forest code.

    theorem finite_walk_family_realizable (hG : G.IsAcyclic)
    (hp : ∀ i, List.IsChain (· ≠ ·) (p i).edges)
    (hsize : (∑ i, (p i).support.length) ≤ N) (color : V → Bool) :
    ∃ t : BinaryTree (walkFamilySupport start finish p),
      (forestNodes t).Nodup ∧ (∀ v, v ∈ forestNodes t) ∧
      (fun i => (restrictedFamilyWalk start finish p i).support.map
        (fun v => @List.idxOf _ instBEqOfDecidableEq v (forestNodes t))) ∈
          Set.range (@ForestPathData.pattern N segments) := by
…

    Mentions: OAI.TwoPointCorrelations.walkFamilySupport, OAI.TwoPointCorrelations.forestNodes, OAI.TwoPointCorrelations.restrictedFamilyWalk, OAI.TwoPointCorrelations.ForestPathData.pattern