ModFiveSmoothedDecay.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Exponential decay for the actual triangularly smoothed nonprincipal Mangoldt sums, obtained by the explicit Perron height exp(sqrt(log x)).

lemma OAI.TwoPointCorrelations.modFive_contour_parameter_bound line 13
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveSmoothedDecay.lean:13 (same declaration text).

theorem OAI.TwoPointCorrelations.modFive_smoothed_decay_exp_square line 74

Source documentation

Uniform over the three nonprincipal characters.

Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveSmoothedDecay.lean:74 (same declaration text).

theorem modFive_smoothed_decay_exp_square : ∃ c : ℝ, 0 < c ∧
    ∀ᶠ y : ℝ in atTop, ∀ χ : DirichletCharacter ℂ 5, χ ≠ 1 →
      (∀ n : ℕ, Real.exp (y ^ 2) ≠ (n : ℝ)) →
      ‖modFiveSmoothedPsi χ (Real.exp (y ^ 2))‖ ≤ Real.exp (y ^ 2 - c * y) := by
…

Mentions: OAI.TwoPointCorrelations.modFiveSmoothedPsi

theorem OAI.TwoPointCorrelations.modFive_smoothed_decay line 105
Source documentation
The original real-cutoff form of the smoothed prime estimate.
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveSmoothedDecay.lean:105 (same declaration text).
```
theorem modFive_smoothed_decay : ∃ c : ℝ, 0 < c ∧
    ∀ᶠ x : ℝ in atTop, ∀ χ : DirichletCharacter ℂ 5, χ ≠ 1 →
      (∀ n : ℕ, x ≠ (n : ℝ)) →
      ‖modFiveSmoothedPsi χ x‖ ≤ x * Real.exp (-c * Real.sqrt (Real.log x)) := by
…
```
Mentions: OAI.TwoPointCorrelations.modFiveSmoothedPsi