OAI/Combinatorics/ContingencyTables/Counting/CompanionUniformPhaseWidth.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

A computed common padded width for every adaptive phase

All bounds are fixed arithmetic circuits. No numeric phase count controls an unbounded preprocessing loop.

  1. abbrev OAI.ContingencyTables.CompanionUniformPhaseWidth.Input line 15
  2. def OAI.ContingencyTables.CompanionUniformPhaseWidth.oracleInput line 17
  3. def OAI.ContingencyTables.CompanionUniformPhaseWidth.oracleInputRealizer line 19
  4. lemma OAI.ContingencyTables.CompanionUniformPhaseWidth.polynomial_oracleInput line 22
  5. def OAI.ContingencyTables.CompanionUniformPhaseWidth.rawFields line 27
  6. def OAI.ContingencyTables.CompanionUniformPhaseWidth.rawFieldsRealizer line 28
  7. lemma OAI.ContingencyTables.CompanionUniformPhaseWidth.polynomial_rawFields line 33
  8. def OAI.ContingencyTables.CompanionUniformPhaseWidth.precision line 38
  9. def OAI.ContingencyTables.CompanionUniformPhaseWidth.precisionRealizer line 39
  10. lemma OAI.ContingencyTables.CompanionUniformPhaseWidth.polynomial_precision line 42
  11. def OAI.ContingencyTables.CompanionUniformPhaseWidth.initialPrecision line 45
  12. def OAI.ContingencyTables.CompanionUniformPhaseWidth.initialPrecisionRealizer line 47
  13. lemma OAI.ContingencyTables.CompanionUniformPhaseWidth.polynomial_initialPrecision line 51
  14. def OAI.ContingencyTables.CompanionUniformPhaseWidth.fields line 55
  15. def OAI.ContingencyTables.CompanionUniformPhaseWidth.fieldsRealizer line 56
  16. lemma OAI.ContingencyTables.CompanionUniformPhaseWidth.polynomial_fields line 61
  17. def OAI.ContingencyTables.CompanionUniformPhaseWidth.measure line 67
  18. def OAI.ContingencyTables.CompanionUniformPhaseWidth.measureRealizer line 68
  19. lemma OAI.ContingencyTables.CompanionUniformPhaseWidth.polynomial_measure line 69
  20. def OAI.ContingencyTables.CompanionUniformPhaseWidth.x line 72
  21. def OAI.ContingencyTables.CompanionUniformPhaseWidth.innerExpression line 73
  22. def OAI.ContingencyTables.CompanionUniformPhaseWidth.timeExpression line 74
  23. def OAI.ContingencyTables.CompanionUniformPhaseWidth.sampleExpression line 75
  24. def OAI.ContingencyTables.CompanionUniformPhaseWidth.binExpression line 76
  25. def OAI.ContingencyTables.CompanionUniformPhaseWidth.estimatorExpression line 77
  26. def OAI.ContingencyTables.CompanionUniformPhaseWidth.medianExpression line 79
  27. def OAI.ContingencyTables.CompanionUniformPhaseWidth.initialExpression line 80
  28. def OAI.ContingencyTables.CompanionUniformPhaseWidth.stepExpression line 81
  29. def OAI.ContingencyTables.CompanionUniformPhaseWidth.stageExpression line 82
  30. def OAI.ContingencyTables.CompanionUniformPhaseWidth.phaseExpression line 83
  31. def OAI.ContingencyTables.CompanionUniformPhaseWidth.widthExpression line 85
  32. def OAI.ContingencyTables.CompanionUniformPhaseWidth.width line 87
  33. def OAI.ContingencyTables.CompanionUniformPhaseWidth.widthRealizer line 88
  34. theorem OAI.ContingencyTables.CompanionUniformPhaseWidth.polynomial_width line 91
  35. theorem OAI.ContingencyTables.CompanionUniformPhaseWidth.width_value line 96
  36. theorem OAI.ContingencyTables.CompanionUniformPhaseWidth.width_pos line 109