OAI/Combinatorics/SumProduct/Alignment/RationalLattice11.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RationalLattice.natpow_prefix_eq line 27
  2. lemma OAI.RationalLattice.powerPolynomial_sub_of_prefix_eq line 42
  3. def OAI.RationalLattice.canonicalLog line 64
  4. lemma OAI.RationalLattice.canonicalLog_sub_of_prefix_eq line 66
  5. lemma OAI.RationalLattice.canonicalLog_polynomial line 72
  6. def OAI.RationalLattice.prefixSection line 80
  7. lemma OAI.RationalLattice.prefixSection_polynomial line 83
  8. lemma OAI.RationalLattice.logCorrection_exists line 90
  9. def OAI.RationalLattice.logCorrection line 95
  10. lemma OAI.RationalLattice.logCorrection_eval line 97
  11. lemma OAI.RationalLattice.canonicalLog_eq_forward line 102
  12. def OAI.RationalLattice.logHomeomorph line 116
  13. lemma OAI.RationalLattice.logHomeomorph_apply line 119
  14. def OAI.RationalLattice.canonicalExp line 122
  15. lemma OAI.RationalLattice.canonicalLog_exp line 124
  16. lemma OAI.RationalLattice.canonicalExp_log line 128
  17. lemma OAI.RationalLattice.canonicalExp_polynomial line 132
  18. lemma OAI.RationalLattice.canonicalLog_continuous line 140
  19. lemma OAI.RationalLattice.canonicalExp_continuous line 145
  20. lemma OAI.RationalLattice.realPower_nat_mul line 147
  21. lemma OAI.RationalLattice.powerPolynomial_realPower line 154
  22. lemma OAI.RationalLattice.canonicalLog_realPower line 160
  23. lemma OAI.RationalLattice.canonicalLog_one line 167
  24. lemma OAI.RationalLattice.canonicalExp_zero line 170
  25. lemma OAI.RationalLattice.canonicalExp_smul line 174
  26. lemma OAI.RationalLattice.canonicalLog_prefix_zero line 179
  27. lemma OAI.RationalLattice.coord_prefix_zero_of_log line 194
  28. lemma OAI.RationalLattice.canonicalLog_prefix_zero_iff line 208
  29. def OAI.RealPolynomialMap.IsPolynomial line 228
  30. lemma OAI.RealPolynomialMap.const line 230
  31. lemma OAI.RealPolynomialMap.coordinate line 231
  32. lemma OAI.RealPolynomialMap.add line 232
  33. lemma OAI.RealPolynomialMap.mul line 237
  34. lemma OAI.RealPolynomialMap.neg line 242
  35. lemma OAI.RealPolynomialMap.eval line 245
  36. lemma OAI.RealPolynomialMap.rational_eval line 251
  37. lemma OAI.RealPolynomialMap.of_rational line 255
  38. lemma OAI.RealPolynomialMap.comp line 259
  39. lemma OAI.RealPolynomialMap.polynomial_eval line 263
  40. lemma OAI.RealPolynomialMap.contDiff_eval line 274
  41. lemma OAI.RealPolynomialMap.contDiff line 281
  42. lemma OAI.RealPolynomialMap.homogeneous_eq_fderiv line 287