OAI/Combinatorics/Progressions/Estimates/AllocatedProductIdealCutoff.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.rowRestrictedSiteMatrix_real_bound line 14
  2. theorem OAI.Erdos3.VectorPolynomial.mixedCoveredRowsSiteValue_full_coordinate_bound line 42
  3. def OAI.Erdos3.VectorPolynomial.allocatedProductSiteCutoff line 101
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedProductSiteCutoff_norm line 105
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedProductSiteCutoff_eq_one line 113
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedProductSiteCutoff_fixes_source line 146
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedProductSiteCutoff_weighted_error line 200
  8. def OAI.Erdos3.VectorPolynomial.allocatedProductIdealSiteRadius line 245
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedProductIdealSiteRadius_one_le line 250
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedProductIdealSiteRadius_pos line 255
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedProductIdealSiteRadius_dominates line 258
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedProductSiteCutoff_fixes_physical_ideal line 284