OAI/Combinatorics/Progressions/Sampling/AllocatedFullGridSpatialWeighted.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.allocated_full_grid_weighted_sampled_error line 39
2. def OAI.Erdos3.VectorPolynomial.allocatedClippedFullGridResidueProfile line 224
3. def OAI.Erdos3.VectorPolynomial.allocatedFullGridWeightedProfileError line 227
4. def OAI.Erdos3.VectorPolynomial.allocatedClippedFullGridWeightedError line 233
5. theorem OAI.Erdos3.VectorPolynomial.allocatedClippedFullGridWeightedError_eq line 245
6. theorem OAI.Erdos3.VectorPolynomial.allocatedClippedFullGridWeightedError_norm line 257
7. theorem OAI.Erdos3.VectorPolynomial.allocatedClippedFullGridWeightedError_sampled line 278
8. theorem OAI.Erdos3.VectorPolynomial.allocatedClippedFullGridWeightedError_test line 291
9. theorem OAI.Erdos3.VectorPolynomial.allocated_full_grid_spatial_weighted_error line 349