OAI/Analysis/IrrationalRotation/Rotation/CircleKernelConvolution.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Invariant233.CircleKernelConvolution.convolution line 16
  2. theorem OAI.Invariant233.CircleKernelConvolution.integrable_unit_bounded line 19
  3. theorem OAI.Invariant233.CircleKernelConvolution.integrable_kernel line 24
  4. theorem OAI.Invariant233.CircleKernelConvolution.integrable_convolution_integrand line 28
  5. theorem OAI.Invariant233.CircleKernelConvolution.convolution_bounds line 42
  6. theorem OAI.Invariant233.CircleKernelConvolution.integrable_joint line 61
  7. theorem OAI.Invariant233.CircleKernelConvolution.integral_convolution line 77
  8. theorem OAI.Invariant233.CircleKernelConvolution.fourier_sub_argument line 86
  9. def OAI.Invariant233.CircleKernelConvolution.testCoefficient line 90
  10. theorem OAI.Invariant233.CircleKernelConvolution.integrable_test_character line 93
  11. theorem OAI.Invariant233.CircleKernelConvolution.norm_testCoefficient_le_one line 104
  12. theorem OAI.Invariant233.CircleKernelConvolution.testCoefficient_zero line 115
  13. theorem OAI.Invariant233.CircleKernelConvolution.convolution_eq_polynomial line 119
  14. def OAI.Invariant233.CircleKernelConvolution.translationError line 149
  15. theorem OAI.Invariant233.CircleKernelConvolution.translationError_nonneg line 152
  16. theorem OAI.Invariant233.CircleKernelConvolution.translationError_le_one line 155
  17. theorem OAI.Invariant233.CircleKernelConvolution.convolution_eq_shift line 169
  18. theorem OAI.Invariant233.CircleKernelConvolution.convolution_error_pointwise_le line 174
  19. theorem OAI.Invariant233.CircleKernelConvolution.integrable_joint_error line 201
  20. theorem OAI.Invariant233.CircleKernelConvolution.l1_error_le_translation_average line 219
  21. theorem OAI.Invariant233.CircleKernelConvolution.l1_error_le_small_translation_and_tail line 233