OAI/Combinatorics/SumProduct/Alignment/DensePolynomial01.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DensePolynomialInterpolation.uniformBound line 17
  2. lemma OAI.DensePolynomialInterpolation.nodes_injective line 19
  3. lemma OAI.DensePolynomialInterpolation.interpolation_error line 31
  4. def OAI.DensePolynomialInterpolation.normalizedNode line 57
  5. lemma OAI.DensePolynomialInterpolation.normalizedNode_injective line 59
  6. lemma OAI.DensePolynomialInterpolation.normalizedNode_mem line 66
  7. def OAI.DensePolynomialInterpolation.coefficientConstant line 74
  8. lemma OAI.DensePolynomialInterpolation.coefficientConstant_pos line 78
  9. lemma OAI.DensePolynomialInterpolation.coefficient_bound_unit line 85
  10. lemma OAI.DensePolynomialInterpolation.coefficient_bound_span line 115
  11. theorem OAI.DensePolynomialInterpolation.dense_coefficient_bound line 136
  12. theorem OAI.DensePolynomialInterpolation.bounded_lattice_coefficients line 157
  13. def OAI.PolynomialIntegralResidual.integerPart line 220
  14. lemma OAI.PolynomialIntegralResidual.integerPart_coeff line 223
  15. lemma OAI.PolynomialIntegralResidual.integerPart_degree line 227
  16. lemma OAI.PolynomialIntegralResidual.integerPart_eval line 232
  17. lemma OAI.PolynomialIntegralResidual.eval_bound line 240
  18. theorem OAI.PolynomialIntegralResidual.residual line 268
  19. lemma OAI.PolynomialIntegralResidual.residual_near_integer line 301