OAI/Combinatorics/ContingencyTables/Rooted/RootedPenaltyProgram.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact binary penalty evaluation for the selected-root forest

The signed affine and fraction programs compute the root-specific geometric penalty from its explicit input metadata.

  1. def OAI.ContingencyTables.RootedPenaltyProgram.rootCount line 20
  2. lemma OAI.ContingencyTables.RootedPenaltyProgram.rootCount_cast line 25
  3. def OAI.ContingencyTables.RootedPenaltyProgram.rationalPenalty line 35
  4. theorem OAI.ContingencyTables.RootedPenaltyProgram.rationalPenalty_cast line 41
  5. def OAI.ContingencyTables.RootedPenaltyProgram.data line 50
  6. theorem OAI.ContingencyTables.RootedPenaltyProgram.penaltyCode_data line 57
  7. theorem OAI.ContingencyTables.RootedPenaltyProgram.exponentCode_data line 74