OAI/Combinatorics/Progressions/Sampling/WeightedUniformGridDensity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.weightedModerateGridApproximation line 13
  2. theorem OAI.Erdos3.weightedModerateGridDensity_fourier line 22
  3. theorem OAI.Erdos3.weightedModerateGridDensity_truncation line 37
  4. theorem OAI.Erdos3.weightedModerateGridDensity_eq_pointMass line 67
  5. theorem OAI.Erdos3.weightedCubeGridDensity_error_of_tail line 89
  6. theorem OAI.Erdos3.weightedModerateGridDensity_error_of_tail line 107
  7. theorem OAI.Erdos3.weightedCube_uniform_grid_density line 137
  8. theorem OAI.Erdos3.weightedModerate_uniform_grid_density line 166