OAI/Combinatorics/ContingencyTables/Rooted/RootedLiteralCount.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Multiplicity-one physical tree sum with the executed root convention

  1. def OAI.ContingencyTables.RootedLiteralCount.actualPenalty line 17
  2. def OAI.ContingencyTables.RootedLiteralCount.RootConditions line 24
  3. lemma OAI.ContingencyTables.RootedLiteralCount.penalty_profile line 31
  4. lemma OAI.ContingencyTables.RootedLiteralCount.nonroot_iff line 57
  5. def OAI.ContingencyTables.RootedLiteralCount.solutionIndex line 115
  6. lemma OAI.ContingencyTables.RootedLiteralCount.physical_solutionIndex line 132
  7. theorem OAI.ContingencyTables.RootedLiteralCount.tree_indicator_sum line 148
  8. theorem OAI.ContingencyTables.RootedLiteralCount.literal_tree_sum line 173