OAI/Computability/DeterministicSum/PolynomialBounds.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Individual-degree bounds and Newton polynomial conversion.

  1. def OAI.DeterministicThreeSum.Newton.univariate line 14
  2. lemma OAI.DeterministicThreeSum.Newton.univariate_degree line 17
  3. def OAI.DeterministicThreeSum.Newton.conversion line 28
  4. lemma OAI.DeterministicThreeSum.Newton.conversion_zero line 31
  5. lemma OAI.DeterministicThreeSum.Newton.univariate_factor line 35
  6. lemma OAI.DeterministicThreeSum.Newton.basis_expansion line 46
  7. def OAI.DeterministicThreeSum.Newton.exponentVector line 59
  8. lemma OAI.DeterministicThreeSum.Newton.exponentVector_apply line 61
  9. lemma OAI.DeterministicThreeSum.Newton.indicator_exponentVector line 64
  10. lemma OAI.DeterministicThreeSum.Newton.exponentVector_injective line 69
  11. lemma OAI.DeterministicThreeSum.Newton.coefficient_basis line 75
  12. lemma OAI.DeterministicThreeSum.Newton.coefficient_truncated line 84
  13. lemma OAI.DeterministicThreeSum.Newton.basis_individual_degree line 95
  14. lemma OAI.DeterministicThreeSum.Newton.truncated_individual_degree line 118