PublishedComplexZeroDensity.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Published zero-density and zero-free inputs for the smooth prime mean

H. L. Montgomery, Zeros of L-functions, Invent. Math. 8 (1969), 346–354, Theorem 1, in the explicit form of S. Inoue, Some explicit formulas for partial sums of Möbius functions, JTNB 33 (2021), 273–315, Lemma 1, p. 282: https://jtnb.centre-mersenne.org/item/10.5802/jtnb.1162.pdf .

The region below is the bounded-height consequence of K. Ford, B. Green, S. Konyagin, J. Maynard and T. Tao, Long gaps between primes, JAMS 31 (2018), 65–105, Lemma 7.1. Deleting the whole exceptional primitive character and replacing Q*(1+|t|) by 2*Q*T only weakens that statement. https://doi.org/10.1090/jams/876 .

These are explicit conditional parameters. The zero enumeration is shared with the explicit-formula input; no smooth-prime-mean estimate is assumed.

structure OAI.Ostmann.PrimitiveComplexCharacter line 26
def OAI.Ostmann.PrimitiveComplexCharacter.L line 33
structure OAI.Ostmann.ComplexZeroEnumeration line 38
Source documentation
A fixed enumeration with multiplicities used by the published density and explicit-formula statements. Bounded ordinate ranges are finite.
```
structure ComplexZeroEnumeration (χ : PrimitiveComplexCharacter) where
…
```
Mentions: OAI.Ostmann.PrimitiveComplexCharacter
def OAI.Ostmann.ComplexZeroEnumeration.heightIndices line 44
theorem OAI.Ostmann.ComplexZeroEnumeration.mem_heightIndices line 47
def OAI.Ostmann.ComplexZeroEnumeration.count line 51
def OAI.Ostmann.PublishedComplexZeroDensity line 57
Source documentation
The exact Montgomery–Inoue estimate, restricted to an arbitrary finite subfamily of the primitive nonprincipal characters of conductor at most Q.
```
def PublishedComplexZeroDensity (Z : ∀ χ, ComplexZeroEnumeration χ) : Prop :=
…
```
Mentions: OAI.Ostmann.ComplexZeroEnumeration
def OAI.Ostmann.PublishedComplexZeroRegion line 67
Source documentation
Bounded-height Landau–Page, with the entire possible exceptional character removed. The exception can be avoided by one prime deletion.
```
def PublishedComplexZeroRegion (Z : ∀ χ, ComplexZeroEnumeration χ) : Prop :=
…
```
Mentions: OAI.Ostmann.ComplexZeroEnumeration