OAI/Combinatorics/ContingencyTables/Dense/DenseOffsets.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Unique bin and offset encoding of free integer entries

  1. def OAI.ContingencyTables.GridBoundary.gridCoordinateFin line 13
  2. abbrev OAI.ContingencyTables.GridBoundary.Offset line 29
  3. abbrev OAI.ContingencyTables.GridBoundary.FreeBox line 30
  4. def OAI.ContingencyTables.GridBoundary.trialBoxEquiv line 32
  5. theorem OAI.ContingencyTables.GridBoundary.trialBoxEquiv_val line 60
  6. def OAI.ContingencyTables.GridBoundary.integerWidth line 64
  7. theorem OAI.ContingencyTables.GridBoundary.integerWidth_pos line 68
  8. theorem OAI.ContingencyTables.GridBoundary.free_entry_lt_box line 74
  9. def OAI.ContingencyTables.GridBoundary.tableFreeBox line 91