MRTMeanSquareKernel.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exponential majorant for Dirichlet-polynomial mean squares

This is the elementary kernel behind the mean-value estimate used at the start of corrected MRT, Appendix A, Proposition A.3. Its Fourier transform has quadratic decay, so the ensuing row sum loses no logarithm.

def OAI.TwoPointCorrelations.mrtMeanSquareKernel line 19
Source documentation
The integrable exponential time weight, with angular frequency ω.
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTMeanSquareKernel.lean:19 (same declaration text).
```
noncomputable def mrtMeanSquareKernel (T ω t : ℝ) : ℂ :=
…
```
lemma OAI.TwoPointCorrelations.mrtMeanSquareKernel_right line 22
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTMeanSquareKernel.lean:22 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtMeanSquareKernel_left line 31
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTMeanSquareKernel.lean:31 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtMeanSquareKernel_integrable line 40
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTMeanSquareKernel.lean:40 (same declaration text).
theorem OAI.TwoPointCorrelations.integral_mrtMeanSquareKernel line 57
Source documentation
Exact quadratic-decay Fourier transform, without an asymptotic constant.
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTMeanSquareKernel.lean:57 (same declaration text).
```
theorem integral_mrtMeanSquareKernel {T : ℝ} (hT : 0 < T) (ω : ℝ) :
    (∫ t : ℝ, mrtMeanSquareKernel T ω t) =
      ((2 * T / (1 + T ^ 2 * ω ^ 2) : ℝ) : ℂ) := by
…
```
Mentions: OAI.TwoPointCorrelations.mrtMeanSquareKernel