OAI/Combinatorics/Progressions/Lattices/AllocatedAffineWholeProfileComparison.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineIdeal_finite_reference_l1 line 51
  2. def OAI.Erdos3.VectorPolynomial.allocatedAffineSourceReferenceError line 123
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineSourceReferenceError_small line 165
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineSourceReferenceError_small_separated line 235
  5. def OAI.Erdos3.VectorPolynomial.AllocatedAffineReferenceComparison line 324
  6. theorem OAI.Erdos3.VectorPolynomial.exists_early_allocated_affine_reference_source line 378
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineCoefficient_from_reference_l1 line 445
  8. theorem OAI.Erdos3.VectorPolynomial.exists_quantitative_early_affine_reference_source line 558
  9. def OAI.Erdos3.VectorPolynomial.AllocatedAffineCoefficientComparison line 602
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineCoefficientComparison_of_reference line 670
  11. theorem OAI.Erdos3.VectorPolynomial.exists_early_allocated_affine_coefficient_source line 694
  12. def OAI.Erdos3.VectorPolynomial.AllocatedAffineCoveredComparison line 733
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineCoveredComparison_of_coefficient line 813
  14. theorem OAI.Erdos3.VectorPolynomial.exists_early_allocated_affine_covered_source line 839
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineWholeCovered_comparison line 941
  16. theorem OAI.Erdos3.VectorPolynomial.exists_early_allocated_affine_bounded_source line 1032
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineWholeProfile_comparison line 1164