OAI/NumberTheory/Ostmann/Characters/CharacterLogDerivativePole.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The exact local poles of a character logarithmic derivative

  1. theorem OAI.Ostmann.PrimitiveComplexCharacter.logDeriv_local_split line 14

    Source documentation

    Removing the actual analytic zero order leaves a nonvanishing analytic factor.

    theorem PrimitiveComplexCharacter.logDeriv_local_split (χ : PrimitiveComplexCharacter)
    (z : ℂ) : ∃ g : ℂ → ℂ, AnalyticAt ℂ g z ∧ g z ≠ 0 ∧
      logDeriv χ.L =ᶠ[𝓝[≠] z] fun w =>
        (analyticOrderNatAt χ.L z : ℂ) / (w - z) + logDeriv g w := by
…

    Mentions: OAI.Ostmann.PrimitiveComplexCharacter

  2. theorem OAI.Ostmann.PrimitiveComplexCharacter.logDeriv_residue_limit line 40

    Source documentation

    The residue of L'/L at any point is its actual zero multiplicity.

    theorem PrimitiveComplexCharacter.logDeriv_residue_limit (χ : PrimitiveComplexCharacter)
    (z : ℂ) : Tendsto (fun w => (w - z) * logDeriv χ.L w) (𝓝[≠] z)
      (𝓝 (analyticOrderNatAt χ.L z : ℂ)) := by
…

    Mentions: OAI.Ostmann.PrimitiveComplexCharacter