OAI/Analysis/ModularRecovery/FourierKernels.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Fourier kernels and uniform bounds for Gaussian multipliers.

  1. def OAI.BoundedRecovery.kernelMass line 17
  2. def OAI.BoundedRecovery.kernelFourier line 19
  3. lemma OAI.BoundedRecovery.kernelMass_pos line 21
  4. lemma OAI.BoundedRecovery.integrable_fourierKernel line 31
  5. lemma OAI.BoundedRecovery.norm_kernelFourier_le line 40
  6. lemma OAI.BoundedRecovery.continuous_kernelFourier line 46
  7. lemma OAI.BoundedRecovery.kernelFourier_zero line 59
  8. lemma OAI.BoundedRecovery.kernelMultiplier_shift line 64
  9. lemma OAI.BoundedRecovery.integrable_cutoff_fourierKernel line 73
  10. lemma OAI.BoundedRecovery.norm_kernelMultiplier_le line 86
  11. lemma OAI.BoundedRecovery.StandardModularData.kernelAverage_nonneg line 105
  12. lemma OAI.BoundedRecovery.StandardModularData.kernelAverage_mono line 118
  13. lemma OAI.BoundedRecovery.StandardModularData.kernelAverage_one line 125
  14. lemma OAI.BoundedRecovery.StandardModularData.norm_kernelAverage_one_le line 137
  15. lemma OAI.BoundedRecovery.StandardModularData.norm_kernelAverage_of_nonneg line 145
  16. lemma OAI.BoundedRecovery.StandardModularData.kernelAverage_sum line 161
  17. lemma OAI.BoundedRecovery.StandardModularData.norm_kernelAverage_le line 170
  18. lemma OAI.BoundedRecovery.gaussianCutoff_antitone_abs line 194
  19. def OAI.BoundedRecovery.kernelCutoffError line 201
  20. lemma OAI.BoundedRecovery.integrable_kernelCutoffError line 204
  21. lemma OAI.BoundedRecovery.kernelCutoffError_nonneg line 216
  22. lemma OAI.BoundedRecovery.kernelCutoffError_tendsto line 221
  23. lemma OAI.BoundedRecovery.norm_kernelMultiplier_sub_le line 236
  24. lemma OAI.BoundedRecovery.kernelMultiplier_mul_tendsto line 260