OAI/Combinatorics/ContingencyTables/Machines/ScheduledCountInput.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Supplying the finite count evaluator from the public sampling parameters

  1. def OAI.ContingencyTables.ProfilePrograms.scheduledCacheParameters line 19

    Source documentation

    The same cache parameters used by the executed approximate sampler.

    def scheduledCacheParameters (z : SamplingParameters) : TransitionCacheParameters :=
…

    Mentions: OAI.ContingencyTables.ProfilePrograms.SamplingParameters, OAI.ContingencyTables.ProfilePrograms.TransitionCacheParameters

  2. def OAI.ContingencyTables.ProfilePrograms.scheduledCacheParametersRealizer line 23
  3. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_scheduledCacheParameters line 28
  4. def OAI.ContingencyTables.ProfilePrograms.scheduledDenseWidth line 35
  5. def OAI.ContingencyTables.ProfilePrograms.scheduledDenseWidthRealizer line 38
  6. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_scheduledDenseWidth line 51
  7. def OAI.ContingencyTables.ProfilePrograms.scheduledUnitWidth line 57
  8. def OAI.ContingencyTables.ProfilePrograms.scheduledUnitWidthRealizer line 59
  9. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_scheduledUnitWidth line 63
  10. def OAI.ContingencyTables.ProfilePrograms.scheduledTrialWidth line 70

    Source documentation

    The all-small branch uses only the proposal bits of each walk.

    def scheduledTrialWidth (z : SamplingParameters) : ℕ :=
…

    Mentions: OAI.ContingencyTables.ProfilePrograms.SamplingParameters

  11. def OAI.ContingencyTables.ProfilePrograms.scheduledTrialWidthRealizer line 73
  12. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_scheduledTrialWidth line 76
  13. def OAI.ContingencyTables.ProfilePrograms.scheduledCountInputMeasure line 82

    Source documentation

    Numeric loop lengths are charged explicitly, in addition to binary input size.

    def scheduledCountInputMeasure (z : SamplingParameters) : ℕ :=
…

    Mentions: OAI.ContingencyTables.ProfilePrograms.SamplingParameters

  14. lemma OAI.ContingencyTables.ProfilePrograms.weight_le_scheduledCountInputMeasure line 85
  15. def OAI.ContingencyTables.ProfilePrograms.scheduledMatrixParameters line 90
  16. def OAI.ContingencyTables.ProfilePrograms.scheduledMatrixParametersRealizer line 93
  17. lemma OAI.ContingencyTables.ProfilePrograms.work_scheduledMatrixParameters line 100
  18. def OAI.ContingencyTables.ProfilePrograms.scheduledStartIndex line 113
  19. def OAI.ContingencyTables.ProfilePrograms.scheduledStartIndexRealizer line 115
  20. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_scheduledStartIndex line 118
  21. def OAI.ContingencyTables.ProfilePrograms.scheduledWalkInput line 122
  22. def OAI.ContingencyTables.ProfilePrograms.scheduledWalkInputRealizer line 125
  23. lemma OAI.ContingencyTables.ProfilePrograms.work_scheduledWalkInput line 130
  24. def OAI.ContingencyTables.ProfilePrograms.scheduledTrialInput line 136
  25. def OAI.ContingencyTables.ProfilePrograms.scheduledTrialInputRealizer line 138
  26. lemma OAI.ContingencyTables.ProfilePrograms.work_scheduledTrialInput line 142
  27. def OAI.ContingencyTables.ProfilePrograms.scheduledTrialDenominator line 147
  28. def OAI.ContingencyTables.ProfilePrograms.scheduledTrialDenominatorRealizer line 150
  29. lemma OAI.ContingencyTables.ProfilePrograms.work_scheduledTrialDenominator line 157
  30. def OAI.ContingencyTables.ProfilePrograms.scheduledOuterInput line 167
  31. def OAI.ContingencyTables.ProfilePrograms.scheduledOuterInputRealizer line 171
  32. lemma OAI.ContingencyTables.ProfilePrograms.work_scheduledOuterInput line 180
  33. def OAI.ContingencyTables.ProfilePrograms.scheduledCounts line 196

    Source documentation

    All first-success numerators, computed from the public binary margins.

    def scheduledCounts (z : SamplingParameters) : List ℕ :=
…

    Mentions: OAI.ContingencyTables.ProfilePrograms.SamplingParameters

  34. def OAI.ContingencyTables.ProfilePrograms.scheduledCountsRealizer line 200
  35. def OAI.ContingencyTables.ProfilePrograms.scheduledCountsMeasure line 209
  36. lemma OAI.ContingencyTables.ProfilePrograms.work_scheduledCounts line 212