OAI/Combinatorics/ContingencyTables/Sampling/ExactSamplingParameters.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Computing the exact sampler's precision from its margin-only input

  1. def OAI.ContingencyTables.ProfilePrograms.sixthPower line 13
  2. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_sixthPower line 17
  3. def OAI.ContingencyTables.ProfilePrograms.exactPrecision line 20
  4. def OAI.ContingencyTables.ProfilePrograms.exactPrecisionRealizer line 22
  5. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_exactPrecision line 29
  6. def OAI.ContingencyTables.ProfilePrograms.exactSamplingParameters line 36
  7. def OAI.ContingencyTables.ProfilePrograms.exactSamplingParametersRealizer line 38
  8. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_exactSamplingParameters line 42
  9. def OAI.ContingencyTables.ProfilePrograms.exactBranchDenominator line 46
  10. def OAI.ContingencyTables.ProfilePrograms.exactBranchDenominatorRealizer line 48
  11. def OAI.ContingencyTables.ProfilePrograms.exactParameterMeasure line 52
  12. lemma OAI.ContingencyTables.ProfilePrograms.work_exactBranchDenominator line 54
  13. def OAI.ContingencyTables.ProfilePrograms.exactResidualInput line 63
  14. def OAI.ContingencyTables.ProfilePrograms.exactResidualInputRealizer line 66
  15. lemma OAI.ContingencyTables.ProfilePrograms.work_exactResidualInput line 69
  16. def OAI.ContingencyTables.ProfilePrograms.exactOrdinaryBits line 75

    Source documentation

    The ordinary branch needs precisely the existing public sampler's word.

    def exactOrdinaryBits (z : CompletionMargins) : ℕ := parameterWordCount (exactSamplingParameters z)

    Mentions: OAI.ContingencyTables.ProfilePrograms.parameterWordCount, OAI.ContingencyTables.ProfilePrograms.exactSamplingParameters

  17. def OAI.ContingencyTables.ProfilePrograms.exactOrdinaryBitsRealizer line 77
  18. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_exactOrdinaryBits line 81
  19. def OAI.ContingencyTables.ProfilePrograms.exactParsedMargins line 84
  20. def OAI.ContingencyTables.ProfilePrograms.exactParsedMarginsRealizer line 86
  21. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_exactParsedMargins line 89
  22. lemma OAI.ContingencyTables.SmallGraphProfiles.exactPrecision_ofFn line 100
  23. lemma OAI.ContingencyTables.SmallGraphProfiles.exactSamplingParameters_ofFn line 104
  24. lemma OAI.ContingencyTables.SmallGraphProfiles.exactBranchDenominator_ofFn line 109
  25. lemma OAI.ContingencyTables.SmallGraphProfiles.exactResidualInput_ofFn line 113
  26. lemma OAI.ContingencyTables.SmallGraphProfiles.exactOrdinaryBits_ofFn line 118
  27. lemma OAI.ContingencyTables.SmallGraphProfiles.exactParsedMargins_spec line 122