OAI/Combinatorics/Progressions/Lattices/AllocatedNormalizedProductResidueCover.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedClippedFullGridCoverCoefficientMass line 42
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedClippedFullGridCoverCoefficientMass_le line 48
  3. def OAI.Erdos3.VectorPolynomial.allocatedClippedFullGridCoverValue line 59
  4. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_clipped_full_grid_residue_cover line 77
  5. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_normalized_full_grid_residue_cover line 161
  6. def OAI.Erdos3.VectorPolynomial.allocatedProductFullGridResidueProfile line 261
  7. def OAI.Erdos3.VectorPolynomial.allocatedProductFullGridWeightedError line 264
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedProductFullGridWeightedError_eq line 278
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedProductFullGridWeightedError_norm line 299
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedProductFullGridWeightedError_sampled line 319
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedProductFullGridWeightedError_test line 332
  12. def OAI.Erdos3.VectorPolynomial.allocatedProductFullGridCoverValue line 395
  13. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_product_full_grid_residue_cover line 413
  14. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_normalized_product_full_grid_residue_cover line 497