OAI/Combinatorics/Progressions/Lattices/WeightedSliceIntegerImage.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.integerGridApproximation line 14
  2. theorem OAI.Erdos3.affine_weightedCube_grid_density line 19
  3. theorem OAI.Erdos3.affine_weightedModerate_grid_density line 49
  4. def OAI.Erdos3.affineCubePlateauApproximation line 102
  5. theorem OAI.Erdos3.affineCubePlateauApproximation_split line 107
  6. theorem OAI.Erdos3.affineCubePlateauMixture_expansion line 124
  7. theorem OAI.Erdos3.affine_weightedCube_fundamental_approximation line 159
  8. theorem OAI.Erdos3.affine_weightedModerate_fundamental_approximation line 195
  9. def OAI.Erdos3.integerRetainedCoefficient line 248
  10. theorem OAI.Erdos3.integerRetainedCoefficient_norm line 253
  11. theorem OAI.Erdos3.integerGridApproximation_eq_sum line 260
  12. theorem OAI.Erdos3.integerRetainedCoefficient_mass line 267
  13. theorem OAI.Erdos3.integerRetainedCoefficient_mass_le line 277
  14. theorem OAI.Erdos3.integerGridApproximation_norm_le line 288
  15. def OAI.Erdos3.progressionCubeSources line 309
  16. def OAI.Erdos3.progressionCubeBlockWeights line 316
  17. def OAI.Erdos3.progressionCubeIntegerSum line 323
  18. theorem OAI.Erdos3.progressionCubeIntegerSum_mass line 329
  19. theorem OAI.Erdos3.progressionCubeIntegerSum_coefficient line 341
  20. theorem OAI.Erdos3.progressionCubeIntegerSum_approximation line 354
  21. def OAI.Erdos3.weightedSliceIntegerSource line 377
  22. def OAI.Erdos3.weightedSliceIntegerSum line 382
  23. theorem OAI.Erdos3.weightedSliceIntegerSum_complexMean line 387
  24. theorem OAI.Erdos3.weightedSliceIntegerSum_mass line 399
  25. theorem OAI.Erdos3.weightedSliceIntegerSum_coefficient line 407
  26. theorem OAI.Erdos3.weightedSliceIntegerSum_approximation line 415
  27. def OAI.Erdos3.moderateSliceIntegerSource line 424
  28. def OAI.Erdos3.moderateSliceIntegerSum line 429
  29. theorem OAI.Erdos3.moderateSliceIntegerSum_complexMean line 436
  30. theorem OAI.Erdos3.moderateSliceIntegerSum_mass line 449
  31. theorem OAI.Erdos3.moderateSliceIntegerSum_coefficient line 457
  32. theorem OAI.Erdos3.moderateSliceIntegerSum_approximation line 467