OAI/Combinatorics/ContingencyTables/Dense/DenseDrawTabulation.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.DensePrograms.rawDrawParameters line 13
2. def OAI.ContingencyTables.DensePrograms.rawDrawParametersRealizer line 16
3. lemma OAI.ContingencyTables.DensePrograms.polynomial_rawDrawParameters line 23
4. def OAI.ContingencyTables.DensePrograms.rawTrialBits line 30
5. def OAI.ContingencyTables.DensePrograms.rawTrialBitsRealizer line 32
6. lemma OAI.ContingencyTables.DensePrograms.polynomial_rawTrialBits line 35
7. def OAI.ContingencyTables.DensePrograms.rawRepeat line 38
8. def OAI.ContingencyTables.DensePrograms.rawRepeatRealizer line 40
9. lemma OAI.ContingencyTables.DensePrograms.polynomial_rawRepeat line 47
10. def OAI.ContingencyTables.DensePrograms.rawCountContext line 55
11. def OAI.ContingencyTables.DensePrograms.rawCountContextRealizer line 58
12. def OAI.ContingencyTables.DensePrograms.rawFallbackIndex line 63
13. def OAI.ContingencyTables.DensePrograms.rawFallbackIndexRealizer line 66
14. lemma OAI.ContingencyTables.DensePrograms.polynomial_rawFallbackIndex line 69
15. def OAI.ContingencyTables.DensePrograms.rawVectorInput line 73
16. def OAI.ContingencyTables.DensePrograms.rawVectorInputRealizer line 77
17. def OAI.ContingencyTables.DensePrograms.rawDrawCounts line 85
18. def OAI.ContingencyTables.DensePrograms.rawDrawCountsRealizer line 88
19. def OAI.ContingencyTables.DensePrograms.rawTabulationMeasure line 91
20. lemma OAI.ContingencyTables.DensePrograms.weight_le_rawMeasure line 94
21. lemma OAI.ContingencyTables.DensePrograms.polynomial_work line 98

    Distinct definitions of this name: OAI/Combinatorics/ContingencyTables/Dense/DenseWalkTabulation.lean:103 (different declaration text). Qualify references as OAI.ContingencyTables.DensePrograms.polynomial_work@path.

22. lemma OAI.ContingencyTables.DensePrograms.paired_work line 102

    Distinct definitions of this name: OAI/Combinatorics/ContingencyTables/Dense/DenseWalkTabulation.lean:107 (different declaration text). Qualify references as OAI.ContingencyTables.DensePrograms.paired_work@path.

23. lemma OAI.ContingencyTables.DensePrograms.work_rawCountContext line 109
24. lemma OAI.ContingencyTables.DensePrograms.work_rawCandidateCounts line 125
25. lemma OAI.ContingencyTables.DensePrograms.work_rawVectorInput line 137
26. theorem OAI.ContingencyTables.DensePrograms.work_rawDrawCounts line 161

    Source documentation

    Full draw-law tabulation is polynomial in the finite box and grid sizes and in the numerical precision schedules.

    theorem work_rawDrawCounts : WorkBound rawDrawCountsRealizer rawTabulationMeasure := by
    …

    Mentions: OAI.ContingencyTables.DensePrograms.rawDrawCountsRealizer, OAI.ContingencyTables.DensePrograms.rawTabulationMeasure

27. lemma OAI.ContingencyTables.DensePrograms.rawTrialBits_code line 178
28. theorem OAI.ContingencyTables.DensePrograms.rawDrawCounts_actual line 186
29. theorem OAI.ContingencyTables.DensePrograms.rawDrawCounts_at line 224

    Source documentation

    Looking up a feasible table returns its exact numerator in the implemented finite Boolean dense draw.

    theorem rawDrawCounts_at {m n d : ℕ} (R : Option (Fin m) → ℕ)
        (P : Option (Fin n) → ℕ) (hd : 14≤d) (hq : m*n≤d)
        (hR : ∀ i,d^12≤R i) (hP : ∀ j,d^12≤P j) (htotal : ∑ i,R i=∑ j,P j)
        (h : ℕ) (X : Table R P) :
        (rawDrawCounts ((marginCode R,marginCode P),(d,h))).getD
          (tableIndex ((marginCode R,marginCode P),tableOutput X)) 0=
        (denseDrawCounts R P d hd hR hP finProdFinEquiv htotal h
          (canonicalOrigin (m*n) d (by omega)) (canonicalFallback R P htotal)).count X := by
    …

    Mentions: OAI.ContingencyTables.Table, OAI.ContingencyTables.DensePrograms.rawDrawCounts, OAI.ContingencyTables.DensePrograms.marginCode, OAI.ContingencyTables.DensePrograms.tableIndex, OAI.ContingencyTables.DensePrograms.tableOutput, OAI.ContingencyTables.DensePrograms.canonicalOrigin, OAI.ContingencyTables.DensePrograms.canonicalFallback