OAI/Combinatorics/Progressions/Estimates/AllocatedProxyAccuracy.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.coefficientErrorAccuracyLog line 11
  2. def OAI.Erdos3.VectorPolynomial.coefficientErrorAccuracy line 14
  3. theorem OAI.Erdos3.VectorPolynomial.coefficientErrorAccuracy_bounds line 17
  4. theorem OAI.Erdos3.VectorPolynomial.coefficientErrorAccuracy_loss_bound line 28
  5. theorem OAI.Erdos3.VectorPolynomial.coefficientError_normalized_exp_bound line 60
  6. def OAI.Erdos3.VectorPolynomial.allocatedCoefficientAccuracyLog line 88
  7. def OAI.Erdos3.VectorPolynomial.allocatedCoefficientAccuracy line 91
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientAccuracy_bounds line 94
  9. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCoefficientAccuracyLog_bound line 100
  10. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCoefficientAccuracy_budget line 122
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientErrorAccuracy_bound line 132
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientAccuracy_proxy_error line 212