OAI/Combinatorics/Progressions/Polynomial/JointBooleanPolynomialPerturbation.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.parameterPolynomialMap_c2_bounds line 16
  2. theorem OAI.Erdos3.parameterPolynomialMap_perturbation_bounds line 44
  3. def OAI.Erdos3.scalePerturbedPolynomial line 76
  4. theorem OAI.Erdos3.scalePerturbedPolynomial_eval line 81
  5. theorem OAI.Erdos3.scalePerturbedPolynomial_mass_le line 89
  6. theorem OAI.Erdos3.scalePerturbedPolynomial_totalDegree_le line 96
  7. theorem OAI.Erdos3.scalePerturbedPolynomial_map_zero line 103
  8. def OAI.Erdos3.polynomialC2BoxBudget line 120
  9. theorem OAI.Erdos3.polynomialC2BoxBudget_nonneg line 123
  10. theorem OAI.Erdos3.polynomialC2BoxBudget_dominates line 126
  11. theorem OAI.Erdos3.parameterPolynomialMap_uniform_c2_error line 149
  12. theorem OAI.Erdos3.polynomialC2BoxBudget_le_exp line 174
  13. theorem OAI.Erdos3.polynomialC2BoxBudget_log_le line 190
  14. theorem OAI.Erdos3.centeredPolynomialC2Budget_le_exp line 203
  15. theorem OAI.Erdos3.centeredPolynomial_uniform_c2_error line 217
  16. def OAI.Erdos3.jointBooleanPolynomial line 258
  17. theorem OAI.Erdos3.jointBooleanPolynomial_eval line 264
  18. theorem OAI.Erdos3.jointBooleanPolynomial_mass_le line 270
  19. theorem OAI.Erdos3.jointBooleanPolynomial_totalDegree_le line 279
  20. def OAI.Erdos3.jointBooleanPerturbedPolynomial line 299
  21. theorem OAI.Erdos3.jointBooleanPerturbedPolynomial_eval line 305
  22. theorem OAI.Erdos3.jointBooleanPerturbedPolynomial_zero line 313
  23. theorem OAI.Erdos3.jointBooleanPerturbedPolynomial_bounds line 322
  24. theorem OAI.Erdos3.jointBooleanPerturbedPolynomial_c2_error line 343