OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFourierCauchy.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The exact Cauchy Fourier kernel follows by Fourier inversion from the exponential transform already used in the mean-square bound.

  1. def OAI.TwoPointCorrelations.mrtLaplaceWeight line 14
  2. lemma OAI.TwoPointCorrelations.mrtLaplaceWeight_integrable line 16
  3. lemma OAI.TwoPointCorrelations.mrtLaplaceWeight_continuous line 21
  4. theorem OAI.TwoPointCorrelations.mrt_laplace_fourier line 25
  5. lemma OAI.TwoPointCorrelations.mrtLaplaceWeight_fourier_integrable line 41
  6. def OAI.TwoPointCorrelations.mrtCauchyKernel line 49
  7. lemma OAI.TwoPointCorrelations.mrtCauchyKernel_integrable line 52
  8. theorem OAI.TwoPointCorrelations.integral_mrtCauchyKernel line 63