OAI/NumberTheory/DirichletL/Poisson/RadialFourier.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EisensteinSchwartzPoisson.radialTestCLM line 70
  2. theorem OAI.EisensteinSchwartzPoisson.radialTestCLM_apply line 76
  3. def OAI.EisensteinSchwartzPoisson.radialFourierCLM line 80
  4. theorem OAI.EisensteinSchwartzPoisson.radialFourierCLM_apply line 83
  5. theorem OAI.EisensteinSchwartzPoisson.paperRadialFourier_eq_plane line 87
  6. theorem OAI.EisensteinSchwartzPoisson.paperFrequency_sqrt_norm_sq line 93
  7. theorem OAI.EisensteinSchwartzPoisson.paperRadialFourier_weighted_bound line 99
  8. theorem OAI.EisensteinSchwartzPoisson.schwartzCLM_finite_seminorm_control line 129
  9. theorem OAI.EisensteinSchwartzPoisson.paperRadialFourier_source_weighted_bound line 146
  10. theorem OAI.EisensteinSchwartzPoisson.paperRadialFourier_source_decay line 160
  11. def OAI.EisensteinSchwartzPoisson.halfEulerCLM line 177
  12. theorem OAI.EisensteinSchwartzPoisson.halfEulerCLM_apply line 181
  13. theorem OAI.EisensteinSchwartzPoisson.hasDerivAt_halfFlow line 190
  14. theorem OAI.EisensteinSchwartzPoisson.iteratedDeriv_halfFlow line 199
  15. theorem OAI.EisensteinSchwartzPoisson.sqrt_exp_half line 212
  16. theorem OAI.EisensteinSchwartzPoisson.eulerDeriv_sqrt_profile line 218
  17. theorem OAI.EisensteinSchwartzPoisson.contDiffOn_sqrt_profile line 229
  18. theorem OAI.EisensteinSchwartzPoisson.contDiff_sqrt_profile_log line 235
  19. theorem OAI.EisensteinSchwartzPoisson.sqrt_profile_rapid_bound line 244
  20. theorem OAI.EisensteinSchwartzPoisson.eulerDeriv_sqrt_profile_rapid_bound line 269
  21. theorem OAI.EisensteinSchwartzPoisson.paperFrequency_real_temperate line 279
  22. theorem OAI.EisensteinSchwartzPoisson.paperFrequency_real_growth line 288
  23. def OAI.EisensteinSchwartzPoisson.paperRealRayCLM line 297
  24. theorem OAI.EisensteinSchwartzPoisson.paperRealRayCLM_apply line 301
  25. def OAI.EisensteinSchwartzPoisson.halfEulerIterateCLM line 304
  26. theorem OAI.EisensteinSchwartzPoisson.halfEulerIterateCLM_apply line 308
  27. def OAI.EisensteinSchwartzPoisson.paperFourierRayCLM line 317
  28. theorem OAI.EisensteinSchwartzPoisson.paperFourierRayCLM_apply line 320
  29. theorem OAI.EisensteinSchwartzPoisson.paperRadialFourier_eq_ray line 325
  30. def OAI.EisensteinSchwartzPoisson.paperEulerCLM line 330
  31. theorem OAI.EisensteinSchwartzPoisson.paperRadialFourier_eulerDeriv line 333
  32. theorem OAI.EisensteinSchwartzPoisson.paperRadialFourier_contDiffOn line 340
  33. theorem OAI.EisensteinSchwartzPoisson.paperRadialFourier_log_contDiff line 345
  34. theorem OAI.EisensteinSchwartzPoisson.paperRadialFourier_euler_weighted_bound line 350
  35. theorem OAI.EisensteinSchwartzPoisson.schwartzCLM_family_finite_seminorm_control line 358
  36. theorem OAI.EisensteinSchwartzPoisson.paperRadialFourier_euler_source_weighted_bound line 394
  37. theorem OAI.EisensteinSchwartzPoisson.paperRadialFourier_euler_source_decay line 407
  38. theorem OAI.EisensteinSchwartzPoisson.paperRadialFourier_euler_bound line 418
  39. theorem OAI.EisensteinSchwartzPoisson.compact_paperRadialFourier_regular line 426
  40. theorem OAI.EisensteinSchwartzPoisson.paperRadialFourier_log_separation line 435
  41. theorem OAI.EisensteinSchwartzPoisson.inverse_square_le_cauchy_product line 461
  42. theorem OAI.EisensteinSchwartzPoisson.eisenstein_cauchy_summable line 477
  43. def OAI.EisensteinSchwartzPoisson.eisensteinCauchyMass line 493
  44. theorem OAI.EisensteinSchwartzPoisson.eisensteinCauchyMass_nonneg line 496
  45. theorem OAI.EisensteinSchwartzPoisson.eisensteinCauchyMass_subtype line 499
  46. theorem OAI.EisensteinSchwartzPoisson.polynomial_tail_majorant line 505
  47. theorem OAI.EisensteinSchwartzPoisson.paperRadialFourier_lattice_summable_norm line 533
  48. theorem OAI.EisensteinSchwartzPoisson.paperRadialFourier_lattice_tail line 544
  49. theorem OAI.ConcretePrimeRowBridge.idealSupport_injective_on_squarefree line 591
  50. theorem OAI.ConcretePrimeRowBridge.baseChangeWeight_eq_zero_of_not_squarefree line 615