OAI/Combinatorics/ContingencyTables/Rooted/RootedIntegerEvaluation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Integral coefficients of the executed selected-root affine penalty

  1. def OAI.ContingencyTables.RootedIntegerEvaluation.integerIndicator line 15
  2. def OAI.ContingencyTables.RootedIntegerEvaluation.sign line 17
  3. lemma OAI.ContingencyTables.RootedIntegerEvaluation.sign_real line 22
  4. lemma OAI.ContingencyTables.RootedIntegerEvaluation.selfSign_square line 28
  5. def OAI.ContingencyTables.RootedIntegerEvaluation.coefficient line 35
  6. lemma OAI.ContingencyTables.RootedIntegerEvaluation.coefficient_real line 40
  7. def OAI.ContingencyTables.RootedIntegerEvaluation.smallContribution line 55
  8. lemma OAI.ContingencyTables.RootedIntegerEvaluation.smallContribution_real line 61
  9. def OAI.ContingencyTables.RootedIntegerEvaluation.offset line 75
  10. lemma OAI.ContingencyTables.RootedIntegerEvaluation.offset_real line 80
  11. def OAI.ContingencyTables.RootedIntegerEvaluation.rationalScaledTree line 95
  12. lemma OAI.ContingencyTables.RootedIntegerEvaluation.rationalScaledTree_cast line 102
  13. def OAI.ContingencyTables.RootedIntegerEvaluation.numerator line 111
  14. theorem OAI.ContingencyTables.RootedIntegerEvaluation.numerator_div line 117
  15. def OAI.ContingencyTables.RootedIntegerEvaluation.forestData line 138
  16. theorem OAI.ContingencyTables.RootedIntegerEvaluation.evaluate_forest line 146