OAI/NumberTheory/Ostmann/Characters/CharacterLogDerivativeLocal.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.characterZeroPolynomial_logDeriv line 12
2. theorem OAI.Ostmann.character_logDeriv_local_error line 31

   Source documentation

   Away from the actual nearby zeros, L'/L differs from their partial fractions by a controlled analytic term. No zero-separation assumption enters this term.

   theorem character_logDeriv_local_error (χ : PrimitiveComplexCharacter) (t M : ℝ)
       (hM : 1 ≤ M)
       (hbound : ∀ z ∈ closedBall (characterZeroCenter t) (11 / 4 : ℝ), ‖χ.L z‖ ≤ M)
       (s : ℂ) (hs : ‖s - characterZeroCenter t‖ ≤ 5 / 2)
       (hszero : s ∉ characterContourZeros χ t) :
       ‖logDeriv χ.L s -
         ∑ z ∈ characterContourZeros χ t, (analyticOrderNatAt χ.L z : ℂ) / (s - z)‖ ≤
         1312 * (Real.log (3 * M) +
           (∑ z ∈ characterContourZeros χ t, (analyticOrderNatAt χ.L z : ℝ)) * Real.log 21 + 1) := by
   …

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