OAI/Combinatorics/ContingencyTables/Rooted/RootedCoefficientProgram.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Computing signed affine coefficients from the actual forest graph

The tree and cell endpoints are ordinary vertex indices. The program computes the canonical cut flags, tests the capacity threshold and tree adjacency, and returns the normalized signed coefficient.

  1. abbrev OAI.ContingencyTables.RootedCoefficientProgram.Input line 19
  2. def OAI.ContingencyTables.RootedCoefficientProgram.bit line 21
  3. def OAI.ContingencyTables.RootedCoefficientProgram.bitRealizer line 23
  4. lemma OAI.ContingencyTables.RootedCoefficientProgram.polynomial_bit line 24
  5. def OAI.ContingencyTables.RootedCoefficientProgram.signs line 27
  6. def OAI.ContingencyTables.RootedCoefficientProgram.signsRealizer line 30
  7. lemma OAI.ContingencyTables.RootedCoefficientProgram.polynomial_signs line 37
  8. def OAI.ContingencyTables.RootedCoefficientProgram.treeSigns line 46
  9. def OAI.ContingencyTables.RootedCoefficientProgram.treeSignsRealizer line 47
  10. lemma OAI.ContingencyTables.RootedCoefficientProgram.polynomial_treeSigns line 48
  11. def OAI.ContingencyTables.RootedCoefficientProgram.adjacent line 51
  12. def OAI.ContingencyTables.RootedCoefficientProgram.adjacentRealizer line 52
  13. lemma OAI.ContingencyTables.RootedCoefficientProgram.polynomial_adjacent line 55
  14. def OAI.ContingencyTables.RootedCoefficientProgram.freeTest line 61
  15. def OAI.ContingencyTables.RootedCoefficientProgram.freeTestRealizer line 64
  16. lemma OAI.ContingencyTables.RootedCoefficientProgram.polynomial_freeTest line 69
  17. def OAI.ContingencyTables.RootedCoefficientProgram.coefficient line 76
  18. def OAI.ContingencyTables.RootedCoefficientProgram.coefficientRealizer line 79
  19. lemma OAI.ContingencyTables.RootedCoefficientProgram.polynomial_coefficient line 86
  20. lemma OAI.ContingencyTables.RootedCoefficientProgram.adjacent_graph line 94
  21. def OAI.ContingencyTables.RootedCoefficientProgram.input line 108
  22. lemma OAI.ContingencyTables.RootedCoefficientProgram.signs_input line 115
  23. lemma OAI.ContingencyTables.RootedCoefficientProgram.treeSigns_input line 125
  24. lemma OAI.ContingencyTables.RootedCoefficientProgram.freeTest_input line 131
  25. theorem OAI.ContingencyTables.RootedCoefficientProgram.coefficient_input line 146

    Source documentation

    The output is the literal signed coefficient, with no supplied cut-membership or coefficient-correctness assumption.

    theorem coefficient_input {m n : ℕ} (A : Instance (Fin m) (Fin n))
    (t : GraphCompletionCounts.TreeCell A.T) (a : Fin m×Fin n) :
    value (coefficient (input A t a))=RootedIntegerEvaluation.coefficient A (rowColumn A.T) t a := by
…

    Mentions: OAI.ContingencyTables.GraphCompletionCounts.TreeCell, OAI.ContingencyTables.RootedCoefficientProgram.coefficient, OAI.ContingencyTables.RootedCoefficientProgram.input, OAI.ContingencyTables.RootedIntegerEvaluation.coefficient