OAI/Combinatorics/Progressions/Lattices/AffineBlockScale.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.centeredFundamentalBox line 9
  2. theorem OAI.Erdos3.centeredFundamentalBox_of_support line 12
  3. theorem OAI.Erdos3.centeredFundamentalBox_iff line 23
  4. theorem OAI.Erdos3.integerGridMass_eq_imageMass_on_centered_box line 31
  5. theorem OAI.Erdos3.integerGridDensity_eq_imageMass_on_centered_box line 44
  6. theorem OAI.Erdos3.finiteImageMass_total line 65
  7. theorem OAI.Erdos3.integerGridMass_total line 72
  8. theorem OAI.Erdos3.integerImageMass_total_on_box line 78
  9. theorem OAI.Erdos3.integerGridDensity_total line 87
  10. def OAI.Erdos3.centeredGridRepresentative line 93
  11. theorem OAI.Erdos3.centeredGridRepresentative_mem line 97
  12. def OAI.Erdos3.affineWeightedCubeGridCoefficient line 114
  13. def OAI.Erdos3.affineWeightedModerateGridCoefficient line 122
  14. theorem OAI.Erdos3.affineWeightedCubeGridCoefficient_norm_le_one line 130
  15. theorem OAI.Erdos3.affineWeightedModerateGridCoefficient_norm_le_one line 138
  16. theorem OAI.Erdos3.affineWeightedCubeGridCoefficient_mem_cover line 158
  17. theorem OAI.Erdos3.affineWeightedModerateGridCoefficient_mem_cover line 179
  18. def OAI.Erdos3.affineWeightedCubeIntegerBlock line 222
  19. theorem OAI.Erdos3.affineWeightedCubeGridCoefficient_eq_image line 228
  20. def OAI.Erdos3.affineWeightedCubeIntegerSum line 243
  21. theorem OAI.Erdos3.affineWeightedCubeIntegerSum_coefficient line 250
  22. def OAI.Erdos3.affineWeightedModerateIntegerBlock line 264
  23. theorem OAI.Erdos3.affineWeightedModerateGridCoefficient_eq_image line 272
  24. def OAI.Erdos3.affineWeightedModerateIntegerSum line 292
  25. theorem OAI.Erdos3.affineWeightedModerateIntegerSum_coefficient line 300
  26. def OAI.Erdos3.affineCubeCoordinateRadius line 324
  27. theorem OAI.Erdos3.affineIntegerCubeCoordinates_bound line 328
  28. def OAI.Erdos3.affineWeightedCubeJetBound line 347
  29. theorem OAI.Erdos3.affineWeightedCubeIntegerSum_bound line 354
  30. def OAI.Erdos3.affineWeightedModerateJetBound line 369
  31. theorem OAI.Erdos3.affineWeightedModerateIntegerBlock_bound line 377
  32. theorem OAI.Erdos3.affineWeightedModerateIntegerSum_bound line 397
  33. theorem OAI.Erdos3.affineWeightedCube_mass_on_fundamental_box line 410
  34. theorem OAI.Erdos3.affineWeightedModerate_mass_on_fundamental_box line 424
  35. theorem OAI.Erdos3.affineCubeCoordinateRadius_le line 449
  36. theorem OAI.Erdos3.affine_coordinate_relative_bound line 463
  37. def OAI.Erdos3.affineBlockScaleBound line 470
  38. theorem OAI.Erdos3.affineBlockScaleBound_nonneg line 473
  39. theorem OAI.Erdos3.affineCube_radius_product_le line 477
  40. theorem OAI.Erdos3.affineWeightedCubeJetBound_le_scale line 489
  41. theorem OAI.Erdos3.affineWeightedModerateJetBound_le_scale line 518