OAI/Combinatorics/ContingencyTables/Dense/DenseIntegerLaw.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.GridBoundary.denseWalkCounts line 18
2. lemma OAI.ContingencyTables.GridBoundary.denseWalkCounts_law line 27
3. def OAI.ContingencyTables.GridBoundary.offsetExponent line 32
4. def OAI.ContingencyTables.GridBoundary.offsetCounts line 35
5. lemma OAI.ContingencyTables.GridBoundary.offsetCounts_law line 52
6. def OAI.ContingencyTables.GridBoundary.denseTrialCounts line 56
7. lemma OAI.ContingencyTables.GridBoundary.denseBooleanTrial_product line 64
8. theorem OAI.ContingencyTables.GridBoundary.denseTrialCounts_law line 79
9. def OAI.ContingencyTables.GridBoundary.denseDrawCounts line 88
10. theorem OAI.ContingencyTables.GridBoundary.denseDrawCounts_law line 98

    Source documentation

    Full first-success dense completion counts agree with the implemented Boolean draw. Bin states and offset tuples are the only spaces summed.

    theorem denseDrawCounts_law (R : Option I → ℕ) (P : Option J → ℕ) (d : ℕ)
        (hd : 14≤d) (hR : ∀ i,d^12≤R i) (hP : ∀ j,d^12≤P j)
        (e : I × J ≃ Fin q) (htotal : ∑ i,R i=∑ j,P j) (h : ℕ)
        (a : Grid (I := Fin q) (4*d^8)) (fallback : Table R P) :
    …

    Mentions: OAI.ContingencyTables.GridBoundary.Grid, OAI.ContingencyTables.Table