OAI/Combinatorics/ContingencyTables/Rooted/RootedPenalty.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Physical factors with the executed component-root convention

The line factors use the explicitly selected roots. Their tree factors, widths and doubled row/column coordinates are exactly the source data.

  1. def OAI.ContingencyTables.RootedPenalty.ell line 21
  2. def OAI.ContingencyTables.RootedPenalty.widths line 22
  3. def OAI.ContingencyTables.RootedPenalty.rootFlag line 24
  4. def OAI.ContingencyTables.RootedPenalty.rootPenalty line 27
  5. def OAI.ContingencyTables.RootedPenalty.penalty line 31
  6. def OAI.ContingencyTables.RootedPenalty.physicalWeight line 35
  7. lemma OAI.ContingencyTables.RootedPenalty.line_product_eq line 41
  8. lemma OAI.ContingencyTables.RootedPenalty.unary_product_eq line 61
  9. theorem OAI.ContingencyTables.RootedPenalty.exact_eq line 79
  10. theorem OAI.ContingencyTables.RootedPenalty.physicalWeight_nonnegative line 100
  11. theorem OAI.ContingencyTables.RootedPenalty.physicalWeight_removal line 107