OAI/Combinatorics/Progressions/Lattices/WeightedCubeIntegerSupport.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.integerGridMass line 11
  2. def OAI.Erdos3.integerGridCoefficient line 15
  3. theorem OAI.Erdos3.integerGridMass_nonneg line 19
  4. theorem OAI.Erdos3.integerGridFourier_inversion line 24
  5. theorem OAI.Erdos3.independent_integerGridCoefficient line 47
  6. def OAI.Erdos3.integerGridDensity line 68
  7. theorem OAI.Erdos3.integerGridDensity_nonneg line 72
  8. theorem OAI.Erdos3.integerGridDensity_fourier line 77
  9. theorem OAI.Erdos3.integerGridDensity_truncation line 87
  10. theorem OAI.Erdos3.integerGridDensity_absolute_cap line 99
  11. theorem OAI.Erdos3.gridVolume_torus_factor line 110
  12. theorem OAI.Erdos3.integerGridResidue_eq_iff_of_close line 124
  13. theorem OAI.Erdos3.integerGridMass_eq_imageMass line 141
  14. theorem OAI.Erdos3.integerGridMass_eq_imageMass_on_box line 153
  15. theorem OAI.Erdos3.integerGridDensity_eq_imageMass_on_box line 165
  16. def OAI.Erdos3.intervalGridRepresentative line 182
  17. theorem OAI.Erdos3.intervalGridRepresentative_bounds line 185
  18. theorem OAI.Erdos3.intervalGridRepresentative_residue line 193
  19. def OAI.Erdos3.rectangularGridRepresentative line 198
  20. theorem OAI.Erdos3.rectangularGridRepresentative_bounds line 201
  21. theorem OAI.Erdos3.rectangularGridRepresentative_residue line 207
  22. theorem OAI.Erdos3.rectangularGridRepresentative_eq line 213
  23. theorem OAI.Erdos3.integerGridMass_representative line 225
  24. def OAI.Erdos3.integerBooleanBlockValue line 242
  25. def OAI.Erdos3.integerBooleanBlockJet line 246
  26. theorem OAI.Erdos3.integerBooleanBlockValue_cast line 250
  27. theorem OAI.Erdos3.integerBooleanBlockJet_cast line 260
  28. theorem OAI.Erdos3.gridJetFrequency_pairing line 269
  29. theorem OAI.Erdos3.integerBooleanBlockJet_pairing line 282
  30. theorem OAI.Erdos3.integerBooleanBlockValue_bound line 298
  31. theorem OAI.Erdos3.integerBooleanBlockJet_bound line 320
  32. theorem OAI.Erdos3.integerScalarCubeBox_coordinate_abs line 337
  33. def OAI.Erdos3.weightedCubeIntegerSource line 353
  34. def OAI.Erdos3.weightedCubeIntegerJetSum line 359
  35. theorem OAI.Erdos3.weightedCubeGridCoefficient_eq_image line 365
  36. theorem OAI.Erdos3.weightedCubeIntegerJetSum_coefficient line 376
  37. def OAI.Erdos3.weightedModerateIntegerSource line 399
  38. def OAI.Erdos3.weightedModerateIntegerBlock line 405
  39. theorem OAI.Erdos3.integerBooleanBlockJet_scaled_pairing line 411
  40. theorem OAI.Erdos3.weightedModerateGridCoefficient_eq_image line 421
  41. def OAI.Erdos3.weightedModerateIntegerProductSource line 436
  42. def OAI.Erdos3.weightedModerateIntegerJetSum line 443
  43. theorem OAI.Erdos3.weightedModerateIntegerJetSum_coefficient line 450
  44. def OAI.Erdos3.weightedCubeJetBound line 472
  45. theorem OAI.Erdos3.weightedCubeIntegerJetSum_bound line 476
  46. theorem OAI.Erdos3.weightedCubeIntegerGridMass_eq line 489