OAI/Combinatorics/Progressions/Sampling/AllocatedFullGridChartModelMeasurable.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedProductFullGridPrefactor line 42
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedProductFullGridPrefactor_zero line 46
  3. def OAI.Erdos3.VectorPolynomial.allocatedProductFullGridProfile line 60
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedProductFullGridProfile_mixed line 64
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedProductFullGridProfile_zero line 76
  6. def OAI.Erdos3.VectorPolynomial.allocatedFullGridChartModel line 124
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridChartModel_mixed line 129
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridChartModel_norm_le line 137
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedProductFullGridProfile_eq_model line 157
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedProductFullGridProfile_prefactor_error line 169
  11. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_product_full_grid_cover line 229
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridChartModel_measurable line 331