OAI/Combinatorics/ContingencyTables/Machines/PowerApproximationProgram.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The executed power-of-two approximation used by the weight oracle

Both stages are concrete binary programs: compute the rounded signed power, then bisect using natural cross-products and shared denominators. The two allowance lists determine the precision parameters.

  1. abbrev OAI.ContingencyTables.PowerApproximationProgram.Input line 16
  2. def OAI.ContingencyTables.PowerApproximationProgram.prepare line 18
  3. def OAI.ContingencyTables.PowerApproximationProgram.prepareRealizer line 20
  4. lemma OAI.ContingencyTables.PowerApproximationProgram.polynomial_prepare line 25
  5. def OAI.ContingencyTables.PowerApproximationProgram.output line 33
  6. def OAI.ContingencyTables.PowerApproximationProgram.outputRealizer line 34
  7. theorem OAI.ContingencyTables.PowerApproximationProgram.polynomial_output line 36
  8. theorem OAI.ContingencyTables.PowerApproximationProgram.output_value line 39
  9. theorem OAI.ContingencyTables.PowerApproximationProgram.output_approximate line 50

    Source documentation

    The encoded output agrees exactly with the rational value used by the existing finite-word correction laws.

    theorem output_approximate (p n d : ℕ) (degree depth : List Bool) (sigma : ℚ)
    (hdegree: degree.length=PowerOfTwoApproximation.rootDegree sigma)
    (hdepth: depth.length=PowerOfTwoApproximation.depth sigma)
    (hlo: -2≤((p:ℚ)-n)/d) (hhi: ((p:ℚ)-n)/d≤2) :
    TreeFraction.val (output (((p,n),d),(degree,depth)))=
      PowerOfTwoApproximation.approximate (((p:ℚ)-n)/d) sigma := by
…

    Mentions: OAI.ContingencyTables.PowerOfTwoApproximation.rootDegree, OAI.ContingencyTables.PowerOfTwoApproximation.depth, OAI.ContingencyTables.PowerApproximationProgram.output, OAI.ContingencyTables.PowerOfTwoApproximation.approximate

  10. theorem OAI.ContingencyTables.PowerApproximationProgram.output_error line 59