OAI/Combinatorics/ContingencyTables/Counting/CountingPhaseScalarProgram.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Fixed arithmetic circuits for the phase scalar controls

  1. def OAI.ContingencyTables.CountingPhaseScalarProgram.p line 14

    Source documentation

    Field order: label count, cutoff, phase count, restart time, observation count, return cap, capacity-bit allowance.

    def p : Expr := .input 0
  2. def OAI.ContingencyTables.CountingPhaseScalarProgram.w line 15
  3. def OAI.ContingencyTables.CountingPhaseScalarProgram.h line 16
  4. def OAI.ContingencyTables.CountingPhaseScalarProgram.tau line 17
  5. def OAI.ContingencyTables.CountingPhaseScalarProgram.observations line 18
  6. def OAI.ContingencyTables.CountingPhaseScalarProgram.returns line 19
  7. def OAI.ContingencyTables.CountingPhaseScalarProgram.capacityBits line 20
  8. def OAI.ContingencyTables.CountingPhaseScalarProgram.observable line 22
  9. def OAI.ContingencyTables.CountingPhaseScalarProgram.observationNumerator line 23
  10. def OAI.ContingencyTables.CountingPhaseScalarProgram.restartTime line 24
  11. def OAI.ContingencyTables.CountingPhaseScalarProgram.returnCap line 25
  12. def OAI.ContingencyTables.CountingPhaseScalarProgram.precisionBase line 26
  13. def OAI.ContingencyTables.CountingPhaseScalarProgram.initialPrecision line 27
  14. lemma OAI.ContingencyTables.CountingPhaseScalarProgram.observable_value line 29
  15. lemma OAI.ContingencyTables.CountingPhaseScalarProgram.observationNumerator_value line 33
  16. lemma OAI.ContingencyTables.CountingPhaseScalarProgram.returnCap_value line 39
  17. lemma OAI.ContingencyTables.CountingPhaseScalarProgram.precisionBase_value line 43
  18. lemma OAI.ContingencyTables.CountingPhaseScalarProgram.initialPrecision_value line 48
  19. lemma OAI.ContingencyTables.CountingPhaseScalarProgram.restartTime_instance line 52
  20. lemma OAI.ContingencyTables.CountingPhaseScalarProgram.polynomial line 61

    Source documentation

    Every circuit above has a fixed polynomial binary-time implementation.

    lemma polynomial (e : Expr) : PolynomialTime e.realizer := e.polynomial
…