OAI/Combinatorics/Progressions/Geometry/GeometricRetainedCommonCover.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.geometricSiteBudget line 10
  2. theorem OAI.Erdos3.VectorPolynomial.geometricSiteBudget_nonneg line 13
  3. theorem OAI.Erdos3.VectorPolynomial.le_geometricSiteBudget line 18
  4. theorem OAI.Erdos3.VectorPolynomial.degree_mul_le_geometricSiteBudget line 27
  5. theorem OAI.Erdos3.VectorPolynomial.boundedCoefficientExponent_card_le_geometricSiteBudget line 36
  6. theorem OAI.Erdos3.VectorPolynomial.cubeSites_card_le_geometricSiteBudget line 53
  7. def OAI.Erdos3.VectorPolynomial.exponentialSiteHeight line 58
  8. theorem OAI.Erdos3.VectorPolynomial.exponentialSiteHeight_pos line 60
  9. theorem OAI.Erdos3.VectorPolynomial.exponentialSiteHeight_le line 63
  10. theorem OAI.Erdos3.VectorPolynomial.boundedSiteMatrix_height_of_exp line 75
  11. theorem OAI.Erdos3.VectorPolynomial.exists_geometricSiteBudget_absorption line 99
  12. theorem OAI.Erdos3.VectorPolynomial.exists_geometric_positive_cover_budget line 118
  13. theorem OAI.Erdos3.BooleanCubeKernel.exists_geometric_retained_common_cover line 137