OAI/Combinatorics/ContingencyTables/Counting/CountingOracleScheduleProgram.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Binary arithmetic for the counting oracle sample schedule

  1. abbrev OAI.ContingencyTables.CountingOracleScheduleProgram.Fraction line 13
  2. def OAI.ContingencyTables.CountingOracleScheduleProgram.ceiling line 15
  3. def OAI.ContingencyTables.CountingOracleScheduleProgram.ceilingRealizer line 16
  4. lemma OAI.ContingencyTables.CountingOracleScheduleProgram.polynomial_ceiling line 17
  5. lemma OAI.ContingencyTables.CountingOracleScheduleProgram.ceiling_val line 19
  6. def OAI.ContingencyTables.CountingOracleScheduleProgram.natural line 25
  7. def OAI.ContingencyTables.CountingOracleScheduleProgram.naturalRealizer line 26
  8. lemma OAI.ContingencyTables.CountingOracleScheduleProgram.polynomial_natural line 27
  9. lemma OAI.ContingencyTables.CountingOracleScheduleProgram.natural_val line 29
  10. abbrev OAI.ContingencyTables.CountingOracleScheduleProgram.SampleInput line 33

    Source documentation

    Phase index, relative tolerance, and failure allowance.

    abbrev SampleInput := ℕ×(Fraction×Fraction)

    Mentions: OAI.ContingencyTables.CountingOracleScheduleProgram.Fraction

  11. def OAI.ContingencyTables.CountingOracleScheduleProgram.sampleBase line 34
  12. def OAI.ContingencyTables.CountingOracleScheduleProgram.sampleBaseRealizer line 35
  13. lemma OAI.ContingencyTables.CountingOracleScheduleProgram.polynomial_sampleBase line 40
  14. def OAI.ContingencyTables.CountingOracleScheduleProgram.sampleDenominator line 44
  15. def OAI.ContingencyTables.CountingOracleScheduleProgram.sampleDenominatorRealizer line 46
  16. lemma OAI.ContingencyTables.CountingOracleScheduleProgram.polynomial_sampleDenominator line 53
  17. def OAI.ContingencyTables.CountingOracleScheduleProgram.sampleRatio line 59
  18. def OAI.ContingencyTables.CountingOracleScheduleProgram.sampleRatioRealizer line 60
  19. lemma OAI.ContingencyTables.CountingOracleScheduleProgram.polynomial_sampleRatio line 63
  20. def OAI.ContingencyTables.CountingOracleScheduleProgram.sampleCount line 67
  21. def OAI.ContingencyTables.CountingOracleScheduleProgram.sampleCountRealizer line 68
  22. lemma OAI.ContingencyTables.CountingOracleScheduleProgram.polynomial_sampleCount line 70
  23. lemma OAI.ContingencyTables.CountingOracleScheduleProgram.sampleCount_val line 73
  24. abbrev OAI.ContingencyTables.CountingOracleScheduleProgram.OffsetInput line 84

    Source documentation

    Ambient dimension and requested relative accuracy.

    abbrev OffsetInput := ℕ×Fraction

    Mentions: OAI.ContingencyTables.CountingOracleScheduleProgram.Fraction

  25. def OAI.ContingencyTables.CountingOracleScheduleProgram.offsetBase line 85
  26. def OAI.ContingencyTables.CountingOracleScheduleProgram.offsetBaseRealizer line 86
  27. lemma OAI.ContingencyTables.CountingOracleScheduleProgram.polynomial_offsetBase line 90
  28. def OAI.ContingencyTables.CountingOracleScheduleProgram.offsetRatio line 94
  29. def OAI.ContingencyTables.CountingOracleScheduleProgram.offsetRatioRealizer line 95
  30. lemma OAI.ContingencyTables.CountingOracleScheduleProgram.polynomial_offsetRatio line 98
  31. def OAI.ContingencyTables.CountingOracleScheduleProgram.offsetAccuracy line 101
  32. def OAI.ContingencyTables.CountingOracleScheduleProgram.offsetAccuracyRealizer line 102
  33. lemma OAI.ContingencyTables.CountingOracleScheduleProgram.polynomial_offsetAccuracy line 104
  34. lemma OAI.ContingencyTables.CountingOracleScheduleProgram.offsetAccuracy_val line 107
  35. abbrev OAI.ContingencyTables.CountingOracleScheduleProgram.TimeInput line 115

    Source documentation

    The natural mixing factor and the natural height-plus-grid allowance, followed by the rational per-call accuracy.

    abbrev TimeInput := (ℕ×ℕ)×Fraction

    Mentions: OAI.ContingencyTables.CountingOracleScheduleProgram.Fraction

  36. def OAI.ContingencyTables.CountingOracleScheduleProgram.timeBase line 117
  37. def OAI.ContingencyTables.CountingOracleScheduleProgram.timeBaseRealizer line 118
  38. lemma OAI.ContingencyTables.CountingOracleScheduleProgram.polynomial_timeBase line 121
  39. def OAI.ContingencyTables.CountingOracleScheduleProgram.timeNumerator line 124
  40. def OAI.ContingencyTables.CountingOracleScheduleProgram.timeNumeratorRealizer line 125
  41. lemma OAI.ContingencyTables.CountingOracleScheduleProgram.polynomial_timeNumerator line 129
  42. def OAI.ContingencyTables.CountingOracleScheduleProgram.timeExtra line 133
  43. def OAI.ContingencyTables.CountingOracleScheduleProgram.timeExtraRealizer line 134
  44. lemma OAI.ContingencyTables.CountingOracleScheduleProgram.polynomial_timeExtra line 137
  45. def OAI.ContingencyTables.CountingOracleScheduleProgram.timeTotal line 140
  46. def OAI.ContingencyTables.CountingOracleScheduleProgram.timeTotalRealizer line 141
  47. lemma OAI.ContingencyTables.CountingOracleScheduleProgram.polynomial_timeTotal line 144
  48. def OAI.ContingencyTables.CountingOracleScheduleProgram.oracleTime line 147
  49. def OAI.ContingencyTables.CountingOracleScheduleProgram.oracleTimeRealizer line 148
  50. lemma OAI.ContingencyTables.CountingOracleScheduleProgram.polynomial_oracleTime line 150
  51. lemma OAI.ContingencyTables.CountingOracleScheduleProgram.oracleTime_val line 153
  52. lemma OAI.ContingencyTables.CountingOracleScheduleProgram.oracleTime_instance line 163