OAI/NumberTheory/PrimePackets/RadialIntegrals.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.HeckeMellin.measurable_radialKernel line 95
  2. lemma OAI.PrimeDegreePackets.HeckeMellin.lintegral_exp_product line 101
  3. lemma OAI.PrimeDegreePackets.HeckeMellin.lintegral_norm_radialKernel line 117
  4. theorem OAI.PrimeDegreePackets.HeckeMellin.integrable_radialKernel_product line 128
  5. def OAI.PrimeDegreePackets.HeckeMellin.realRadialKernel line 146
  6. lemma OAI.PrimeDegreePackets.HeckeMellin.radialKernel_ofReal line 150
  7. lemma OAI.PrimeDegreePackets.HeckeMellin.norm_radialKernel line 159
  8. lemma OAI.PrimeDegreePackets.HeckeMellin.integral_radialKernel_ofReal line 171
  9. theorem OAI.PrimeDegreePackets.HeckeMellin.integral_realRadialKernel line 181
  10. lemma OAI.PrimeDegreePackets.HeckeMellin.logEnergy_embeddings line 198
  11. theorem OAI.PrimeDegreePackets.HeckeMellin.arithmetic_gaussian_mellin line 205
  12. lemma OAI.PrimeDegreePackets.HeckeMellin.measurable_realRadialKernel line 232
  13. lemma OAI.PrimeDegreePackets.HeckeMellin.ae_positive_first line 238
  14. lemma OAI.PrimeDegreePackets.HeckeMellin.integrable_realRadialKernel line 242
  15. theorem OAI.PrimeDegreePackets.HeckeMellin.lintegral_realRadialKernel line 252
  16. theorem OAI.PrimeDegreePackets.HeckeMellin.arithmetic_gaussian_lintegral line 267
  17. lemma OAI.PrimeDegreePackets.HeckeMellin.idealElementRepresentative_absNorm line 298
  18. lemma OAI.PrimeDegreePackets.HeckeMellin.measurable_arithmeticFlowGaussian_joint line 314
  19. def OAI.PrimeDegreePackets.HeckeMellin.realHeckeFactor line 322
  20. lemma OAI.PrimeDegreePackets.HeckeMellin.realHeckeFactor_nonneg line 325
  21. theorem OAI.PrimeDegreePackets.HeckeMellin.fractionalIdealTheta_mellin_lintegral line 333
  22. theorem OAI.PrimeDegreePackets.HeckeMellin.integralFractionalIdeals_norm_tsum line 391
  23. def OAI.PrimeDegreePackets.HeckeMellin.nonnegativeIdealThetaMellin line 412
  24. lemma OAI.PrimeDegreePackets.HeckeMellin.rpow_cancel_ennreal_factor line 420
  25. theorem OAI.PrimeDegreePackets.HeckeMellin.classTheta_mellin_lintegral line 431
  26. lemma OAI.PrimeDegreePackets.HeckeMellin.idealClass_norm_tsum_ne_top line 457
  27. lemma OAI.PrimeDegreePackets.HeckeMellin.nonnegativeIdealThetaMellin_ne_top line 470
  28. lemma OAI.PrimeDegreePackets.HeckeMellin.normalizedTheta_sub_one_real line 481
  29. lemma OAI.PrimeDegreePackets.HeckeMellin.normalizedTheta_sub_one_re_nonneg line 487
  30. lemma OAI.PrimeDegreePackets.HeckeMellin.norm_normalizedTheta_sub_one line 494
  31. def OAI.PrimeDegreePackets.HeckeMellin.idealThetaMellinKernel line 501
  32. lemma OAI.PrimeDegreePackets.HeckeMellin.measurable_idealThetaMellinKernel line 509
  33. lemma OAI.PrimeDegreePackets.HeckeMellin.norm_idealThetaMellinKernel line 528
  34. lemma OAI.PrimeDegreePackets.HeckeMellin.lintegral_norm_idealThetaMellinKernel line 540
  35. theorem OAI.PrimeDegreePackets.HeckeMellin.integrable_idealThetaMellinKernel line 556