OAI/Combinatorics/SumProduct/Alignment/WeightedPolynomial02.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeightedPolynomial.bounded_iff_degreeLT line 24
  2. lemma OAI.WeightedPolynomial.Bounded.mono line 29
  3. lemma OAI.WeightedPolynomial.bounded_zero line 31
  4. lemma OAI.WeightedPolynomial.bounded_C line 32
  5. lemma OAI.WeightedPolynomial.bounded_X line 34
  6. lemma OAI.WeightedPolynomial.Bounded.add line 36
  7. lemma OAI.WeightedPolynomial.Bounded.neg line 40
  8. lemma OAI.WeightedPolynomial.Bounded.sub line 42
  9. lemma OAI.WeightedPolynomial.Bounded.mul line 44
  10. lemma OAI.WeightedPolynomial.Bounded.pow line 49
  11. lemma OAI.WeightedPolynomial.bounded_sum line 54
  12. lemma OAI.WeightedPolynomial.bounded_prod line 62
  13. lemma OAI.WeightedPolynomial.Bounded.substitute line 73
  14. def OAI.WeightedPolynomial.IsWeighted line 104
  15. lemma OAI.WeightedPolynomial.IsWeighted.const line 106
  16. lemma OAI.WeightedPolynomial.IsWeighted.coordinate line 108
  17. lemma OAI.WeightedPolynomial.IsWeighted.mono line 110
  18. lemma OAI.WeightedPolynomial.IsWeighted.add line 114
  19. lemma OAI.WeightedPolynomial.IsWeighted.sub line 119
  20. lemma OAI.WeightedPolynomial.IsWeighted.comp line 124
  21. lemma OAI.RationalLattice.logCorrection_weighted line 146
  22. theorem OAI.RationalLattice.canonicalExp_weighted line 164
  23. lemma OAI.WeightedPolynomial.eval_kill_inr line 204
  24. lemma OAI.WeightedPolynomial.exists_left_of_vanishing line 217
  25. theorem OAI.WeightedPolynomial.fixed_left_spends_weight line 240