OAI/Combinatorics/ContingencyTables/Rooted/RootedRootPenalty.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The selected-root discrepancy is independent of the free entries

Every large-cell edge stays in a maximum-forest component. Its two incidences therefore cancel in the selected-root component sum.

  1. lemma OAI.ContingencyTables.RootedRootPenalty.componentSum_decidable line 21
  2. lemma OAI.ContingencyTables.RootedRootPenalty.root_eq_large line 29
  3. def OAI.ContingencyTables.RootedRootPenalty.componentTotal line 51
  4. lemma OAI.ContingencyTables.RootedRootPenalty.componentTotal_residual line 55
  5. lemma OAI.ContingencyTables.RootedRootPenalty.table_row_all line 91
  6. lemma OAI.ContingencyTables.RootedRootPenalty.table_column_all line 107
  7. def OAI.ContingencyTables.RootedRootPenalty.signedResidual line 129
  8. theorem OAI.ContingencyTables.RootedRootPenalty.signedResidual_eq_small line 135
  9. theorem OAI.ContingencyTables.RootedRootPenalty.signedResidual_independent line 171
  10. lemma OAI.ContingencyTables.RootedRootPenalty.abs_actualDeviation_solved line 177