CharacterZeroQuotientBound.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Modulus bounds after removing the finite zero factors

theorem OAI.Ostmann.characterZeroPolynomial_norm_le line 13
theorem OAI.Ostmann.characterZeroPolynomial_norm_ge line 21

theorem OAI.Ostmann.character_contour_quotient_exists line 30

Source documentation

The removed quotient is nonvanishing on the whole smaller disk.

theorem character_contour_quotient_exists (χ : PrimitiveComplexCharacter) (t : ℝ) :
    ∃ g : ℂ → ℂ, (∀ s, AnalyticAt ℂ g s) ∧
      (∀ s, χ.L s = characterZeroPolynomial χ (characterContourZeros χ t) s * g s) ∧
      (∀ s ∈ closedBall (characterZeroCenter t) (21 / 8 : ℝ), g s ≠ 0) := by
…

Mentions: OAI.Ostmann.PrimitiveComplexCharacter, OAI.Ostmann.characterZeroPolynomial, OAI.Ostmann.characterContourZeros, OAI.Ostmann.characterZeroCenter

theorem OAI.Ostmann.character_contour_quotient_bound line 45

Source documentation

A fixed annular reserve bounds the analytic quotient throughout the outer disk, even when the original L-function vanishes inside it.

theorem character_contour_quotient_bound (χ : PrimitiveComplexCharacter) (t M : ℝ)
    (_hM : 0 ≤ M)
    (hbound : ∀ z ∈ closedBall (characterZeroCenter t) (11 / 4 : ℝ), ‖χ.L z‖ ≤ M)
    (g : ℂ → ℂ) (hg : ∀ s, AnalyticAt ℂ g s)
    (he : ∀ s, χ.L s = characterZeroPolynomial χ (characterContourZeros χ t) s * g s) :
    ∀ z ∈ closedBall (characterZeroCenter t) (11 / 4 : ℝ),
      ‖g z‖ ≤ M * 8 ^ (∑ w ∈ characterContourZeros χ t, analyticOrderNatAt χ.L w) := by
…

Mentions: OAI.Ostmann.PrimitiveComplexCharacter, OAI.Ostmann.characterZeroCenter, OAI.Ostmann.characterZeroPolynomial, OAI.Ostmann.characterContourZeros