OAI/Combinatorics/Progressions/Estimates/AllocatedFixedCommonCover.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.AllocatedRawSourceData line 30
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedRawSourceData_of_original line 125
  3. def OAI.Erdos3.VectorPolynomial.AllocatedUniformSourceContract line 172
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedRawCoverData_of_source line 191
  5. def OAI.Erdos3.VectorPolynomial.AllocatedProductUniformSourceContract line 309
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedProductRawCoverData_of_source line 328
  7. def OAI.Erdos3.VectorPolynomial.AllocatedProductSeparatedUniformSourceContract line 446
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedProductSeparatedRawData_of_source line 465
  9. theorem OAI.Erdos3.VectorPolynomial.exists_original_common_raw_cover line 607
  10. theorem OAI.Erdos3.VectorPolynomial.exists_original_common_genuine_cover line 702
  11. def OAI.Erdos3.VectorPolynomial.AllocatedCommonGenuineCoverAt line 754
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonOriginalMesh_genuine_cover line 794
  13. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_common_genuine_cover line 816
  14. def OAI.Erdos3.VectorPolynomial.AllocatedCommonRawCoverAt line 890
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonRawCoverAt_of_source line 930
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonRawCoverAt_genuine line 949
  17. def OAI.Erdos3.VectorPolynomial.AllocatedRegularizedCommonCover line 987
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedRegularizedCommonCover_of_cutoff line 1015
  19. theorem OAI.Erdos3.VectorPolynomial.exists_fixed_regularized_common_cover line 1071