OAI/Combinatorics/ContingencyTables/Dense/DenseWalkTabulation.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ContingencyTables.DensePrograms.TabulationData line 13
2. def OAI.ContingencyTables.DensePrograms.tabulationDimension line 15
3. def OAI.ContingencyTables.DensePrograms.tabulationSteps line 18
4. def OAI.ContingencyTables.DensePrograms.tabulationStepsRealizer line 20
5. lemma OAI.ContingencyTables.DensePrograms.polynomial_tabulationSteps line 27
6. def OAI.ContingencyTables.DensePrograms.tabulationAllowance line 37
7. def OAI.ContingencyTables.DensePrograms.tabulationAllowanceRealizer line 39
8. lemma OAI.ContingencyTables.DensePrograms.polynomial_tabulationAllowance line 44
9. def OAI.ContingencyTables.DensePrograms.tabulationDenominatorInput line 52
10. def OAI.ContingencyTables.DensePrograms.tabulationDenominatorInputRealizer line 55
11. lemma OAI.ContingencyTables.DensePrograms.polynomial_tabulationDenominatorInput line 58
12. def OAI.ContingencyTables.DensePrograms.tabulationDenominator line 62
13. def OAI.ContingencyTables.DensePrograms.tabulationDenominatorRealizer line 65
14. def OAI.ContingencyTables.DensePrograms.tabulationDimensions line 68
15. def OAI.ContingencyTables.DensePrograms.tabulationDimensionsRealizer line 71
16. lemma OAI.ContingencyTables.DensePrograms.polynomial_tabulationDimensions line 76
17. lemma OAI.ContingencyTables.DensePrograms.tabulationDimensions_length line 81
18. def OAI.ContingencyTables.DensePrograms.tabulationCountInput line 85
19. def OAI.ContingencyTables.DensePrograms.tabulationCountInputRealizer line 89
20. def OAI.ContingencyTables.DensePrograms.tabulationMeasure line 95
21. lemma OAI.ContingencyTables.DensePrograms.weight_le_measure line 99
22. lemma OAI.ContingencyTables.DensePrograms.polynomial_work line 103

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

23. lemma OAI.ContingencyTables.DensePrograms.paired_work line 107

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

24. lemma OAI.ContingencyTables.DensePrograms.work_tabulationDenominator line 113
25. lemma OAI.ContingencyTables.DensePrograms.work_tabulationCountInput line 122
26. lemma OAI.ContingencyTables.DensePrograms.tabulation_enumerationMeasure line 136
27. lemma OAI.ContingencyTables.DensePrograms.work_tabulationEnumeration line 142
28. def OAI.ContingencyTables.DensePrograms.tabulationInput line 153
29. def OAI.ContingencyTables.DensePrograms.tabulationInputRealizer line 156
30. lemma OAI.ContingencyTables.DensePrograms.work_tabulationInput line 162
31. def OAI.ContingencyTables.DensePrograms.tabulateDenseWalk line 174
32. def OAI.ContingencyTables.DensePrograms.tabulateDenseWalkRealizer line 176
33. theorem OAI.ContingencyTables.DensePrograms.work_tabulateDenseWalk line 181

    Source documentation

    Binary matrix propagation computes all walk numerators in polynomial work in the explicit state count and the scheduled number of steps.

    theorem work_tabulateDenseWalk : WorkBound tabulateDenseWalkRealizer tabulationMeasure :=
    …

    Mentions: OAI.ContingencyTables.DensePrograms.tabulateDenseWalkRealizer, OAI.ContingencyTables.DensePrograms.tabulationMeasure

34. lemma OAI.ContingencyTables.DensePrograms.tabulationDimension_code line 184
35. theorem OAI.ContingencyTables.DensePrograms.tabulateDenseWalk_actual line 191

    Source documentation

    The caller computes its grid, zero starting state and full iteration schedule from the margins. No state list or probability oracle is supplied.

    theorem tabulateDenseWalk_actual {m n d : ℕ} (R : Option (Fin m) → ℕ)
        (P : Option (Fin n) → ℕ) (hq : m*n≤d) (hd : 0<d) (h : ℕ) :
        tabulateDenseWalk ((marginCode R,marginCode P),(d,h))=
          List.ofFn (fun i => IntegerPropagation.numerators
            (denseTransitionCount R P d finProdFinEquiv)
            (canonicalOrigin (m*n) d hd) (d^50*(h+1)^2)
            (gridEnumeration (m*n) (4*d^8) i)) := by
    …

    Mentions: OAI.ContingencyTables.DensePrograms.tabulateDenseWalk, OAI.ContingencyTables.DensePrograms.marginCode, OAI.ContingencyTables.IntegerPropagation.numerators, OAI.ContingencyTables.DensePrograms.canonicalOrigin, OAI.ContingencyTables.DensePrograms.gridEnumeration