MRTDyadicMeanSquare.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The normalized dyadic Dirichlet-polynomial mean-value estimate used in corrected MRT Appendix A. The coefficient bound is completely arbitrary.

theorem OAI.TwoPointCorrelations.mrt_dirichlet_mean_square_subset line 14
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTDyadicMeanSquare.lean:14 (same declaration text).
def OAI.TwoPointCorrelations.mrtDyadicPolynomial line 44
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTDyadicMeanSquare.lean:44 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_line_one_term line 48
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTDyadicMeanSquare.lean:48 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtDyadicPolynomial_eq_LSeries line 61
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTDyadicMeanSquare.lean:61 (same declaration text).
theorem OAI.TwoPointCorrelations.mrt_dyadic_mean_square line 71
Source documentation
On the line Re(s)=1, a one-bounded dyadic polynomial has mean square O(T/N+1), with the absolute constant 16e.
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTDyadicMeanSquare.lean:71 (same declaration text).
```
theorem mrt_dyadic_mean_square (b : ℕ → ℂ) {N : ℕ} (hN : 0 < N)
    (hb : ∀ n ∈ Ioc N (2 * N), ‖b n‖ ≤ 1) {T : ℝ} (hT : 0 < T) :
    (∫ t in -T..T, ‖mrtDyadicPolynomial b N t‖ ^ 2) ≤
      16 * Real.exp 1 * (T / (N : ℝ) + 1) := by
…
```
Mentions: OAI.TwoPointCorrelations.mrtDyadicPolynomial