OAI/Combinatorics/Progressions/Lattices/AffineWindowGoodKernelBound.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.integerStrideHom line 13
  2. theorem OAI.Erdos3.integerStride_reflectsPairSums line 18
  3. def OAI.Erdos3.integerProgressionSupport line 24
  4. def OAI.Erdos3.supportedIntervalProgressionEquiv line 27
  5. theorem OAI.Erdos3.supportedIntervalProgressionEquiv_value line 36
  6. theorem OAI.Erdos3.integerScalarCubeWeights_progression_mean line 41
  7. abbrev OAI.Erdos3.TranslatedResidueSupportedCube line 62
  8. def OAI.Erdos3.shiftedScalarCubeResidueEquiv line 67
  9. theorem OAI.Erdos3.shiftedScalarCubeResidueEquiv_coordinates line 98
  10. theorem OAI.Erdos3.mem_integerProgressionSupport_iff line 115
  11. def OAI.Erdos3.progressionCubeResidues line 139
  12. def OAI.Erdos3.progressionResidueSupportedCubeEquiv line 143
  13. def OAI.Erdos3.affineScalarCubeWindowWeights line 183
  14. theorem OAI.Erdos3.affineScalarCubeWindowWeights_supported_mean line 191
  15. theorem OAI.Erdos3.affineScalarCubeWindowWeights_weight_le line 210
  16. theorem OAI.Erdos3.affineScalarCubeWindowWeights_progression_mean line 229
  17. theorem OAI.Erdos3.scalarKernelCutoff_window_size line 249
  18. theorem OAI.Erdos3.affineKernel_explicit_probability_le line 255
  19. theorem OAI.Erdos3.exists_affine_window_good_scalar_kernel_bound line 291