HadamardPrimeBound.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Deriving signed prime-mass bounds from the published zero expansion

theorem OAI.Ostmann.realCharacterZeroExpansion_anchor line 12

theorem OAI.Ostmann.exists_signed_prime_lower_of_zero_sum line 22

Source documentation

The bounded Euler prime-power error has already been proved. Only the Hadamard expansion remains an input to this implication.

theorem exists_signed_prime_lower_of_zero_sum :
    ∃ A : ℝ, 0 ≤ A ∧ ∀ (χ : PrimitiveRealCharacter) (C : ℝ)
      (Z : RealCharacterZeroExpansion χ C) (s B : ℝ), 1 < s → s ≤ 2 →
      (∑' i, realZeroKernel (s - (Z.zeros i).re) (Z.zeros i).im) ≤ B →
      -B - C - A ≤ ∑' n, realPrimeTerm χ.character s n := by
…

Mentions: OAI.Ostmann.PrimitiveRealCharacter, OAI.Ostmann.RealCharacterZeroExpansion, OAI.Ostmann.realZeroKernel, OAI.Ostmann.realPrimeTerm

theorem OAI.Ostmann.exceptional_zero_sum_bound line 42

Source documentation

Actual real exceptions in a finite zero family cost at most one Siegel term when the region has at most one exceptional zero.

theorem exceptional_zero_sum_bound (hSiegel : PublishedSiegelBound)
    (ε : ℝ) (hε : 0 < ε) : ∃ K : ℝ, 0 < K ∧
    ∀ (χ : PrimitiveRealCharacter) (C : ℝ) (Z : RealCharacterZeroExpansion χ C)
      (E : Finset ℕ) (s : ℝ), E.card ≤ 1 → 1 < s →
      (∀ i ∈ E, (Z.zeros i).im = 0) →
      (∑ i ∈ E, (s - (Z.zeros i).re)⁻¹) ≤ K * (χ.modulus : ℝ) ^ ε := by
…

Mentions: OAI.Ostmann.PublishedSiegelBound, OAI.Ostmann.PrimitiveRealCharacter, OAI.Ostmann.RealCharacterZeroExpansion