ActualRealZeroExpansion.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Ostmann.actualRealZeroErrorConstant line 12
theorem OAI.Ostmann.actualRealZeroErrorConstant_pos line 14
theorem OAI.Ostmann.real_character_hadamard_error line 18
Source documentation
The exact zero-sum identity has only the bounded archimedean term left over.
```
theorem real_character_hadamard_error (χ : PrimitiveRealCharacter) (s : ℝ)
    (hs : 1 < s) (hs2 : s ≤ 2) :
    |realCharacterZeroSum χ s - χ.logDerivative s - (1 / 2) * Real.log χ.modulus| ≤
      actualRealZeroErrorConstant := by
…
```
Mentions: OAI.Ostmann.PrimitiveRealCharacter, OAI.Ostmann.realCharacterZeroSum, OAI.Ostmann.actualRealZeroErrorConstant
def OAI.Ostmann.actualRealCharacterZeroExpansion line 38
Source documentation
The Hadamard expansion fields of the real-zero input.
```
noncomputable def actualRealCharacterZeroExpansion (χ : PrimitiveRealCharacter) :
    RealCharacterZeroExpansion χ actualRealZeroErrorConstant where
…
```
Mentions: OAI.Ostmann.PrimitiveRealCharacter, OAI.Ostmann.RealCharacterZeroExpansion, OAI.Ostmann.actualRealZeroErrorConstant
def OAI.Ostmann.ActualRealLowHeightRegion line 48
Source documentation
The low-height clause of Montgomery--Vaughan 11.3/11.10, stated for the analytic multiplicity enumeration.
```
def ActualRealLowHeightRegion (P : PublishedProgressionInput) : Prop :=
…
```
Mentions: OAI.Ostmann.PublishedProgressionInput
def OAI.Ostmann.actualPublishedRealZeroInput line 56