ModFiveUnsmoothingScale.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The finite-difference step with the actual short interval length. A ceiling is used so that both triangular cutoffs have the same fractional part, and the resulting exponential saving only loses a fixed factor.

lemma OAI.TwoPointCorrelations.modFive_nonnat_add line 14
Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveUnsmoothingScale.lean:14 (same declaration text).
lemma OAI.TwoPointCorrelations.modFive_unsmoothing_numeric line 23
Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveUnsmoothingScale.lean:23 (same declaration text).
lemma OAI.TwoPointCorrelations.modFive_unsmoothing_scale line 90
Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveUnsmoothingScale.lean:90 (same declaration text).
theorem OAI.TwoPointCorrelations.modFive_unsmoothed_decay_nonnat line 126
Source documentation
The nonprincipal twisted Mangoldt sum has a quantitative exponential saving. Nonintegral cutoffs suffice here and are removed by floor transfer.
Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveUnsmoothingScale.lean:126 (same declaration text).
```
theorem modFive_unsmoothed_decay_nonnat : ∃ c : ℝ, 0 < c ∧
    ∀ᶠ x : ℝ in atTop, ∀ χ : DirichletCharacter ℂ 5, χ ≠ 1 →
      (∀ n : ℕ, x ≠ (n : ℝ)) →
      ‖modFiveTwistedPsi χ x‖ ≤ x * Real.exp (-c * Real.sqrt (Real.log x)) := by
…
```
Mentions: OAI.TwoPointCorrelations.modFiveTwistedPsi