OAI/NumberTheory/Ostmann/Characters/CharacterEnumerationCount.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Connecting zero enumerations to actual analytic multiplicities

This is a representation condition: an enumeration may list a zero no more times than its analytic multiplicity. The numerical zero bound itself is proved in CharacterFullZeroCount, not assumed here.

  1. def OAI.Ostmann.ComplexZeroEnumeration.RespectsMultiplicity line 17
  2. theorem OAI.Ostmann.ComplexZeroEnumeration.count_zero_eq_card line 22
  3. theorem OAI.Ostmann.ComplexZeroEnumeration.count_bound_of_multiplicity line 30
  4. def OAI.Ostmann.smoothExplicitFormula_of_multiplicity line 55

    Source documentation

    For multiplicity-respecting enumerations, only the actual explicit formula remains in this analytic package. The zero count, Mellin decay and absolute convergence are all derived.

    noncomputable def smoothExplicitFormula_of_multiplicity {Z : ∀ χ, ComplexZeroEnumeration χ}
    (hZ : ∀ χ, (Z χ).RespectsMultiplicity) (E : ℝ) (hE : 0 < E)
    (hformula : ∀ χ : PrimitiveComplexCharacter, ∀ X : ℝ, 2 ≤ X →
      ‖smoothMangoldtMean χ.modulus χ.character X +
        (∑' i, smoothZeroTerm Z χ X i) + smoothTrivialZeroTerm χ‖ ≤
          E / Real.sqrt X * Real.log (2 * (χ.modulus : ℝ))) :
    PublishedSmoothExplicitFormula Z :=
…

    Mentions: OAI.Ostmann.ComplexZeroEnumeration, OAI.Ostmann.PrimitiveComplexCharacter, OAI.Ostmann.smoothMangoldtMean, OAI.Ostmann.smoothZeroTerm, OAI.Ostmann.smoothTrivialZeroTerm, OAI.Ostmann.PublishedSmoothExplicitFormula