OAI/Combinatorics/ContingencyTables/Transport/FiniteGridWords.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ContingencyTables.DensePrograms.GridEnumerationData line 12
2. def OAI.ContingencyTables.DensePrograms.clippedGridPowerInput line 14
3. def OAI.ContingencyTables.DensePrograms.clippedGridPowerInputRealizer line 17
4. lemma OAI.ContingencyTables.DensePrograms.polynomial_clippedGridPowerInput line 21
5. def OAI.ContingencyTables.DensePrograms.clippedGridPower line 27
6. def OAI.ContingencyTables.DensePrograms.clippedGridPowerRealizer line 30
7. lemma OAI.ContingencyTables.DensePrograms.polynomial_clippedGridPower line 33
8. abbrev OAI.ContingencyTables.DensePrograms.GridCoordinateData line 43
9. def OAI.ContingencyTables.DensePrograms.gridCoordinate line 45
10. def OAI.ContingencyTables.DensePrograms.gridCoordinateRealizer line 48
11. lemma OAI.ContingencyTables.DensePrograms.polynomial_gridCoordinate line 54
12. def OAI.ContingencyTables.DensePrograms.gridCoordinateIndices line 64
13. def OAI.ContingencyTables.DensePrograms.gridCoordinateIndicesRealizer line 66
14. lemma OAI.ContingencyTables.DensePrograms.polynomial_gridCoordinateIndices line 69
15. def OAI.ContingencyTables.DensePrograms.gridCoordinates line 76
16. def OAI.ContingencyTables.DensePrograms.gridCoordinatesRealizer line 79
17. lemma OAI.ContingencyTables.DensePrograms.polynomial_gridCoordinates line 82
18. def OAI.ContingencyTables.DensePrograms.gridStateCount line 86
19. def OAI.ContingencyTables.DensePrograms.gridStateCountRealizer line 89
20. lemma OAI.ContingencyTables.DensePrograms.polynomial_gridStateCount line 92
21. lemma OAI.ContingencyTables.DensePrograms.gridStateCount_eq line 96
22. def OAI.ContingencyTables.DensePrograms.gridWords line 99
23. def OAI.ContingencyTables.DensePrograms.gridWordsRealizer line 102
24. theorem OAI.ContingencyTables.DensePrograms.work_gridWords line 108

    Source documentation

    State enumeration is polynomial in its output count, not in the precision or number of fair random words of the sampler.

    theorem work_gridWords : WorkBound gridWordsRealizer
        (fun z => gridStateCount z+weight z) := by
    …

    Mentions: OAI.ContingencyTables.DensePrograms.gridWordsRealizer, OAI.ContingencyTables.DensePrograms.gridStateCount

25. lemma OAI.ContingencyTables.DensePrograms.map_range_eq_ofFn line 121
26. lemma OAI.ContingencyTables.DensePrograms.gridCoordinates_eq line 125
27. def OAI.ContingencyTables.DensePrograms.gridDigitEquiv line 134
28. def OAI.ContingencyTables.DensePrograms.gridEnumeration line 150
29. lemma OAI.ContingencyTables.DensePrograms.gridEnumeration_code line 153
30. theorem OAI.ContingencyTables.DensePrograms.gridWords_eq line 161

    Source documentation

    Every box state occurs once in this explicit, mixed-radix list.

    theorem gridWords_eq (z : GridEnumerationData) :
        gridWords z=List.ofFn (fun i => gridNatCode (gridEnumeration z.1.length z.2 i)) := by
    …

    Mentions: OAI.ContingencyTables.DensePrograms.GridEnumerationData, OAI.ContingencyTables.DensePrograms.gridWords, OAI.ContingencyTables.DensePrograms.gridNatCode, OAI.ContingencyTables.DensePrograms.gridEnumeration

31. lemma OAI.ContingencyTables.DensePrograms.gridWords_eq_length line 169