MRTRamareMeanError.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The actual coefficient error made by replacing the corrected Ramaré denominator with ω_P(m)+1. The pointwise error is supported on prime squares, so the preceding second-moment count applies directly.

def OAI.TwoPointCorrelations.mrtRamareCorrection line 14
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTRamareMeanError.lean:14 (same declaration text).
theorem OAI.TwoPointCorrelations.mrt_ramare_correction_bound line 19
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTRamareMeanError.lean:19 (same declaration text).
theorem OAI.TwoPointCorrelations.mrt_ramare_correction_oneBounded line 46
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTRamareMeanError.lean:46 (same declaration text).
theorem OAI.TwoPointCorrelations.mrt_ramare_correction_mean_square line 57
Source documentation
The literal denominator correction costs only the reciprocal square mass in the normalized dyadic mean square. Multiplicativity is not needed for this error estimate.
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTRamareMeanError.lean:57 (same declaration text).
```
theorem mrt_ramare_correction_mean_square (P : Finset ℕ)
    (hP : ∀ p ∈ P, p.Prime) (F : ℕ → ℂ) (hF : OneBounded F)
    {N : ℕ} (hN : 0 < N) {T : ℝ} (hT : 0 < T) :
    (∫ t in -T..T, ‖mrtDyadicPolynomial (mrtRamareCorrection P F) N t‖ ^ 2) ≤
      32 * Real.exp 1 * (T / (N : ℝ) + 1) *
        ((∑ p ∈ P, 1 / (p : ℝ) ^ 2) + (∑ p ∈ P, 1 / (p : ℝ) ^ 2) ^ 2) := by
…
```
Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtDyadicPolynomial, OAI.TwoPointCorrelations.mrtRamareCorrection