SmoothMellinBounds.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform Mellin decay of the fixed test in the required strip

theorem OAI.Ostmann.shiftedPrimeMeanMellin_product line 12
theorem OAI.Ostmann.shiftedPrimeMeanMellin_norm_bound line 23
Source documentation
All shifted integrals needed below have a uniform bound on the fixed half-unit interval. The power of t is bounded using only Re(s) >= -1/2.
```
theorem shiftedPrimeMeanMellin_norm_bound (n : ℕ) (s : ℂ) (D : ℝ)
    (hD : 0 ≤ D) (hd : ∀ t : ℝ, |iteratedDeriv n primeMeanTest t| ≤ D)
    (hs : -(1 / 2 : ℝ) ≤ s.re) :
    ‖shiftedPrimeMeanMellin n s‖ ≤ 4 * D := by
…
```
Mentions: OAI.Ostmann.primeMeanTest, OAI.Ostmann.shiftedPrimeMeanMellin
theorem OAI.Ostmann.primeMeanMellin_height_bound line 61
Source documentation
The product introduced by eight integrations by parts controls the imaginary height without excluding real s.
```
theorem primeMeanMellin_height_bound (s : ℂ) (D : ℝ) (hD : 0 ≤ D)
    (hd : ∀ t : ℝ, |iteratedDeriv 8 primeMeanTest t| ≤ D)
    (hs : -(1 / 2 : ℝ) ≤ s.re) :
    |s.im| ^ 8 * ‖primeMeanMellin s‖ ≤ 4 * D := by
…
```
Mentions: OAI.Ostmann.primeMeanTest, OAI.Ostmann.primeMeanMellin
theorem OAI.Ostmann.primeMeanMellin_decay line 82
Source documentation
The precise eighth-order decay field needed in the published explicit formula structure is unconditional for the actual fixed test.
```
theorem primeMeanMellin_decay : ∃ C : ℝ, 0 < C ∧
    ∀ s : ℂ, -(1 / 2 : ℝ) ≤ s.re → s.re ≤ 2 →
      ‖primeMeanMellin s‖ ≤ C * Real.exp (-8 * Real.log (1 + |s.im|)) := by
…
```
Mentions: OAI.Ostmann.primeMeanMellin