OAI/Combinatorics/Progressions/Estimates/AllocatedIdealReferenceInsertion.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.norm_profile_sum_sub line 12
  2. theorem OAI.Erdos3.norm_nested_profile_reference_sub line 22
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedReferenceProfile_as_covered line 101
  4. def OAI.Erdos3.VectorPolynomial.allocatedRefinedProfileCoefficient line 182
  5. def OAI.Erdos3.VectorPolynomial.allocatedRefinedCoveredReference line 191
  6. def OAI.Erdos3.VectorPolynomial.allocatedRefinedCoveredError line 201
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedTupleReference_as_coveredReference line 209
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedCoveredReference_error line 219
  9. def OAI.Erdos3.VectorPolynomial.allocatedRefinedIdealProfile line 294
  10. def OAI.Erdos3.VectorPolynomial.allocatedRefinedIdealReference line 301
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedTupleReference_ideal_error line 306
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedTupleReference_ideal_exp_error line 321
  13. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_reference_profile_window_bound line 359
  14. def OAI.Erdos3.VectorPolynomial.allocatedRefinedComplexReference line 560
  15. def OAI.Erdos3.VectorPolynomial.allocatedRefinedComplexError line 570
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedComplexReference_real line 579
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedIdealReference_as_complex line 588
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedComplexReference_error line 597
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedComplexReference_sum line 609
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedComplexReference_pointwise_error line 636
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedComplexReference_const_mul line 740
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedIdealReference_site_error line 823
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedTupleReference_site_error line 846