ForestAssignmentSplit.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Splitting actual large-cell assignments into tree and free choices

The coordinate enumeration used for signatures and the graph completion sum use exactly the same assignments. This finite equivalence records that fact, including the larger signed tree intervals.

def OAI.ContingencyTables.ForestAssignmentSplit.FreeCell line 21
def OAI.ContingencyTables.ForestAssignmentSplit.FreeIndex line 24
def OAI.ContingencyTables.ForestAssignmentSplit.freeTable line 27
lemma OAI.ContingencyTables.ForestAssignmentSplit.freeTable_bound line 31

def OAI.ContingencyTables.ForestAssignmentSplit.assignmentSplit line 43

Source documentation

The large-cell product is the tree-interval product times the original free-cell product, each with multiplicity one.

noncomputable def assignmentSplit (small : I → J → Bool) (T : SimpleGraph (I⊕J))
    (hTG : T≤cellGraph small) (d : ℕ) (b : I → J → ℕ) :
    ((a : LargeCell (fun a : I×J => small a.1 a.2)) →
      Fin (width T d b a.val.1 a.val.2+1)) ≃ TreeIndex T d b×FreeIndex small T b where
…

Mentions: OAI.ContingencyTables.ForestAssignmentSplit.FreeIndex

lemma OAI.ContingencyTables.ForestAssignmentSplit.split_cellCount line 73
Source documentation
A tree/free split assignment gives precisely the cell counts in the literal graph profile, before taking the complementary column view.
```
lemma split_cellCount (small : I → J → Bool) (T : SimpleGraph (I⊕J))
    (hTG : T≤cellGraph small) (d : ℕ) (b : I → J → ℕ)
    (a : TreeIndex T d b×FreeIndex small T b)
    (l : LargeCell (fun a : I×J => small a.1 a.2)) :
    (((assignmentSplit small T hTG d b).symm a l).val)=
      cellCount T d b (freeTable small T b a.2) a.1 l.val.1 l.val.2 := by
…
```
Mentions: OAI.ContingencyTables.ForestAssignmentSplit.FreeIndex, OAI.ContingencyTables.ForestAssignmentSplit.assignmentSplit, OAI.ContingencyTables.ForestAssignmentSplit.freeTable