PublishedProgressionInputs.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Precisely stated published inputs for primes in progressions

Reference: H. L. Montgomery and R. C. Vaughan, Multiplicative Number Theory I: Classical Theory, Cambridge Studies in Advanced Mathematics 97, Chapter 11, DOI 10.1017/CBO9780511618314.013.

PublishedProgressionInput.theta is Corollary 11.20, equations (11.32) and (11.34), p. 381. complete specifies the exceptional zero in Theorem 11.3, p. 360. unique is the real-zero specialization of Corollary 11.10 (Page), p. 369. The positive zero-free constant can be decreased so these use one constant and the harmless denominator log (4*q) throughout.

These are explicit conditional inputs. In particular, no logarithmic interval estimate or arithmetic comparison is assumed here.

structure OAI.Ostmann.PrimitiveRealZero line 27
Source documentation
An actual primitive real character and an actual zero of its continued Dirichlet L-function, rather than an unrestricted correction coefficient.
```
structure PrimitiveRealZero where
…
```
def OAI.Ostmann.pageCoefficient line 39
def OAI.Ostmann.pageBeta line 44
theorem OAI.Ostmann.pageCoefficient_abs_le_one line 49
theorem OAI.Ostmann.pageBeta_pos line 55
theorem OAI.Ostmann.pageBeta_le_one line 60
structure OAI.Ostmann.PublishedProgressionInput line 67
Source documentation
The restricted classical analytic input. The family chooses the local exceptional primitive character, if one exists, for each modulus.
```
structure PublishedProgressionInput where
…
```

theorem OAI.Ostmann.PublishedProgressionInput.local_log_interval line 93

Source documentation

The logarithmic prime estimate is derived by partial summation; it is not included among the published assumptions.

theorem PublishedProgressionInput.local_log_interval (P : PublishedProgressionInput)
    (q a : ℕ) (hq : 1 ≤ q) (ha : a.Coprime q) {s t : ℝ}
    (hs : 1 ≤ s) (hst : s ≤ t) (hshort : t ≤ s + 1) :
    |reciprocalPrimeInterval q a (Real.exp s) (Real.exp t) -
      ∫ y in Set.Ioc s t, primeLogDensity (Nat.totient q)
        (pageCoefficient (P.localZero q) a) (pageBeta (P.localZero q)) y| ≤
      18 * P.errorConstant * Real.exp (-P.decay * Real.sqrt s) := by
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.reciprocalPrimeInterval, OAI.Ostmann.primeLogDensity, OAI.Ostmann.pageCoefficient, OAI.Ostmann.pageBeta