OAI/Combinatorics/ContingencyTables/Dense/DenseTrial.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Accepted dense trials are in bijection with the actual tables

  1. abbrev OAI.ContingencyTables.GridBoundary.DenseTrial line 16
  2. def OAI.ContingencyTables.GridBoundary.trialFree line 19
  3. def OAI.ContingencyTables.GridBoundary.TrialAccepted line 23
  4. def OAI.ContingencyTables.GridBoundary.trialTable line 26
  5. def OAI.ContingencyTables.GridBoundary.tableTrial line 31
  6. theorem OAI.ContingencyTables.GridBoundary.trialFree_tableTrial line 36
  7. theorem OAI.ContingencyTables.GridBoundary.tableTrial_accepted line 44
  8. theorem OAI.ContingencyTables.GridBoundary.trialTable_tableTrial line 54
  9. theorem OAI.ContingencyTables.GridBoundary.tableTrial_trialTable line 63
  10. def OAI.ContingencyTables.GridBoundary.acceptedTrialEquiv line 74