OAI/NumberTheory/DirichletL/Detector/RadialMellin.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.ProbeRadialMellin.laplace line 11
  2. lemma OAI.SevenEighths.ProbeRadialMellin.mellin_real line 14
  3. lemma OAI.SevenEighths.ProbeRadialMellin.mellinConvergent_real line 22
  4. lemma OAI.SevenEighths.ProbeRadialMellin.gamma_scaled_integrable line 31
  5. lemma OAI.SevenEighths.ProbeRadialMellin.gamma_scaled_integral line 43
  6. lemma OAI.SevenEighths.ProbeRadialMellin.laplace_mellin_integrable line 49
  7. lemma OAI.SevenEighths.ProbeRadialMellin.mellin_laplace line 89
  8. def OAI.SevenEighths.ProbeRadialMellin.paperConstant line 128
  9. lemma OAI.SevenEighths.ProbeRadialMellin.paperConstant_pos line 130
  10. lemma OAI.SevenEighths.ProbeRadialMellin.paperConstant_sq line 134
  11. lemma OAI.SevenEighths.ProbeRadialMellin.paperE_norm line 139
  12. lemma OAI.SevenEighths.ProbeRadialMellin.paper_fourier_pairing line 143
  13. lemma OAI.SevenEighths.ProbeRadialMellin.paper_gaussian_fourier line 164
  14. lemma OAI.SevenEighths.ProbeRadialMellin.radial_continuous line 181
  15. lemma OAI.SevenEighths.ProbeRadialMellin.radial_isBigO_top line 185
  16. lemma OAI.SevenEighths.ProbeRadialMellin.radial_isBigO_zero line 200
  17. theorem OAI.SevenEighths.ProbeRadialMellin.radial_mellin_convergent line 208
  18. theorem OAI.SevenEighths.ProbeRadialMellin.radial_mellin_differentiable line 215
  19. lemma OAI.SevenEighths.ProbeRadialMellin.radial_laplace_duality line 223
  20. lemma OAI.SevenEighths.ProbeRadialMellin.mellin_reciprocal_laplace line 251
  21. theorem OAI.SevenEighths.ProbeRadialMellin.radial_mellin_gamma line 267
  22. lemma OAI.SevenEighths.ProbeRadialMellin.paper_prefactor line 293
  23. theorem OAI.SevenEighths.ProbeRadialMellin.radial_mellin_identity line 305
  24. lemma OAI.SevenEighths.ProbeRadialMellin.positive_source_mellin line 312
  25. theorem OAI.SevenEighths.ProbeRadialMellin.radial_mellin_positive line 359
  26. theorem OAI.SevenEighths.ProbeRadialMellin.radial_mellin_one_sixth_pos line 380
  27. theorem OAI.SevenEighths.ProbeRadialMellin.radial_mellin_identity_right line 388
  28. lemma OAI.SevenEighths.ProbeRadialMellin.gamma_quotient_strip line 421
  29. theorem OAI.SevenEighths.ProbeRadialMellin.radial_mellin_strip_decay line 449
  30. theorem OAI.SevenEighths.ProbeRadialMellin.radial_mellin_analytic line 487
  31. theorem OAI.SevenEighths.ProbeRadialMellin.radial_mellin_strip_rapid line 492
  32. theorem OAI.SevenEighths.ProbeRadialMellin.radial_mellin_vertical_integrable line 500
  33. theorem OAI.SevenEighths.ProbeRadialMellin.radial_mellin_inverse_integrable line 514
  34. theorem OAI.SevenEighths.ProbeRadialMellin.radial_mellin_inversion line 529
  35. theorem OAI.SevenEighths.ProbeRadialMellin.radial_mellin_one_sixth_ne_zero line 537