OAI/NumberTheory/Ostmann/ZeroDensity/CharacterZeroCopies.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual zero set with multiplicity labels

Each copy is a genuine zero together with an integer smaller than its analytic order. Any bijective numbering of these copies automatically has the correct multiplicity bound and finite bounded-height ranges.

  1. abbrev OAI.Ostmann.CharacterZeroCopy line 17
  2. theorem OAI.Ostmann.characterZeroCopy_finite_height line 20
  3. def OAI.Ostmann.characterZeroEnumeration line 31
  4. theorem OAI.Ostmann.characterZeroEnumeration_respectsMultiplicity line 39
  5. theorem OAI.Ostmann.characterZeroEnumeration_complete line 56

    Source documentation

    Every genuine zero and every one of its multiplicity labels occurs once.

    theorem characterZeroEnumeration_complete (χ : PrimitiveComplexCharacter)
    (e : ℕ ≃ CharacterZeroCopy χ) (z : ℂ) (hz : z ∈ complexCharacterZeros χ)
    (k : ℕ) (hk : k < analyticOrderNatAt χ.L z) :
    ∃! i : ℕ, (e i).val = (z, k) := by
…

    Mentions: OAI.Ostmann.PrimitiveComplexCharacter, OAI.Ostmann.CharacterZeroCopy, OAI.Ostmann.complexCharacterZeros