ModFiveUnsmoothing.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Exact finite differences for the triangularly smoothed Mangoldt sum. The error is confined to the short interval at the upper endpoint.

lemma OAI.TwoPointCorrelations.modFive_smoothed_scale line 14
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveUnsmoothing.lean:14 (same declaration text).
lemma OAI.TwoPointCorrelations.modFive_smoothed_difference line 24
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveUnsmoothing.lean:24 (same declaration text).
lemma OAI.TwoPointCorrelations.modFive_mangoldt_norm_le_log line 53
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveUnsmoothing.lean:53 (same declaration text).
lemma OAI.TwoPointCorrelations.modFive_smoothed_remainder line 59
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveUnsmoothing.lean:59 (same declaration text).
lemma OAI.TwoPointCorrelations.modFive_twistedPsi_sum line 92
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveUnsmoothing.lean:92 (same declaration text).
theorem OAI.TwoPointCorrelations.modFive_unsmoothing_bound line 116
Source documentation
A completely finite unsmoothing inequality, with the short-interval cost bounded only by the elementary Mangoldt estimate Λ(n)≤log n.
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveUnsmoothing.lean:116 (same declaration text).
```
theorem modFive_unsmoothing_bound (χ : DirichletCharacter ℂ 5) {x : ℝ}
    (hx : 0 < x) {m : ℕ} (hm : 0 < m) :
    ‖modFiveTwistedPsi χ x‖ ≤
      ((x + m) * ‖modFiveSmoothedPsi χ (x + m)‖ +
        x * ‖modFiveSmoothedPsi χ x‖ + (m : ℝ) ^ 2 * Real.log (x + m)) / m := by
…
```
Mentions: OAI.TwoPointCorrelations.modFiveTwistedPsi, OAI.TwoPointCorrelations.modFiveSmoothedPsi