OAI/Combinatorics/SumProduct/Alignment/RationalLattice17.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TriangularDenominators.polynomial_partial_origin_grid line 23
2. lemma OAI.TriangularDenominators.polynomial_partial_origin_grid_real line 74
3. lemma OAI.RationalPolynomialMap.power line 114
4. lemma OAI.RationalPolynomialMap.finset_prod line 119
5. lemma OAI.RationalLattice.PolynomialArrays.toLog_joint_polynomial line 137
6. lemma OAI.RationalLattice.PolynomialArrays.toLog_zero line 150
7. lemma OAI.RationalLattice.PolynomialArrays.joint_coordinates_polynomial line 158
8. lemma OAI.RationalLattice.PolynomialArrays.coefficient_grid_lattice line 165
9. lemma OAI.RationalLattice.PolynomialArrays.chart_grid_lattice line 198
10. lemma OAI.RationalLattice.PolynomialArrays.sampled_injective line 234
11. def OAI.RationalLattice.PolynomialArrays.latticeSample line 249
12. lemma OAI.RationalLattice.PolynomialArrays.latticeSample_continuous line 254
13. lemma OAI.RationalLattice.PolynomialArrays.lattice_discrete line 260