SmoothZeroCountFamily.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The ordinary individual zero count supplies the family count

theorem OAI.Ostmann.family_zero_count_of_individual line 13

def OAI.Ostmann.smoothExplicitFormula_of_individual line 40

Source documentation

Only the ordinary individual count and the explicit formula are needed. The family count, Mellin decay and absolute convergence are already proved.

noncomputable def smoothExplicitFormula_of_individual {Z : ∀ χ, ComplexZeroEnumeration χ}
    (E C : ℝ) (hE : 0 < E) (hC : 0 < C)
    (hcount : ∀ χ : PrimitiveComplexCharacter, ∀ T : ℝ, 0 ≤ T →
      ((Z χ).count 0 T : ℝ) ≤ C * (T + 1) * Real.log ((χ.modulus : ℝ) * (T + 2)))
    (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