OAI/Combinatorics/ContingencyTables/Dense/GridAdjacency.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Actual axis neighbours and the 2q proposal-degree bound

  1. def OAI.ContingencyTables.GridBoundary.OrientedNeighbor line 16
  2. def OAI.ContingencyTables.GridBoundary.Neighbor line 19
  3. theorem OAI.ContingencyTables.GridBoundary.neighbor_symm line 22
  4. theorem OAI.ContingencyTables.GridBoundary.neighbor_ne line 27
  5. theorem OAI.ContingencyTables.GridBoundary.oriented_target_unique line 37
  6. def OAI.ContingencyTables.GridBoundary.neighborDirection line 58
  7. theorem OAI.ContingencyTables.GridBoundary.neighborDirection_spec line 62
  8. theorem OAI.ContingencyTables.GridBoundary.neighborDirection_injective line 67
  9. theorem OAI.ContingencyTables.GridBoundary.neighbor_degree line 77
  10. theorem OAI.ContingencyTables.GridBoundary.edge_axis_unique line 84