OAI/Combinatorics/ContingencyTables/Rooted/TreeMarginalEnumeration.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The physical one-cell marginal is exactly its balanced assignment fibre

  1. def OAI.ContingencyTables.TreeMarginalSignature.otherCells line 17
  2. lemma OAI.ContingencyTables.TreeMarginalSignature.one_view_reindex line 23
  3. lemma OAI.ContingencyTables.TreeMarginalSignature.eliminate_eq_view_sum line 39
  4. theorem OAI.ContingencyTables.TreeMarginalSignature.eliminate_eq_one_cell_sum line 56
  5. lemma OAI.ContingencyTables.TreeMarginalSignature.physical_one_cell_profile line 70
  6. theorem OAI.ContingencyTables.TreeMarginalSignature.exact_eq_fibre line 88

    Source documentation

    No multiplicity or factorial appears: the exact retained-cell balanced marginal is the literal full physical assignment fibre.

    theorem exact_eq_fibre (A : Instance I J) (alpha : ℝ) (t : I×J)
    (k : Fin (cellWidth A t+1)) :
    scalarExact A alpha t k.val=
      fibre (cellWidth A)
        (physicalWeight A.T A.b (ForestLiteralCount.lower A.T A.d A.b)
          (ForestLiteralCount.width A.T A.d A.b) A.r A.c alpha) t k := by
…

    Mentions: OAI.ContingencyTables.TreeMarginalSignature.cellWidth, OAI.ContingencyTables.TreeMarginalSignature.scalarExact, OAI.ContingencyTables.ForestLiteralCount.lower, OAI.ContingencyTables.ForestLiteralCount.width