OAI/NumberTheory/DirichletL/Detector/MellinBoundary.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.ProbeMellinBoundary.height line 14
  2. lemma OAI.SevenEighths.ProbeMellinBoundary.height_pos line 15
  3. lemma OAI.SevenEighths.ProbeMellinBoundary.height_one_le line 16
  4. def OAI.SevenEighths.ProbeMellinBoundary.cauchy line 18
  5. lemma OAI.SevenEighths.ProbeMellinBoundary.cauchy_nonneg line 19
  6. lemma OAI.SevenEighths.ProbeMellinBoundary.cauchy_integrable line 20
  7. lemma OAI.SevenEighths.ProbeMellinBoundary.cauchy_tendsto line 21
  8. theorem OAI.SevenEighths.ProbeMellinBoundary.boundaryControl_of_cauchy line 25
  9. lemma OAI.SevenEighths.ProbeMellinBoundary.pole_distance_vertical line 54
  10. lemma OAI.SevenEighths.ProbeMellinBoundary.pole_distance_horizontal line 56
  11. theorem OAI.SevenEighths.ProbeMellinBoundary.boundaryControl_of_pole_product line 59
  12. def OAI.SevenEighths.ProbeMellinBoundary.scaleBound line 106
  13. lemma OAI.SevenEighths.ProbeMellinBoundary.scaleBound_pos line 107
  14. lemma OAI.SevenEighths.ProbeMellinBoundary.rpow_le_scaleBound line 108
  15. lemma OAI.SevenEighths.ProbeMellinBoundary.cpow_le_scaleBound line 115
  16. def OAI.SevenEighths.ProbeMellinBoundary.wScalar line 120
  17. theorem OAI.SevenEighths.ProbeMellinBoundary.source_w_boundary line 124
  18. lemma OAI.SevenEighths.ProbeMellinBoundary.gaussian_strip_norm_le line 187
  19. def OAI.SevenEighths.ProbeMellinBoundary.zScalar line 202
  20. def OAI.SevenEighths.ProbeMellinBoundary.zScaleBound line 205
  21. lemma OAI.SevenEighths.ProbeMellinBoundary.zScalar_continuous line 209
  22. lemma OAI.SevenEighths.ProbeMellinBoundary.zScalar_norm_le line 221
  23. theorem OAI.SevenEighths.ProbeMellinBoundary.source_z_boundary line 242
  24. def OAI.SevenEighths.ProbeMellinBoundary.profile line 315
  25. def OAI.SevenEighths.ProbeMellinBoundary.jointHeight line 318
  26. lemma OAI.SevenEighths.ProbeMellinBoundary.jointHeight_pos line 319
  27. def OAI.SevenEighths.ProbeMellinBoundary.gaussianMoment line 321
  28. lemma OAI.SevenEighths.ProbeMellinBoundary.gaussianMoment_nonneg line 322
  29. lemma OAI.SevenEighths.ProbeMellinBoundary.gaussianMoment_integrable line 325
  30. lemma OAI.SevenEighths.ProbeMellinBoundary.height_sub_le line 336
  31. lemma OAI.SevenEighths.ProbeMellinBoundary.jointHeight_le_shear line 342
  32. lemma OAI.SevenEighths.ProbeMellinBoundary.weighted_to_cauchy line 359
  33. lemma OAI.SevenEighths.ProbeMellinBoundary.weighted_coupled_cauchy line 366
  34. abbrev OAI.SevenEighths.ProbeMellinBoundary.HeightSpace line 388
  35. abbrev OAI.SevenEighths.ProbeMellinBoundary.heightMeasure line 389
  36. def OAI.SevenEighths.ProbeMellinBoundary.jointEnvelope line 391
  37. lemma OAI.SevenEighths.ProbeMellinBoundary.jointEnvelope_nonneg line 394
  38. lemma OAI.SevenEighths.ProbeMellinBoundary.jointEnvelope_integrable line 397
  39. def OAI.SevenEighths.ProbeMellinBoundary.onLines line 408
  40. lemma OAI.SevenEighths.ProbeMellinBoundary.onLines_norm line 411
  41. lemma OAI.SevenEighths.ProbeMellinBoundary.onLines_continuous line 421
  42. def OAI.SevenEighths.ProbeMellinBoundary.realGaussianBound line 436
  43. lemma OAI.SevenEighths.ProbeMellinBoundary.realGaussianBound_pos line 438
  44. lemma OAI.SevenEighths.ProbeMellinBoundary.realGaussian_le line 440
  45. lemma OAI.SevenEighths.ProbeMellinBoundary.profile_moment_majorant line 455
  46. theorem OAI.SevenEighths.ProbeMellinBoundary.profile_uniform_moments line 477
  47. def OAI.SevenEighths.ProbeMellinBoundary.outsideBox line 515
  48. lemma OAI.SevenEighths.ProbeMellinBoundary.outsideBox_measurable line 517
  49. lemma OAI.SevenEighths.ProbeMellinBoundary.height_le_joint_on_tail line 520
  50. lemma OAI.SevenEighths.ProbeMellinBoundary.weighted_tail_pointwise line 525
  51. theorem OAI.SevenEighths.ProbeMellinBoundary.profile_uniform_tails line 535
  52. theorem OAI.SevenEighths.ProbeMellinBoundary.profile_arithmetic_integrable line 567
  53. inductive OAI.SevenEighths.ProbeMellinBoundary.SliceAxis line 583
  54. def OAI.SevenEighths.ProbeMellinBoundary.sliceMap line 586
  55. lemma OAI.SevenEighths.ProbeMellinBoundary.sliceMap_continuous line 592
  56. lemma OAI.SevenEighths.ProbeMellinBoundary.slice_height_le line 595
  57. lemma OAI.SevenEighths.ProbeMellinBoundary.cauchy_le_one line 600
  58. def OAI.SevenEighths.ProbeMellinBoundary.sliceEnvelope line 604
  59. def OAI.SevenEighths.ProbeMellinBoundary.sliceMass line 609
  60. lemma OAI.SevenEighths.ProbeMellinBoundary.sliceEnvelope_nonneg line 611
  61. lemma OAI.SevenEighths.ProbeMellinBoundary.jointEnvelope_slice_le line 615
  62. lemma OAI.SevenEighths.ProbeMellinBoundary.pairEnvelope_integrable line 630
  63. lemma OAI.SevenEighths.ProbeMellinBoundary.sliceEnvelope_integrable line 638
  64. lemma OAI.SevenEighths.ProbeMellinBoundary.sliceEnvelope_integral line 645
  65. lemma OAI.SevenEighths.ProbeMellinBoundary.weighted_slice_pointwise line 659
  66. theorem OAI.SevenEighths.ProbeMellinBoundary.profile_uniform_slices line 671
  67. theorem OAI.SevenEighths.ProbeMellinBoundary.profile_arithmetic_tails line 725
  68. theorem OAI.SevenEighths.ProbeMellinBoundary.profile_arithmetic_slices line 761
  69. theorem OAI.SevenEighths.ProbeMellinBoundary.profile_arithmetic_fubini line 802