OAI/Combinatorics/ContingencyTables/Rooted/RootedLargeMarginal.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Actual balanced large-cell marginal for the explicit root selector

The raw removal and reflected signatures are derived from the physical line/unary factors. No signature of the marginal is postulated.

  1. def OAI.ContingencyTables.RootedLargeMarginal.largeMarginal line 20
  2. theorem OAI.ContingencyTables.RootedLargeMarginal.largeMarginal_nonnegative line 28
  3. theorem OAI.ContingencyTables.RootedLargeMarginal.largeMarginal_eq_eliminate line 35
  4. lemma OAI.ContingencyTables.RootedLargeMarginal.large_width line 47
  5. theorem OAI.ContingencyTables.RootedLargeMarginal.largeMarginal_removal line 59
  6. theorem OAI.ContingencyTables.RootedLargeMarginal.largeMarginal_reflected line 81