OAI/Combinatorics/ContingencyTables/Rooted/RootedComponentCode.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Computing every root label before summing its signed demand

The input contains an adjacency list and one positive/negative demand pair per vertex. The polynomial program computes the root labels itself.

  1. abbrev OAI.ContingencyTables.RootedComponentCode.Input line 18
  2. def OAI.ContingencyTables.RootedComponentCode.entry line 20
  3. def OAI.ContingencyTables.RootedComponentCode.entryRealizer line 23
  4. lemma OAI.ContingencyTables.RootedComponentCode.polynomial_entry line 27
  5. def OAI.ContingencyTables.RootedComponentCode.labels line 36
  6. def OAI.ContingencyTables.RootedComponentCode.indicesRealizer line 39
  7. lemma OAI.ContingencyTables.RootedComponentCode.polynomial_indices line 42
  8. def OAI.ContingencyTables.RootedComponentCode.labelsRealizer line 48
  9. lemma OAI.ContingencyTables.RootedComponentCode.polynomial_labels line 51
  10. def OAI.ContingencyTables.RootedComponentCode.count line 55
  11. def OAI.ContingencyTables.RootedComponentCode.countRealizer line 56
  12. theorem OAI.ContingencyTables.RootedComponentCode.polynomial_count line 58
  13. lemma OAI.ContingencyTables.RootedComponentCode.labels_graph line 61
  14. theorem OAI.ContingencyTables.RootedComponentCode.count_graph line 74
  15. theorem OAI.ContingencyTables.RootedComponentCode.count_instance line 84

    Source documentation

    The binary root computation produces the actual penalty metadata for the canonical row-then-column root convention.

    theorem count_instance {m n : ℕ} (A : Instance (Fin m) (Fin n)) (z : View A → ℕ) :
    count (FiniteGraphRootProgram.graphCode (A.T.comap finSumFinEquiv.symm),
      List.ofFn (fun i : Fin (m+n) =>
        (positiveDemand A z (finSumFinEquiv.symm i),
          negativeDemand A z (finSumFinEquiv.symm i))))=
      RootedPenaltyProgram.rootCount A (rowColumn A.T)
        (ForestScaledPenalty.rowCounts A z) (ForestScaledPenalty.columnCounts A z) := by
…

    Mentions: OAI.ContingencyTables.RootedComponentCode.count, OAI.ContingencyTables.FiniteGraphRootProgram.graphCode, OAI.ContingencyTables.RootedPenaltyProgram.rootCount, OAI.ContingencyTables.ForestScaledPenalty.rowCounts, OAI.ContingencyTables.ForestScaledPenalty.columnCounts