OAI/Geometry/PeriodicTiling/ScalarVanDerCorput.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PeriodicTilingThree.norm_vectorAverage line 22
  2. theorem OAI.PeriodicTilingThree.sum_shift_sub_sum line 27
  3. theorem OAI.PeriodicTilingThree.norm_sum_range_le_length line 40
  4. theorem OAI.PeriodicTilingThree.norm_shift_sum_sub_le line 49
  5. theorem OAI.PeriodicTilingThree.norm_shift_average_sub_le line 59
  6. def OAI.PeriodicTilingThree.smoothedAverage line 67
  7. theorem OAI.PeriodicTilingThree.smoothedAverage_eq_sum line 70
  8. theorem OAI.PeriodicTilingThree.smoothedAverage_sub line 76
  9. theorem OAI.PeriodicTilingThree.norm_smoothedAverage_sub_le line 86
  10. theorem OAI.PeriodicTilingThree.norm_vectorAverage_sq_le line 113
  11. def OAI.PeriodicTilingThree.offDiagonalAverage line 138
  12. theorem OAI.PeriodicTilingThree.block_energy_eq line 142
  13. theorem OAI.PeriodicTilingThree.diagonal_average_le_one line 158
  14. theorem OAI.PeriodicTilingThree.block_energy_le line 174
  15. theorem OAI.PeriodicTilingThree.norm_smoothedAverage_sq_le line 197
  16. theorem OAI.PeriodicTilingThree.finite_vanDerCorput line 212
  17. theorem OAI.PeriodicTilingThree.offDiagonalAverage_tendsto_zero line 238
  18. theorem OAI.PeriodicTilingThree.vectorAverage_tendsto_zero_of_shift_inner line 257
  19. theorem OAI.PeriodicTilingThree.vectorAverage_complex_inner_eq_re line 297
  20. theorem OAI.PeriodicTilingThree.complexAverage_vanDerCorput line 304