OAI/Combinatorics/ContingencyTables/Rooted/RootedCountIdentification.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The selected-root physical marginal is its literal completion count

  1. def OAI.ContingencyTables.RootedCountIdentification.h line 17
  2. theorem OAI.ContingencyTables.RootedCountIdentification.h_positive line 26
  3. theorem OAI.ContingencyTables.RootedCountIdentification.h_zero line 34
  4. theorem OAI.ContingencyTables.RootedCountIdentification.physical_sum_split line 38
  5. theorem OAI.ContingencyTables.RootedCountIdentification.h_eq_largeMarginal line 59
  6. theorem OAI.ContingencyTables.RootedCountIdentification.h_removal line 84
  7. theorem OAI.ContingencyTables.RootedCountIdentification.h_reflected line 93