OAI/NumberTheory/DirichletL/Mellin/UniformKernelBounds.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicReflectionKernel.compact_family_mul_fourier_power_source_bound line 76
  2. theorem OAI.CubicReflectionKernel.compact_family_mul_fourier_weighted_source_bound line 115
  3. def OAI.CubicReflectionKernel.negativeLogPullbackCLM line 154
  4. theorem OAI.CubicReflectionKernel.negativeLogPullbackCLM_eq_actual line 158
  5. def OAI.CubicReflectionKernel.logWeight line 164
  6. theorem OAI.CubicReflectionKernel.logWeight_smooth line 166
  7. theorem OAI.CubicReflectionKernel.logWeight_support line 172
  8. theorem OAI.CubicReflectionKernel.logWeight_mul_pullback line 184
  9. theorem OAI.CubicReflectionKernel.mellin_strip_source_bound line 193
  10. theorem OAI.CubicReflectionKernel.mellinData_strip_source_bound line 228
  11. theorem OAI.CubicReflectionKernel.mellinEulerData_strip_source_bound line 258
  12. theorem OAI.CubicReflectionKernel.mellinInv_euler_line_source_bound line 285
  13. theorem OAI.CubicReflectionKernel.paperKernel_euler_source_power_decay line 315
  14. theorem OAI.CubicReflectionKernel.paperKernel_euler_source_uniform_weighted_bound line 364
  15. def OAI.FirstPassCubeLabels.gaussBlock line 429
  16. theorem OAI.FirstPassCubeLabels.canonicalProductGauss_eq_gaussBlock line 435
  17. def OAI.FirstPassCubeLabels.blockCross line 471
  18. theorem OAI.FirstPassCubeLabels.gaussBlock_union line 477
  19. theorem OAI.FirstPassCubeLabels.gaussBlock_congr line 518
  20. def OAI.FirstPassCubeLabels.cubeActiveSupport line 526
  21. def OAI.FirstPassCubeLabels.blockCubeExponent line 529
  22. theorem OAI.FirstPassCubeLabels.gaussBlock_cube_partition line 534
  23. theorem OAI.FirstPassCubeLabels.canonicalProductGauss_cube_partition line 561
  24. theorem OAI.FirstPassCubeLabels.columnCoefficient_eq_gaussBlock line 589
  25. theorem OAI.FirstPassCubeLabels.blockCross_two_eq_row_four line 600
  26. theorem OAI.FirstPassCubeLabels.columnCoefficient_union_row_four line 618
  27. theorem OAI.FirstPassCubeLabels.gaussBlock_norm_one line 639