OAI/Combinatorics/Progressions/Estimates/SplitSmoothProductProfile.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.splitInputProfile line 20
  2. theorem OAI.Erdos3.splitCoordinates_norm line 23
  3. theorem OAI.Erdos3.splitInputProfile_lipschitz line 40
  4. theorem OAI.Erdos3.splitInputProfile_zero_outside line 51
  5. theorem OAI.Erdos3.splitInputProfile_integral line 56
  6. theorem OAI.Erdos3.splitInputProfile_sample_sum line 62
  7. def OAI.Erdos3.tensorCutoffWeight line 80
  8. theorem OAI.Erdos3.tensorCutoffWeight_nonneg line 83
  9. theorem OAI.Erdos3.tensorCutoffWeight_tsupport line 87
  10. theorem OAI.Erdos3.tensorCutoffWeight_compact line 102
  11. theorem OAI.Erdos3.tensorCutoffWeight_contDiff line 108
  12. theorem OAI.Erdos3.tensorCutoffWeight_integral line 115
  13. theorem OAI.Erdos3.tensorCutoffWeight_abs_mass line 120
  14. theorem OAI.Erdos3.tensorCutoffWeight_abs_mass_le_one line 126
  15. theorem OAI.Erdos3.tensorCutoffWeight_mass_loss line 132
  16. def OAI.Erdos3.scaledInputWeightSum line 157
  17. def OAI.Erdos3.scaledInputMass line 160
  18. theorem OAI.Erdos3.scaledIntegerWeight_summable line 163
  19. theorem OAI.Erdos3.scaledInputMass_error line 177
  20. theorem OAI.Erdos3.scaledInputMass_nonneg line 198
  21. theorem OAI.Erdos3.scaledInputMass_bounds line 204
  22. def OAI.Erdos3.sigmaAxisWeight line 229
  23. theorem OAI.Erdos3.sigmaAxisWeight_contDiff line 232
  24. theorem OAI.Erdos3.sigmaAxisWeight_compact line 237
  25. theorem OAI.Erdos3.sigmaAxisWeight_tsupport line 242
  26. theorem OAI.Erdos3.sigmaAxisWeight_nonneg line 252
  27. theorem OAI.Erdos3.sigmaAxisWeight_integral line 256
  28. theorem OAI.Erdos3.sigmaAxisWeight_abs_mass line 264
  29. theorem OAI.Erdos3.sigmaAxisWeight_abs_mass_le_one line 272
  30. theorem OAI.Erdos3.sigmaAxisWeight_mass_loss line 277
  31. def OAI.Erdos3.smoothProductProfile line 295
  32. theorem OAI.Erdos3.smoothProductProfile_eq_cutoff line 298
  33. theorem OAI.Erdos3.smoothProductProfile_contDiff line 303
  34. theorem OAI.Erdos3.smoothProductProfile_compact line 308
  35. theorem OAI.Erdos3.smoothProductProfile_range line 313
  36. theorem OAI.Erdos3.smoothProductProfile_norm_le line 319
  37. theorem OAI.Erdos3.smoothProductProfile_zero_outside line 324
  38. theorem OAI.Erdos3.smoothProductProfile_integral line 335
  39. theorem OAI.Erdos3.smoothProductProfile_lipschitz line 341
  40. theorem OAI.Erdos3.smoothProductProfile_equiv line 348
  41. theorem OAI.Erdos3.smoothProductProfile_sum line 352
  42. theorem OAI.Erdos3.tensorCutoffWeight_update line 369
  43. theorem OAI.Erdos3.tensorCutoffWeight_fderiv_single line 380
  44. theorem OAI.Erdos3.tensorCutoffWeight_derivative_integral line 398
  45. theorem OAI.Erdos3.tensorCutoffWeight_derivative_le line 420
  46. def OAI.Erdos3.splitSmoothProductProfile line 442
  47. theorem OAI.Erdos3.splitSmoothProductProfile_range line 446
  48. theorem OAI.Erdos3.splitSmoothProductProfile_integrable line 453
  49. theorem OAI.Erdos3.splitSmoothProductProfile_integral line 459
  50. theorem OAI.Erdos3.splitSmoothProductProfile_lipschitz line 464
  51. theorem OAI.Erdos3.splitSmoothProductProfile_zero_outside line 476
  52. theorem OAI.Erdos3.splitSmoothProductProfile_join line 483