OAI/Combinatorics/SumProduct/Alignment/PolynomialArray01.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PolynomialArrayInterpolation.Grid line 21
  2. lemma OAI.PolynomialArrayInterpolation.bounded_totalDegree line 23
  3. lemma OAI.PolynomialArrayInterpolation.real_orthogonality line 31
  4. lemma OAI.PolynomialArrayInterpolation.reconstruction line 38
  5. def OAI.PolynomialArrayInterpolation.coefficients line 48
  6. lemma OAI.PolynomialArrayInterpolation.coefficients_eval line 51
  7. lemma OAI.PolynomialArrayInterpolation.reconstruction_function line 57
  8. lemma OAI.PolynomialArrayInterpolation.coefficients_zero_high line 69
  9. lemma OAI.PolynomialArrayInterpolation.coefficients_continuous line 85
  10. lemma OAI.PolynomialArrayInterpolation.gridEval_weighted line 91
  11. lemma OAI.PolynomialArrayInterpolation.coefficients_gridEval line 119
  12. lemma OAI.PolynomialArrayInterpolation.grid_injective line 122
  13. lemma OAI.SortedFiniteWeights.exists_ordered line 144
  14. def OAI.SortedFiniteWeights.indexing line 161
  15. lemma OAI.SortedFiniteWeights.indexing_monotone line 162
  16. abbrev OAI.RationalLattice.PolynomialArrays.Index line 185
  17. def OAI.RationalLattice.PolynomialArrays.fullCoeff line 188
  18. def OAI.RationalLattice.PolynomialArrays.toLog line 191
  19. lemma OAI.RationalLattice.PolynomialArrays.toLog_array line 195
  20. def OAI.RationalLattice.PolynomialArrays.coefficients line 203
  21. lemma OAI.RationalLattice.PolynomialArrays.fullCoeff_coefficients line 206
  22. lemma OAI.RationalLattice.PolynomialArrays.toLog_coefficients line 215
  23. lemma OAI.RationalLattice.PolynomialArrays.coefficients_toLog line 221
  24. lemma OAI.RationalLattice.PolynomialArrays.toLog_continuous line 227
  25. lemma OAI.RationalLattice.PolynomialArrays.coefficients_continuous line 238
  26. def OAI.RationalLattice.PolynomialArrays.coefficientHomeomorph line 247
  27. lemma OAI.RationalLattice.PolynomialArrays.coefficientHomeomorph_one line 268