OAI/Combinatorics/SumProduct/Alignment/WeightedPolynomial01.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeightedPolynomial.Bounded line 26
  2. def OAI.WeightedPolynomial.rayTable line 29
  3. lemma OAI.WeightedPolynomial.rayTable_monomial line 33
  4. lemma OAI.WeightedPolynomial.coeff_rayTable line 51
  5. def OAI.WeightedPolynomial.ray line 66
  6. def OAI.WeightedPolynomial.scale line 69
  7. lemma OAI.WeightedPolynomial.ray_C line 71
  8. lemma OAI.WeightedPolynomial.ray_X line 73
  9. lemma OAI.WeightedPolynomial.ray_mul line 75
  10. lemma OAI.WeightedPolynomial.ray_add line 77
  11. lemma OAI.WeightedPolynomial.ray_eval line 80
  12. lemma OAI.WeightedPolynomial.bounded_iff_ray line 91
  13. lemma OAI.RationalLattice.scale_path_mem line 141
  14. lemma OAI.RationalLattice.coordinate_weighted line 166
  15. theorem OAI.RationalLattice.multiplication_weighted line 180
  16. def OAI.WeightedPolynomial.coeffPolynomial line 209
  17. lemma OAI.WeightedPolynomial.coeffPolynomial_add line 212
  18. lemma OAI.WeightedPolynomial.coeffPolynomial_monomial line 218
  19. lemma OAI.WeightedPolynomial.coeff_coeffPolynomial line 222
  20. lemma OAI.WeightedPolynomial.eval_coeffPolynomial line 232
  21. lemma OAI.WeightedPolynomial.bounded_coeff_of_nat_evals line 243