OAI/Combinatorics/SumProduct/Alignment/RationalLattice19.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RationalLattice.FiniteProducts.Index line 29
  2. def OAI.RationalLattice.FiniteProducts.weight line 30
  3. def OAI.RationalLattice.FiniteProducts.logCoordinates line 32
  4. lemma OAI.RationalLattice.FiniteProducts.logCoordinates_one line 42
  5. lemma OAI.RationalLattice.FiniteProducts.law_polynomial line 47
  6. lemma OAI.RationalLattice.FiniteProducts.law_weighted line 60
  7. def OAI.RationalLattice.FiniteProducts.chart line 72
  8. def OAI.RationalLattice.FiniteProducts.orderedWeight line 75
  9. lemma OAI.RationalLattice.FiniteProducts.orderedWeight_positive line 78
  10. lemma OAI.RationalLattice.FiniteProducts.orderedWeight_monotone line 79
  11. def OAI.RationalLattice.FiniteProducts.level line 81
  12. def OAI.RationalLattice.FiniteProducts.filtration line 86
  13. lemma OAI.RationalLattice.FiniteProducts.chart_adapted line 93
  14. lemma OAI.RationalLattice.FiniteProducts.chart_projection_polynomial line 109
  15. lemma OAI.RationalLattice.FiniteProducts.projection_rational line 116
  16. def OAI.RationalLattice.PolynomialArrays.constantElement line 142
  17. def OAI.RationalLattice.PolynomialArrays.sourceElement line 143
  18. def OAI.RationalLattice.PolynomialArrays.sourceOrbit line 146
  19. lemma OAI.RationalLattice.PolynomialArrays.sourceOrbit_apply line 150
  20. lemma OAI.WeightedPolynomial.IsWeighted.scale line 176
  21. lemma OAI.RationalLattice.canonicalLog_natpow line 197
  22. lemma OAI.RationalLattice.power_translate_log_weighted line 206
  23. lemma OAI.RationalLattice.PolynomialArrays.coefficients_natpow line 229
  24. lemma OAI.RationalLattice.PolynomialArrays.chart_natpow line 238
  25. lemma OAI.RationalLattice.PolynomialArrays.chart_canonicalLog line 245
  26. lemma OAI.RationalLattice.PolynomialArrays.source_joint_log_weighted line 259