OAI/Combinatorics/SumProduct/Alignment/RationalLattice02.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Polynomial.eq_of_eval_nat_eq line 25
  2. lemma OAI.RationalLattice.polynomial_substitute_eval line 35
  3. theorem OAI.RationalLattice.natpow_polynomial line 50
  4. def OAI.RationalLattice.powerPolynomial line 85
  5. lemma OAI.RationalLattice.powerPolynomial_nat line 86
  6. def OAI.RationalLattice.realPower line 91
  7. lemma OAI.RationalLattice.realPower_coord line 94
  8. lemma OAI.RationalLattice.realPower_nat line 98
  9. lemma OAI.RationalLattice.realPower_zero line 103
  10. lemma OAI.RationalLattice.realPower_one line 105
  11. lemma OAI.RationalLattice.realPower_continuous line 108
  12. def OAI.RationalLattice.evalPath line 117
  13. def OAI.RationalLattice.pathMul line 118
  14. lemma OAI.RationalLattice.evalPath_coord line 123
  15. lemma OAI.RationalLattice.evalPath_C line 125
  16. lemma OAI.RationalLattice.evalPath_comp line 127
  17. lemma OAI.RationalLattice.evalPath_mul line 130
  18. lemma OAI.RationalLattice.evalPath_ext_nat line 140
  19. lemma OAI.RationalLattice.realPower_add_nat line 152
  20. theorem OAI.RationalLattice.realPower_add line 169
  21. lemma OAI.RationalLattice.realPower_neg line 185
  22. abbrev OAI.RationalLattice.ParamPoly line 203
  23. def OAI.RationalLattice.parameterEval line 205
  24. lemma OAI.RationalLattice.parameterEval_X line 208
  25. lemma OAI.RationalLattice.universal_substitute_eval line 211
  26. theorem OAI.RationalLattice.universal_natpow_polynomial line 227
  27. def OAI.RationalLattice.universalPowerPolynomial line 267
  28. lemma OAI.RationalLattice.universalPowerPolynomial_nat line 268
  29. theorem OAI.RationalLattice.powerPolynomial_eq_universal line 272
  30. lemma OAI.RationalLattice.realPower_coord_universal line 278