OAI/Combinatorics/Progressions/Estimates/PartialComplexScaledQuadrature.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.sampledWeightIndices line 15
  2. def OAI.Erdos3.sampledWeight line 18
  3. def OAI.Erdos3.sampledWeightSum line 21
  4. def OAI.Erdos3.sampledWeightHistogram line 24
  5. theorem OAI.Erdos3.sampledWeight_zero_off_indices line 27
  6. theorem OAI.Erdos3.sampledWeightSum_eq_tsum line 41
  7. theorem OAI.Erdos3.sampledWeightHistogram_eq line 46
  8. theorem OAI.Erdos3.sampledWeightHistogram_integrable line 51
  9. theorem OAI.Erdos3.sampledWeightHistogram_integral line 54
  10. theorem OAI.Erdos3.sampledWeightSum_nonneg line 58
  11. def OAI.Erdos3.finiteRectangularHistogram line 74
  12. theorem OAI.Erdos3.rectangularLatticeCell_indicator_integrable line 78
  13. theorem OAI.Erdos3.finiteRectangularHistogram_integrable line 83
  14. theorem OAI.Erdos3.finiteRectangularHistogram_integral line 89
  15. theorem OAI.Erdos3.finiteRectangularHistogram_eq_round line 102
  16. theorem OAI.Erdos3.finiteRectangularHistogram_mul_test line 128
  17. theorem OAI.Erdos3.finiteRectangularHistogram_test_integral line 141
  18. theorem OAI.Erdos3.finiteRectangularHistogram_normalized_mean line 148
  19. def OAI.Erdos3.rectangularWeightIndices line 174
  20. def OAI.Erdos3.rectangularWeight line 178
  21. def OAI.Erdos3.rectangularWeightSum line 181
  22. def OAI.Erdos3.rectangularWeightHistogram line 184
  23. theorem OAI.Erdos3.rectangularWeight_zero_off_indices line 188
  24. theorem OAI.Erdos3.rectangularWeight_summable line 207
  25. theorem OAI.Erdos3.rectangularWeightSum_eq_tsum line 212
  26. theorem OAI.Erdos3.rectangularWeightHistogram_eq line 217
  27. theorem OAI.Erdos3.rectangularWeightHistogram_integrable line 223
  28. theorem OAI.Erdos3.rectangularWeightHistogram_integral line 226
  29. theorem OAI.Erdos3.rectangularWeightHistogram_error line 244
  30. theorem OAI.Erdos3.rectangularWeightHistogram_zero_outside line 253
  31. theorem OAI.Erdos3.rectangularWeightHistogram_l1_error line 268
  32. theorem OAI.Erdos3.rectangularWeightSum_error line 283
  33. theorem OAI.Erdos3.rectangularLattice_quadrature line 295
  34. theorem OAI.Erdos3.sampledWeightIndices_mem_bound line 314
  35. theorem OAI.Erdos3.sampledWeightIndices_card_le line 322
  36. theorem OAI.Erdos3.rectangularWeightIndices_card_le line 331
  37. theorem OAI.Erdos3.rectangularLatticePoint_scaled line 360
  38. theorem OAI.Erdos3.scaledRectangularWeight_summable line 368
  39. theorem OAI.Erdos3.scaledRectangular_quadrature line 377
  40. theorem OAI.Erdos3.rectangularLatticePoint_zero_origin line 404
  41. theorem OAI.Erdos3.rectangularLatticePoint_sub_displacement line 410
  42. theorem OAI.Erdos3.rectangularWeight_translation_pointwise line 418
  43. theorem OAI.Erdos3.rectangularWeight_translation_l1 line 427
  44. theorem OAI.Erdos3.scaledRectangularComplex_summable line 455
  45. theorem OAI.Erdos3.compactBox_complex_integrable line 467
  46. theorem OAI.Erdos3.scaledRectangular_complex_quadrature line 476
  47. theorem OAI.Erdos3.normalized_rectangular_translation_test_le line 525
  48. theorem OAI.Erdos3.partial_scaledRectangular_complex_quadrature line 563