OAI/Combinatorics/MatchingPSD/PolynomialInterpolation.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingInterpolation.Point line 9
  2. abbrev OAI.MatchingInterpolation.GridIndex line 10
  3. def OAI.MatchingInterpolation.coord line 11
  4. def OAI.MatchingInterpolation.lagrange line 12
  5. def OAI.MatchingInterpolation.tensorBasis line 14
  6. def OAI.MatchingInterpolation.gridNode line 16
  7. lemma OAI.MatchingInterpolation.power_interpolation line 18
  8. lemma OAI.MatchingInterpolation.list_product_counts line 31
  9. lemma OAI.MatchingInterpolation.monomial_interpolation line 39
  10. lemma OAI.MatchingInterpolation.lowDegree_interpolation line 51
  11. def OAI.MatchingInterpolation.linePolynomial line 67
  12. lemma OAI.MatchingInterpolation.linePolynomial_eval line 70
  13. lemma OAI.MatchingInterpolation.linePolynomial_zero line 78
  14. lemma OAI.MatchingInterpolation.linePolynomial_one line 83
  15. def OAI.MatchingInterpolation.origin line 98
  16. def OAI.MatchingInterpolation.dirA line 99
  17. def OAI.MatchingInterpolation.dirB line 100
  18. def OAI.MatchingInterpolation.dirStar line 101
  19. def OAI.MatchingInterpolation.dirP line 102
  20. def OAI.MatchingInterpolation.weightPolynomial line 103
  21. lemma OAI.MatchingInterpolation.weightPolynomial_zero line 107
  22. lemma OAI.MatchingInterpolation.weightPolynomial_one line 113
  23. lemma OAI.MatchingInterpolation.weightPolynomial_bound line 124
  24. def OAI.MatchingInterpolation.weight line 143
  25. lemma OAI.MatchingInterpolation.weights_bound line 146
  26. lemma OAI.MatchingInterpolation.lowDegree_affine_pullback line 164
  27. lemma OAI.MatchingInterpolation.weighted_interpolation line 188