ModFivePsiDecay.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Removal of the nonintegral-cutoff condition. The Mangoldt sums only depend on the floor; the midpoint of the same unit interval is always an admissible triangular cutoff.

lemma OAI.TwoPointCorrelations.modFive_half_cutoff_nonnat line 13
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePsiDecay.lean:13 (same declaration text).
lemma OAI.TwoPointCorrelations.modFive_half_cutoff_floor line 20
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePsiDecay.lean:20 (same declaration text).
lemma OAI.TwoPointCorrelations.modFive_half_cutoff_geometry line 25
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePsiDecay.lean:25 (same declaration text).
theorem OAI.TwoPointCorrelations.modFive_nonprincipal_psi_decay line 54
Source documentation
The full real-cutoff estimate for every nonprincipal character mod 5.
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePsiDecay.lean:54 (same declaration text).
```
theorem modFive_nonprincipal_psi_decay : ∃ c : ℝ, 0 < c ∧
    ∀ᶠ x : ℝ in atTop, ∀ χ : DirichletCharacter ℂ 5, χ ≠ 1 →
      ‖modFiveTwistedPsi χ x‖ ≤ 2 * x * Real.exp (-c * Real.sqrt (Real.log x)) := by
…
```
Mentions: OAI.TwoPointCorrelations.modFiveTwistedPsi