OAI/NumberTheory/DirichletL/Mellin/InverseContour.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicReflectionKernel.inverseMellinIntegrand line 76
  2. theorem OAI.CubicReflectionKernel.inverseMellinIntegrand_differentiableAt line 79
  3. theorem OAI.CubicReflectionKernel.inverseMellinIntegrand_vertical_integrable line 88
  4. theorem OAI.CubicReflectionKernel.inverseMellinIntegrand_strip_bound line 102
  5. theorem OAI.CubicReflectionKernel.mellinInv_euler_shift line 124
  6. theorem OAI.CubicReflectionKernel.mellinInv_euler_line_bound line 152
  7. def OAI.CubicReflectionKernel.paperEulerKernel line 181
  8. theorem OAI.CubicReflectionKernel.mellinEulerData_axis line 184
  9. theorem OAI.CubicReflectionKernel.paperEulerKernel_eq_euler line 196
  10. theorem OAI.CubicReflectionKernel.paperKernel_euler_decay_at_line line 210
  11. theorem OAI.CubicReflectionKernel.paperKernel_euler_power_decay line 226
  12. theorem OAI.CubicReflectionKernel.paperKernel_euler_uniform_weighted_bound line 253
  13. abbrev OAI.DescentFiberCost.O line 304
  14. theorem OAI.DescentFiberCost.finite_ideal_count_real line 306
  15. theorem OAI.DescentFiberCost.fixed_triple_count line 319
  16. theorem OAI.DescentFiberCost.complete_second_prefactor line 367
  17. theorem OAI.DescentFiberCost.complete_second_zero_prefactor line 380
  18. theorem OAI.EisensteinSchwartzPoisson.fourier_real_line_integrable line 396
  19. theorem OAI.EisensteinSchwartzPoisson.fourier_real_line_integral line 403
  20. theorem OAI.EisensteinSchwartzPoisson.paperFrequency_imaginary line 420
  21. theorem OAI.EisensteinSchwartzPoisson.paperRadialFourier_square line 426
  22. theorem OAI.EisensteinSchwartzPoisson.radial_square_integrable line 436
  23. theorem OAI.EisensteinSchwartzPoisson.paperRadialFourier_square_integrable line 443
  24. theorem OAI.EisensteinSchwartzPoisson.paperRadialFourier_square_integral line 453
  25. theorem OAI.EisensteinSchwartzPoisson.integral_even_eq_twice_Ioi line 471
  26. theorem OAI.EisensteinSchwartzPoisson.paperRadialFourier_halfline_integral line 481
  27. def OAI.CubicReflectionKernel.logRadius line 496
  28. theorem OAI.CubicReflectionKernel.logRadius_pos line 498
  29. def OAI.CubicReflectionKernel.logCutoff line 500
  30. def OAI.CubicReflectionKernel.logOuterCutoff line 506
  31. def OAI.CubicReflectionKernel.expCorrection line 512
  32. def OAI.CubicReflectionKernel.patchedExp line 513
  33. theorem OAI.CubicReflectionKernel.expCorrection_compact line 515
  34. theorem OAI.CubicReflectionKernel.expCorrection_smooth line 518
  35. theorem OAI.CubicReflectionKernel.patchedExp_temperate line 521
  36. theorem OAI.CubicReflectionKernel.patchedExp_proper line 525
  37. def OAI.CubicReflectionKernel.logPullbackCLM line 538
  38. theorem OAI.CubicReflectionKernel.logPullbackCLM_apply line 542
  39. theorem OAI.CubicReflectionKernel.logCutoff_eq_one_of_source line 548
  40. theorem OAI.CubicReflectionKernel.patchedExp_eq_exp_of_cutoff_ne_zero line 560
  41. theorem OAI.CubicReflectionKernel.logPullbackCLM_eq_actual line 571
  42. theorem OAI.CubicReflectionKernel.compact_family_deriv_sup_bound line 588
  43. theorem OAI.CubicReflectionKernel.compact_family_mul_deriv_L1_source_bound line 608