OAI/NumberTheory/TwoPoint/Walks/ClosedWordStateMask.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual closed masked word is its finite-state coefficient times one indicator for survival of all its vertices.

  1. lemma OAI.TwoPointCorrelations.wordVertexSite_closed line 14
  2. lemma OAI.TwoPointCorrelations.closed_word_vertex_iff line 19
  3. lemma OAI.TwoPointCorrelations.closed_word_mask line 35
  4. lemma OAI.TwoPointCorrelations.closed_actual_word_state line 51