OAI/Combinatorics/Progressions/Polynomial/PolynomialDeterminantDerivativeBound.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.pderiv_prod_zero line 18
  2. theorem OAI.Erdos3.pderiv_prod_one_active line 29
  3. theorem OAI.Erdos3.pderiv_booleanCoefficient line 37
  4. abbrev OAI.Erdos3.BlockParameter line 60
  5. def OAI.Erdos3.booleanAffinePolynomial line 62
  6. def OAI.Erdos3.blockSpecialization line 66
  7. theorem OAI.Erdos3.booleanAffinePolynomial_eval line 70
  8. theorem OAI.Erdos3.blockSpecialization_abs_le_one line 76
  9. theorem OAI.Erdos3.booleanAffinePolynomial_specialization line 81
  10. theorem OAI.Erdos3.booleanAffinePolynomial_pderiv line 90
  11. theorem OAI.Erdos3.booleanAffinePolynomial_degreeOf_le line 106
  12. theorem OAI.Erdos3.mvPolynomial_prod_eval_abs_le line 128
  13. theorem OAI.Erdos3.mvPolynomial_prod_pderiv_eval_abs_le_of_bound line 137
  14. theorem OAI.Erdos3.mvPolynomial_prod_pderiv_eval_abs_le line 170
  15. theorem OAI.Erdos3.polynomial_det_pderiv_eval_abs_le line 188
  16. theorem OAI.Erdos3.polynomial_det_eval_function line 213
  17. theorem OAI.Erdos3.polynomial_det_fderiv_norm_le line 221