OAI/Combinatorics/ContingencyTables/Transport/FiniteAcceptCounts.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.FiniteAcceptCounts.denominator line 16
2. def OAI.ContingencyTables.FiniteAcceptCounts.offCount line 18
3. def OAI.ContingencyTables.FiniteAcceptCounts.row line 22
4. lemma OAI.ContingencyTables.FiniteAcceptCounts.denominator_pos line 26
5. lemma OAI.ContingencyTables.FiniteAcceptCounts.offCount_mass line 30
6. lemma OAI.ContingencyTables.FiniteAcceptCounts.offCount_sum_le line 44
7. lemma OAI.ContingencyTables.FiniteAcceptCounts.row_total line 57
8. theorem OAI.ContingencyTables.FiniteAcceptCounts.row_kernel line 64

   Source documentation

   The diagonal count is recovered from the row total; all other entries use a proposal count and one binary power, independently of 2^K coins.

   theorem row_kernel (a : α) (proposal : α → β → Option α) (gap : α → α → ℕ) (K : ℕ) :
       (IntegerPropagation.kernel (fun a b => row a (proposal a) (gap a) K b)
         (denominator (β := β) K) (denominator_pos K)
   …

   Mentions: OAI.ContingencyTables.IntegerPropagation.kernel, OAI.ContingencyTables.FiniteAcceptCounts.row, OAI.ContingencyTables.FiniteAcceptCounts.denominator, OAI.ContingencyTables.FiniteAcceptCounts.denominator_pos