OAI/NumberTheory/Ostmann/ZeroDensity/SmoothExplicitFormulaCore.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Removing the elementary fields of the smooth explicit-formula input

The analytic input is only the zero count and fixed-test explicit formula. The Mellin decay and absolute summability are derived for the actual test.

  1. structure OAI.Ostmann.SmoothExplicitFormulaCore line 20

    Source documentation

    The fixed-test explicit formula.

    structure SmoothExplicitFormulaCore (Z : ∀ χ, ComplexZeroEnumeration χ) where
…

    Mentions: OAI.Ostmann.ComplexZeroEnumeration

  2. theorem OAI.Ostmann.SmoothExplicitFormulaCore.finite_height_count line 34
  3. theorem OAI.Ostmann.smoothZeroTerm_bound_of_mellin line 53
  4. theorem OAI.Ostmann.SmoothExplicitFormulaCore.absolute_summability line 75
  5. def OAI.Ostmann.SmoothExplicitFormulaCore.toPublished line 96