OAI/Combinatorics/Progressions/Polynomial/PolynomialDensityBudget.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.natPolynomial_eval_nonneg line 9
  2. theorem OAI.Erdos3.exists_natPolynomial_eval_budget line 14
  3. theorem OAI.Erdos3.exists_majorPhaseDetectedDecomposition_budget line 52
  4. theorem OAI.Erdos3.pow_mul_exp_le_exp_of_le_budget line 90
  5. theorem OAI.Erdos3.nat_pow_mul_le_exp_of_le_budget line 104
  6. def OAI.Erdos3.VectorPolynomial.polynomialDensityBudget line 124
  7. theorem OAI.Erdos3.VectorPolynomial.polynomialDensityBudget_nonneg line 127
  8. theorem OAI.Erdos3.VectorPolynomial.polynomialDensityBudget_dominates line 132
  9. theorem OAI.Erdos3.VectorPolynomial.coefficientSampleDomain_card_le_budget line 143
  10. theorem OAI.Erdos3.VectorPolynomial.exists_polynomial_density_threshold line 152