MRTMeanSquareRows.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Summable quadratic-gap bounds for the MRT Dirichlet mean-value estimate.

lemma OAI.TwoPointCorrelations.mrt_log_gap line 16
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTMeanSquareRows.lean:16 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_quadratic_gap_sum line 28
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTMeanSquareRows.lean:28 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_nat_distance_sum line 86
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTMeanSquareRows.lean:86 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_log_nat_gap line 153
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTMeanSquareRows.lean:153 (same declaration text).
theorem OAI.TwoPointCorrelations.mrt_logarithmic_kernel_row line 168
Source documentation
The actual logarithmic-frequency kernel has row sum O(T+N).
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTMeanSquareRows.lean:168 (same declaration text).
```
theorem mrt_logarithmic_kernel_row {T : ℝ} (hT : 0 < T) {N m : ℕ}
    (hm : m ∈ Ioc 0 N) :
    (∑ n ∈ Ioc 0 N,
      2 * T / (1 + T ^ 2 * (Real.log (m : ℝ) - Real.log (n : ℝ)) ^ 2)) ≤
      8 * (T + (N : ℝ)) := by
…
```