OAI/Combinatorics/EditApproximation/Probability/FiniteBitPolynomial.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A structural polynomial bound for finite Boolean arithmetic loops. The expression language includes only operations whose magnitude is bounded by a fixed power of a common input bound.

  1. inductive OAI.EditApproximation.FiniteBitPolynomial line 11
  2. instance OAI.EditApproximation.FiniteBitPolynomial.(instance at line 23) line 23
  3. instance OAI.EditApproximation.FiniteBitPolynomial.(instance at line 24) line 24
  4. instance OAI.EditApproximation.FiniteBitPolynomial.(instance at line 25) line 25
  5. instance OAI.EditApproximation.FiniteBitPolynomial.(instance at line 26) line 26
  6. def OAI.EditApproximation.FiniteBitPolynomial.eval line 28
  7. def OAI.EditApproximation.FiniteBitPolynomial.degree line 38
  8. theorem OAI.EditApproximation.FiniteBitPolynomial.eval_le_pow line 48