OAI/Computability/DepthThree/Language.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.ParsedInput.hashPolynomial line 16
  2. def OAI.DepthThreeLowerBound.ParsedInput.coefficientPolynomial line 20
  3. def OAI.DepthThreeLowerBound.ParsedInput.modulus line 24
  4. theorem OAI.DepthThreeLowerBound.ParsedInput.modulus_monic line 27
  5. theorem OAI.DepthThreeLowerBound.ParsedInput.modulus_degree line 30
  6. def OAI.DepthThreeLowerBound.ParsedInput.evaluationPolynomial line 34
  7. def OAI.DepthThreeLowerBound.ParsedInput.evaluationRemainder line 38
  8. theorem OAI.DepthThreeLowerBound.ParsedInput.evaluationRemainder_degree_lt line 41
  9. def OAI.DepthThreeLowerBound.ParsedInput.evaluate line 46
  10. theorem OAI.DepthThreeLowerBound.ParsedInput.evaluate_eq_true_iff line 49
  11. def OAI.DepthThreeLowerBound.language line 55
  12. theorem OAI.DepthThreeLowerBound.language_of_not_fits line 60
  13. theorem OAI.DepthThreeLowerBound.language_of_fits line 64
  14. theorem OAI.DepthThreeLowerBound.language_eq_true_iff line 68