OAI/Combinatorics/ContingencyTables/Machines/RoundedPowerProgram.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Executing the rounded power used by the correction oracle

The exponent lies in [-2,2]. Clipping the computed signed floor at twice the supplied degree allowance plus one is therefore inactive on valid inputs, and keeps every binary execution polynomial even on arbitrary malformed numerator/denominator data.

  1. abbrev OAI.ContingencyTables.RoundedPowerProgram.Input line 19
  2. def OAI.ContingencyTables.RoundedPowerProgram.normalized line 21
  3. def OAI.ContingencyTables.RoundedPowerProgram.normalizedRealizer line 22
  4. lemma OAI.ContingencyTables.RoundedPowerProgram.polynomial_normalized line 24
  5. def OAI.ContingencyTables.RoundedPowerProgram.cap line 27
  6. def OAI.ContingencyTables.RoundedPowerProgram.capRealizer line 28
  7. lemma OAI.ContingencyTables.RoundedPowerProgram.polynomial_cap line 32
  8. def OAI.ContingencyTables.RoundedPowerProgram.clipped line 38
  9. def OAI.ContingencyTables.RoundedPowerProgram.clippedRealizer line 40
  10. lemma OAI.ContingencyTables.RoundedPowerProgram.polynomial_clipped line 43
  11. def OAI.ContingencyTables.RoundedPowerProgram.positiveInput line 49
  12. def OAI.ContingencyTables.RoundedPowerProgram.negativeInput line 50
  13. def OAI.ContingencyTables.RoundedPowerProgram.positiveInputRealizer line 51
  14. def OAI.ContingencyTables.RoundedPowerProgram.negativeInputRealizer line 52
  15. lemma OAI.ContingencyTables.RoundedPowerProgram.polynomial_positiveInput line 53
  16. lemma OAI.ContingencyTables.RoundedPowerProgram.polynomial_negativeInput line 55
  17. def OAI.ContingencyTables.RoundedPowerProgram.positivePower line 58
  18. def OAI.ContingencyTables.RoundedPowerProgram.negativePower line 59
  19. def OAI.ContingencyTables.RoundedPowerProgram.positivePowerRealizer line 60
  20. def OAI.ContingencyTables.RoundedPowerProgram.negativePowerRealizer line 62
  21. lemma OAI.ContingencyTables.RoundedPowerProgram.polynomial_positivePower line 65
  22. lemma OAI.ContingencyTables.RoundedPowerProgram.polynomial_negativePower line 74
  23. def OAI.ContingencyTables.RoundedPowerProgram.output line 83
  24. def OAI.ContingencyTables.RoundedPowerProgram.outputRealizer line 85
  25. theorem OAI.ContingencyTables.RoundedPowerProgram.polynomial_output line 87
  26. lemma OAI.ContingencyTables.RoundedPowerProgram.floor_bounds line 91
  27. lemma OAI.ContingencyTables.RoundedPowerProgram.clipped_eq line 102
  28. theorem OAI.ContingencyTables.RoundedPowerProgram.output_value line 115

    Source documentation

    The returned natural fraction is exactly the rational power used by the approximation, including negative rounded exponents.

    theorem output_value (p n d : ℕ) (xs : List Bool)
    (hlo: -2 ≤ ((p:ℚ)-n)/d) (hhi: ((p:ℚ)-n)/d ≤ 2) :
    TreeFraction.val (output (((p,n),d),xs))=
      (2:ℚ)^PowerOfTwoApproximation.numerator (((p:ℚ)-n)/d) xs.length := by
…

    Mentions: OAI.ContingencyTables.RoundedPowerProgram.output, OAI.ContingencyTables.PowerOfTwoApproximation.numerator

  29. theorem OAI.ContingencyTables.RoundedPowerProgram.output_denominator_pos line 128