OAI/Combinatorics/ContingencyTables/Transport/NetworkVertexCode.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Explicit source/row/column/sink indices for the executed network

  1. def OAI.ContingencyTables.NetworkVertexCode.index line 15

    Source documentation

    Source and sink occupy zero and one, then rows and columns.

    def index : Vertex m nā†’ā„•
  | .inl false => 0
  | .inl true => 1
  | .inr (.inl i) => 2+i.val
  | .inr (.inr j) => 2+m+j.val
  2. def OAI.ContingencyTables.NetworkVertexCode.tag line 21
  3. def OAI.ContingencyTables.NetworkVertexCode.kind line 27
  4. lemma OAI.ContingencyTables.NetworkVertexCode.kind_index line 30
  5. lemma OAI.ContingencyTables.NetworkVertexCode.index_vertices line 42
  6. abbrev OAI.ContingencyTables.NetworkVertexCode.Input line 51
  7. def OAI.ContingencyTables.NetworkVertexCode.entry line 53
  8. def OAI.ContingencyTables.NetworkVertexCode.data line 61
  9. lemma OAI.ContingencyTables.NetworkVertexCode.entry_code line 64
  10. def OAI.ContingencyTables.NetworkVertexCode.vertexCount line 76
  11. def OAI.ContingencyTables.NetworkVertexCode.matrix line 78
  12. lemma OAI.ContingencyTables.NetworkVertexCode.matrix_code line 82