OAI/Combinatorics/ContingencyTables/Rooted/RootedAffine.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Cut coefficients for an explicitly selected forest root

The same signed cut calculation applies to the executed root selector. In particular, coefficient size and the maximum-forest capacity bound do not depend on a classical choice of cut representative.

  1. def OAI.ContingencyTables.RootedAffine.coefficient line 21
  2. lemma OAI.ContingencyTables.RootedAffine.coefficient_abs_le_one line 26
  3. lemma OAI.ContingencyTables.RootedAffine.capacity_le_of_coefficient_ne_zero line 34
  4. theorem OAI.ContingencyTables.RootedAffine.normalized_coefficient_bound line 51
  5. def OAI.ContingencyTables.RootedAffine.smallContribution line 71
  6. def OAI.ContingencyTables.RootedAffine.offset line 77
  7. def OAI.ContingencyTables.RootedAffine.affineTree line 82
  8. theorem OAI.ContingencyTables.RootedAffine.affine_of_nonroot_equations line 86