OAI/Combinatorics/ContingencyTables/Sampling/SmallPatternProgram.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ContingencyTables.ProfilePrograms.PatternData line 11
2. abbrev OAI.ContingencyTables.ProfilePrograms.LabelledPattern line 12
3. def OAI.ContingencyTables.ProfilePrograms.pairSum line 14
4. def OAI.ContingencyTables.ProfilePrograms.pairSumRealizer line 16
5. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_pairSum line 21
6. def OAI.ContingencyTables.ProfilePrograms.indexIndicator line 31
7. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_indexIndicator line 35
8. def OAI.ContingencyTables.ProfilePrograms.patternIndices line 40
9. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_patternIndices line 43
10. def OAI.ContingencyTables.ProfilePrograms.balancedAt line 54
11. def OAI.ContingencyTables.ProfilePrograms.balancedAtRealizer line 56
12. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_balancedAt line 59
13. def OAI.ContingencyTables.ProfilePrograms.balancedTest line 63
14. def OAI.ContingencyTables.ProfilePrograms.balancedTestRealizer line 66
15. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_balancedTest line 70
16. def OAI.ContingencyTables.ProfilePrograms.defectAt line 75
17. def OAI.ContingencyTables.ProfilePrograms.defectAtRealizer line 79
18. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_defectAt line 88
19. def OAI.ContingencyTables.ProfilePrograms.defectTest line 103
20. def OAI.ContingencyTables.ProfilePrograms.defectTestRealizer line 106
21. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_defectTest line 116
22. def OAI.ContingencyTables.ProfilePrograms.patternTest line 124
23. def OAI.ContingencyTables.ProfilePrograms.patternTestRealizer line 127
24. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_patternTest line 135
25. lemma OAI.ContingencyTables.ProfilePrograms.pairSum_ofFn line 144
26. theorem OAI.ContingencyTables.ProfilePrograms.balancedTest_ofFn line 149
27. theorem OAI.ContingencyTables.ProfilePrograms.defectTest_ofFn line 159
28. theorem OAI.ContingencyTables.ProfilePrograms.patternTest_ofFn line 174
29. theorem OAI.ContingencyTables.SmallGraphProfiles.patternTest_views line 203

    Source documentation

    The binary list test recognizes exactly the manuscript's profile patterns on the common small-cell box.

    theorem patternTest_views (small : I → J → Bool) (B : I → J → ℕ)
        {n : ℕ} (e : Fin n ≃ Cells small) (z : SmallProfile small) (U : ℕ)
        (hU : ∀ a : Cells small,B a.val.1 a.val.2=U)
        (hb : ∀ a : Cells small,z (a,true)≤B a.val.1 a.val.2) :
        patternTest ((viewList small e z false,viewList small e z true),U)=true ↔
          Pattern small B z := by
    …

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.viewList, OAI.ContingencyTables.SmallGraphProfiles.Pattern