OAI/NumberTheory/Ostmann/ZeroDensity/CharacterZeroPolynomial.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Removing the actual finite zero factors of an entire character L-function

  1. def OAI.Ostmann.characterZeroPolynomial line 12
  2. theorem OAI.Ostmann.characterZeroPolynomial_analytic line 16
  3. theorem OAI.Ostmann.characterZeroPolynomial_ne_zero line 20
  4. theorem OAI.Ostmann.characterZeroPolynomial_insert line 26
  5. theorem OAI.Ostmann.character_remove_finite_zeros line 34

    Source documentation

    The quotient by any finite collection of complete zero factors extends analytically to the whole plane. It is nonzero at each removed zero.

    theorem character_remove_finite_zeros (χ : PrimitiveComplexCharacter) (S : Finset ℂ) :
    ∃ g : ℂ → ℂ, (∀ s, AnalyticAt ℂ g s) ∧
      (∀ s, χ.L s = characterZeroPolynomial χ S s * g s) ∧
      (∀ s ∈ S, g s ≠ 0) := by
…

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