OAI/Combinatorics/Progressions/Sampling/AllocatedUniformGeometricSampling.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedGeometricSamplingInput line 9
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedGeometricSamplingInput_controls line 16
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedGeometricSamplingInput_dimension line 39
  4. theorem OAI.Erdos3.VectorPolynomial.map_allocatedGeometrySourceInput line 49
  5. theorem OAI.Erdos3.VectorPolynomial.map_allocatedSiteErrorFourierOutput line 63
  6. theorem OAI.Erdos3.VectorPolynomial.map_allocatedGeometricSamplingInput line 70
  7. def OAI.Erdos3.VectorPolynomial.allocatedGeometricSamplingThreshold line 78
  8. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedGeometricSamplingThreshold_bound line 82
  9. def OAI.Erdos3.VectorPolynomial.AllocatedGeometricCoverAt line 162
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedGeometricCoverAt_of_sampling line 242
  11. theorem OAI.Erdos3.VectorPolynomial.exists_uniform_geometric_cover line 273