OAI/NumberTheory/TwoPoint/Walks/ColumnClosedEncoding.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Recover the column data of the actual joined matrix paths.

  1. lemma OAI.TwoPointCorrelations.ofFn_rev_eq_reverse line 13
  2. def OAI.TwoPointCorrelations.closedColumnRows line 24
  3. lemma OAI.TwoPointCorrelations.closedColumnRows_word line 29
  4. def OAI.TwoPointCorrelations.closedColumnAssignment line 41
  5. def OAI.TwoPointCorrelations.closedColumnPadding line 46
  6. def OAI.TwoPointCorrelations.closedColumnForward line 50
  7. theorem OAI.TwoPointCorrelations.closedColumn_encoding_word line 54