OAI/Combinatorics/Progressions/Estimates/WeightedRetainedCoefficients.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.weightedCube_uniform_absolute_cap line 11
  2. theorem OAI.Erdos3.weightedModerate_uniform_absolute_cap line 31
  3. theorem OAI.Erdos3.weightedCube_grid_density_bound line 56
  4. theorem OAI.Erdos3.weightedModerate_grid_density_bound line 70
  5. def OAI.Erdos3.weightedCubeRetainedCoefficient line 94
  6. theorem OAI.Erdos3.weightedCubeGridApproximation_eq_sum line 99
  7. theorem OAI.Erdos3.weightedCubeRetainedCoefficient_norm line 110
  8. theorem OAI.Erdos3.weightedCubeRetainedCoefficient_mass line 118
  9. def OAI.Erdos3.weightedModerateRetainedCoefficient line 127
  10. theorem OAI.Erdos3.weightedModerateGridApproximation_eq_sum line 133
  11. theorem OAI.Erdos3.weightedModerateRetainedCoefficient_norm line 145
  12. theorem OAI.Erdos3.weightedModerateRetainedCoefficient_mass line 153