PublishedRealZeros.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Published inputs for the real-character zero argument

The Hadamard input is the real-axis specialization of H. A. Helfgott, The ternary Goldbach problem, Part I, 15 December 2019, section 3.7.4, equations (3.97)--(3.102), printed pp. 86--87: https://webusers.imj-prg.fr/~harald.helfgott/anglais/PartI.pdf . The bounded gamma term on 1 < s <= 2 is included in the absolute constant.

The low-height region and single simple exception are H. L. Montgomery and R. C. Vaughan, Multiplicative Number Theory I, Theorem 11.3 and Corollary 11.10, pp. 360 and 369, using the same decreased constant as PublishedProgressionInput. The separate Siegel specialization is Corollary 11.15 of that book. All these are explicit conditional parameters.

structure OAI.Ostmann.PrimitiveRealCharacter line 26
def OAI.Ostmann.PrimitiveRealCharacter.complexCharacter line 33
def OAI.Ostmann.PrimitiveRealCharacter.L line 36
def OAI.Ostmann.PrimitiveRealCharacter.logDerivative line 39
structure OAI.Ostmann.RealCharacterZeroExpansion line 44
Source documentation
A genuine zero sequence, indexed with multiplicities. The Hadamard identity specifies its sum; no downstream prime-mass bound is included.
```
structure RealCharacterZeroExpansion (χ : PrimitiveRealCharacter) (C : ℝ) where
…
```
Mentions: OAI.Ostmann.PrimitiveRealCharacter
structure OAI.Ostmann.PublishedRealZeroInput line 56
Source documentation
Hadamard factorization and the full low-height zero-free region. Page uniqueness for the resulting actual real zeros is already in P.
```
structure PublishedRealZeroInput (P : PublishedProgressionInput) where
…
```
Mentions: OAI.Ostmann.PublishedProgressionInput
def OAI.Ostmann.PublishedSiegelBound line 69
Source documentation
The one-sided real-zero consequence of Siegel's theorem, for every fixed positive exponent. Its constant is allowed to be ineffective.
```
def PublishedSiegelBound : Prop :=
…
```
def OAI.Ostmann.RealCharacterZeroExpansion.realZero line 73