OAI/Combinatorics/SumProduct/Alignment/PolynomialLine01.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SquareInduction.degree_general_leibman_binomial line 44
  2. abbrev OAI.IntegerGridInterpolation.Grid line 123
  3. def OAI.IntegerGridInterpolation.weight line 125
  4. theorem OAI.IntegerGridInterpolation.one_dimensional line 128
  5. def OAI.IntegerGridInterpolation.tensorWeight line 147
  6. theorem OAI.IntegerGridInterpolation.tensor_orthogonality line 149
  7. theorem OAI.IntegerGridInterpolation.reconstruction line 162
  8. theorem OAI.IntegerGridInterpolation.clear_denominators line 174
  9. theorem OAI.IntegerGridInterpolation.exists_integer_weights line 191
  10. theorem OAI.IntegerGridInterpolation.real_reconstruction line 214
  11. abbrev OAI.PolynomialLineCoefficients.Grid line 237
  12. def OAI.PolynomialLineCoefficients.totalDegree line 238
  13. def OAI.PolynomialLineCoefficients.natLine line 240
  14. theorem OAI.PolynomialLineCoefficients.linear_degree line 243
  15. theorem OAI.PolynomialLineCoefficients.prod_degree line 248
  16. theorem OAI.PolynomialLineCoefficients.prod_top_coeff line 253
  17. theorem OAI.PolynomialLineCoefficients.natLine_degree line 264
  18. theorem OAI.PolynomialLineCoefficients.natLine_coeff_zero line 270
  19. theorem OAI.PolynomialLineCoefficients.natLine_top_coeff line 274
  20. theorem OAI.PolynomialLineCoefficients.coeff_times_pow_le_eval line 284
  21. theorem OAI.PolynomialLineCoefficients.totalDegree_le line 293
  22. theorem OAI.PolynomialLineCoefficients.natLine_eval_bound line 298
  23. theorem OAI.PolynomialLineCoefficients.natLine_coeff_bound line 308
  24. def OAI.PolynomialLineCoefficients.line line 328
  25. theorem OAI.PolynomialLineCoefficients.line_coeff line 331
  26. theorem OAI.PolynomialLineCoefficients.line_eval line 335
  27. theorem OAI.PolynomialLineCoefficients.line_degree line 343