OAI/NumberTheory/DirichletL/Mellin/VerticalContourShift.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.VerticalContourShift.gaussian_regulator_norm line 80
  2. lemma OAI.VerticalContourShift.gaussian_regulator_norm_le line 88
  3. def OAI.VerticalContourShift.gaussianRegulatorSequence line 95
  4. lemma OAI.VerticalContourShift.gaussianRegulatorSequence_pos line 97
  5. lemma OAI.VerticalContourShift.gaussianRegulatorSequence_le_one line 101
  6. lemma OAI.VerticalContourShift.gaussianRegulatorSequence_tendsto line 106
  7. theorem OAI.VerticalContourShift.gaussian_regulator_integral_tendsto line 109
  8. lemma OAI.VerticalContourShift.rpow_between_endpoints line 134
  9. theorem OAI.VerticalContourShift.mellin_uniform_strip_bound line 142
  10. lemma OAI.GaussianMoment.gaussian_le_inverse_quadratic line 165
  11. lemma OAI.GaussianMoment.linear_height_young line 180
  12. theorem OAI.GaussianMoment.gaussian_regulator_strip_bound line 192
  13. theorem OAI.GaussianMoment.gaussian_regulator_strip_decay line 231
  14. theorem OAI.VerticalContourShift.integral_eq_of_exponential_strip_growth line 248
  15. lemma OAI.CubicGammaExponential.norm_Gamma_le_real line 292
  16. lemma OAI.CubicGammaExponential.norm_sin_le_exp_abs_im line 304
  17. lemma OAI.CubicGammaExponential.Gamma_ne_zero_of_im_ne_zero line 316
  18. lemma OAI.CubicGammaExponential.inverse_Gamma_reflection line 323
  19. lemma OAI.CubicGammaExponential.inverse_Gamma_norm_of_left line 341
  20. lemma OAI.CubicGammaExponential.inverse_Gamma_norm_le_shift_left line 359
  21. lemma OAI.CubicGammaExponential.real_Gamma_compact_bound line 374
  22. lemma OAI.CubicGammaExponential.inverse_Gamma_compact_strip_bound line 383
  23. theorem OAI.CubicGammaExponential.inverse_Gamma_strip_exp_bound line 395
  24. theorem OAI.CubicGammaExponential.inverse_Gamma_strip_exp_bound_complex line 435
  25. theorem OAI.CubicGammaExponential.inverse_cubic_Gamma_pair_strip_bound line 443
  26. lemma OAI.CubicEisenstein.cubic_bessel_mellin_norm_scale line 469
  27. lemma OAI.CubicEisenstein.weighted_cubic_bessel_integral_norm line 500
  28. theorem OAI.CubicEisenstein.cubic_bessel_series_mellin line 512
  29. lemma OAI.CubicEisenstein.positive_sqrt_cpow_twice line 536
  30. lemma OAI.CubicEisenstein.radial_bessel_coefficient_norm line 548
  31. lemma OAI.CubicEisenstein.radial_bessel_coefficient_identity line 564
  32. def OAI.CubicEisenstein.radialBesselProfile line 578
  33. theorem OAI.CubicEisenstein.radialBesselProfile_mellin line 582