OAI/NumberTheory/PowerFree/HilbertSimplex.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuarticPowerFree.extend_independent_finset line 15
  2. theorem OAI.QuarticPowerFree.hilbert_simplex_shift line 47
  3. theorem OAI.QuarticPowerFree.simplex_order_step line 89
  4. theorem OAI.QuarticPowerFree.independent_weighted_simplex line 98
  5. def OAI.QuarticPowerFree.monomialWeight line 161
  6. theorem OAI.QuarticPowerFree.monomialWeight_nonneg line 164
  7. def OAI.QuarticPowerFree.weightedExponentBound line 168
  8. def OAI.QuarticPowerFree.weightedMonomials line 171
  9. theorem OAI.QuarticPowerFree.mem_weightedMonomials line 176
  10. theorem OAI.QuarticPowerFree.weightedMonomials_mono line 192
  11. def OAI.QuarticPowerFree.weightedDegreeBound line 199
  12. theorem OAI.QuarticPowerFree.weighted_monomial_degree_bound line 202
  13. def OAI.QuarticPowerFree.weightedFunctions line 211
  14. instance OAI.QuarticPowerFree.weightedFunctions_finite line 217
  15. def OAI.QuarticPowerFree.weightedHilbert line 223
  16. theorem OAI.QuarticPowerFree.integer_monomial_abs_le line 227
  17. theorem OAI.QuarticPowerFree.select_weighted_monomials line 255
  18. theorem OAI.QuarticPowerFree.exists_simplex_margin line 289