OAI/NumberTheory/PrimePackets/ZeroReflection.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.AnalyticGrowth.zeroMultiplicity_reflection line 95
  2. lemma OAI.PrimeDegreePackets.AnalyticGrowth.logDeriv_reflection line 106
  3. lemma OAI.PrimeDegreePackets.AnalyticGrowth.hasSum_of_nonneg_finite_exhaustion line 122
  4. def OAI.PrimeDegreePackets.AnalyticGrowth.realZeroPole line 158
  5. lemma OAI.PrimeDegreePackets.AnalyticGrowth.realZeroPole_nonneg line 161
  6. lemma OAI.PrimeDegreePackets.AnalyticGrowth.realZeroPole_pair line 172
  7. lemma OAI.PrimeDegreePackets.AnalyticGrowth.diskPoleSum_sub_re line 182
  8. theorem OAI.PrimeDegreePackets.AnalyticGrowth.hasSum_realZeroPole line 193
  9. lemma OAI.PrimeDegreePackets.HeckeMellin.lintegral_comp_pos_mul line 240
  10. lemma OAI.PrimeDegreePackets.HeckeMellin.lintegral_snoc line 256
  11. def OAI.PrimeDegreePackets.HeckeMellin.coordinates line 273
  12. lemma OAI.PrimeDegreePackets.HeckeMellin.continuous_coordinates line 276
  13. theorem OAI.PrimeDegreePackets.HeckeMellin.lintegral_coordinates line 284
  14. theorem OAI.PrimeDegreePackets.HeckeMellin.map_coordinates line 325
  15. lemma OAI.PrimeDegreePackets.HeckeMellin.integral_coordinates line 338
  16. lemma OAI.PrimeDegreePackets.HeckeMellin.integrable_coordinates line 347
  17. def OAI.PrimeDegreePackets.HeckeMellin.logGammaKernel line 363
  18. lemma OAI.PrimeDegreePackets.HeckeMellin.logGammaKernel_eq line 366
  19. lemma OAI.PrimeDegreePackets.HeckeMellin.integrable_logGammaKernel line 377
  20. lemma OAI.PrimeDegreePackets.HeckeMellin.integral_logGammaKernel line 388
  21. def OAI.PrimeDegreePackets.HeckeMellin.gaussianLogKernel line 400
  22. lemma OAI.PrimeDegreePackets.HeckeMellin.gaussianLogKernel_eq line 403
  23. lemma OAI.PrimeDegreePackets.HeckeMellin.integrable_gaussianLogKernel line 414
  24. lemma OAI.PrimeDegreePackets.HeckeMellin.integral_gaussianLogKernel line 421
  25. lemma OAI.PrimeDegreePackets.HeckeMellin.continuous_gaussianLogKernel line 432
  26. lemma OAI.PrimeDegreePackets.HeckeMellin.integral_gaussianLogKernel_product line 438
  27. lemma OAI.PrimeDegreePackets.HeckeMellin.integrable_gaussianLogKernel_product line 444
  28. lemma OAI.PrimeDegreePackets.HeckeMellin.exp_two_mul line 449
  29. lemma OAI.PrimeDegreePackets.HeckeMellin.scaled_cpow line 452
  30. lemma OAI.PrimeDegreePackets.HeckeMellin.gaussianLogKernel_scale line 466
  31. lemma OAI.PrimeDegreePackets.HeckeMellin.integral_scaled_gaussianLogKernel line 474
  32. lemma OAI.PrimeDegreePackets.HeckeMellin.prod_abs_cpow line 483
  33. lemma OAI.PrimeDegreePackets.HeckeMellin.coordinates_eq line 500
  34. lemma OAI.PrimeDegreePackets.HeckeMellin.sum_coordinates line 505
  35. def OAI.PrimeDegreePackets.HeckeMellin.logEnergy line 513
  36. lemma OAI.PrimeDegreePackets.HeckeMellin.continuous_logEnergy line 516
  37. lemma OAI.PrimeDegreePackets.HeckeMellin.logEnergy_pos line 522
  38. def OAI.PrimeDegreePackets.HeckeMellin.logRadialKernel line 531
  39. lemma OAI.PrimeDegreePackets.HeckeMellin.gaussianLogKernel_coordinates line 535
  40. lemma OAI.PrimeDegreePackets.HeckeMellin.integrable_logRadialKernel line 559
  41. theorem OAI.PrimeDegreePackets.HeckeMellin.integral_logRadialKernel line 573
  42. def OAI.PrimeDegreePackets.HeckeMellin.radialKernel line 598
  43. lemma OAI.PrimeDegreePackets.HeckeMellin.logRadialKernel_eq_radial line 603
  44. lemma OAI.PrimeDegreePackets.HeckeMellin.radialIntegral_log line 615
  45. lemma OAI.PrimeDegreePackets.HeckeMellin.integrable_radialIntegral line 622
  46. theorem OAI.PrimeDegreePackets.HeckeMellin.integral_radialKernel line 638