OAI/Combinatorics/ContingencyTables/Counting/CompanionInitialization.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact initial normalizer for the literal companion completion count

  1. def OAI.ContingencyTables.CompanionInitialization.freeTotal line 15
  2. theorem OAI.ContingencyTables.CompanionInitialization.h_zero line 19
  3. theorem OAI.ContingencyTables.CompanionInitialization.denominator_eq line 22
  4. theorem OAI.ContingencyTables.CompanionInitialization.total_zero line 30

    Source documentation

    C(0) is derived for the actual source f, using the finite paired-transversal enumeration and the literal free-completion count.

    theorem total_zero (A : Instance I J) :
    slotTotal pairs (f A 0) ∅=freeTotal A*∏ s : SmallCell A, ((A.b s.val.1 s.val.2:ℝ)+1) := by
…

    Mentions: OAI.ContingencyTables.CompanionInitialization.freeTotal