OAI/Combinatorics/ContingencyTables/Sampling/AllSamplingProgram.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

A single computed sampler for large and all-small rectangles

  1. def OAI.ContingencyTables.ProfilePrograms.parameterUnitWords line 11
  2. def OAI.ContingencyTables.ProfilePrograms.parameterUnitWordsRealizer line 13
  3. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_parameterUnitWords line 20
  4. abbrev OAI.ContingencyTables.ProfilePrograms.SamplingWordInput line 27
  5. def OAI.ContingencyTables.ProfilePrograms.unitSamplingBits line 29
  6. def OAI.ContingencyTables.ProfilePrograms.unitSamplingBitsRealizer line 31
  7. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_unitSamplingBits line 39
  8. def OAI.ContingencyTables.ProfilePrograms.unitSamplingInput line 43
  9. def OAI.ContingencyTables.ProfilePrograms.unitSamplingInputRealizer line 45
  10. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_unitSamplingInput line 49
  11. def OAI.ContingencyTables.ProfilePrograms.unitSamplingMatrix line 53
  12. def OAI.ContingencyTables.ProfilePrograms.unitSamplingMatrixRealizer line 54
  13. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_unitSamplingMatrix line 58
  14. def OAI.ContingencyTables.ProfilePrograms.parameterLargeIndices line 61
  15. def OAI.ContingencyTables.ProfilePrograms.parameterLargeIndicesRealizer line 63
  16. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_parameterLargeIndices line 76
  17. def OAI.ContingencyTables.ProfilePrograms.hasLargeRectangle line 85
  18. def OAI.ContingencyTables.ProfilePrograms.hasLargeRectangleRealizer line 87
  19. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_hasLargeRectangle line 101
  20. def OAI.ContingencyTables.ProfilePrograms.samplingMatrixAll line 109
  21. def OAI.ContingencyTables.ProfilePrograms.samplingMatrixAllRealizer line 111
  22. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_samplingMatrixAll line 115
  23. def OAI.ContingencyTables.ProfilePrograms.publicSamplingAll line 119
  24. def OAI.ContingencyTables.ProfilePrograms.publicSamplingAllRealizer line 121
  25. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_publicSamplingAll line 129