OAI/Combinatorics/ContingencyTables/Machines/InitialLocalChoices.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.InitialLocalChoices.localWeight line 13
2. theorem OAI.ContingencyTables.InitialLocalChoices.sum_localWeight line 18

   Source documentation

   Enumerating all choices of the remaining row labels gives exactly the binomial/factorial bracket, including empty local spaces.

   theorem sum_localWeight (b u v : ℕ) :
       (∑ S : Finset (Fin (b-u-v)), localWeight b u v S)=bracket b u v := by
   …

   Mentions: OAI.ContingencyTables.InitialLocalChoices.localWeight

3. theorem OAI.ContingencyTables.InitialLocalChoices.sum_independent_choices line 27

   Source documentation

   Independent choices in the cells factor exactly; the expression is a finite combinatorial sum before evaluating its four bracket cases.

   theorem sum_independent_choices {C : Type*} [Fintype C] (b u v : C → ℕ) :
       (∑ S : ((c : C) → Finset (Fin (b c-u c-v c))),
         ∏ c, localWeight (b c) (u c) (v c) (S c))=
         ∏ c, bracket (b c) (u c) (v c) := by
   …

   Mentions: OAI.ContingencyTables.InitialLocalChoices.localWeight