MRTCofactorMean.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A mean-square bound for the actual fixed-window cofactor polynomial. The reciprocal-count weight is a contraction, so this estimate is uniform in all remaining typical-factorization masks.

lemma OAI.TwoPointCorrelations.mrt_cofactor_exponential_polynomial line 14
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTCofactorMean.lean:14 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_reciprocal_count_oneBounded line 28
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTCofactorMean.lean:28 (same declaration text).
theorem OAI.TwoPointCorrelations.mrt_cofactor_mean_square line 38
Source documentation
The usual cofactor mean square, with its actual length N/a. Neither the number nor the sizes of other prime bands enter the constant.
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTCofactorMean.lean:38 (same declaration text).
```
theorem mrt_cofactor_mean_square (P : Finset ℕ) (F : ℕ → ℂ)
    (hF : OneBounded F) (N : ℕ) {a : ℝ} (ha : 1 ≤ a)
    (hx : 2 ≤ (N : ℝ) / a) {T : ℝ} (hT : 0 < T) :
    (∫ t in -T..T, ‖mrtCofactorPolynomial P F N a t‖ ^ 2) ≤
      32 * Real.exp 1 * (T * a / (N : ℝ) + 1) := by
…
```
Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtCofactorPolynomial