OAI/NumberTheory/Ostmann/ZeroDensity/RealZeroKernel.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Comparing the real parts of zero contributions at two real points

  1. def OAI.Ostmann.realZeroKernel line 12
  2. theorem OAI.Ostmann.realZeroKernel_nonneg line 14
  3. theorem OAI.Ostmann.realZeroKernel_complex line 17
  4. theorem OAI.Ostmann.realZeroKernel_ratio line 24

    Source documentation

    The universal ratio bound used for zeros near the real axis.

    theorem realZeroKernel_ratio {a b y : ℝ} (ha : 0 < a) (hab : a ≤ b) :
    realZeroKernel a y ≤ (b / a) * realZeroKernel b y := by
…

    Mentions: OAI.Ostmann.realZeroKernel

  5. theorem OAI.Ostmann.realZeroKernel_high line 40

    Source documentation

    At imaginary height at least one, bounded real parts give an absolute constant independent of the zero-free region.

    theorem realZeroKernel_high {a b y : ℝ} (ha : 0 < a) (hab : a ≤ b)
    (hb : b ≤ 2) (hy : 1 ≤ y ^ 2) :
    realZeroKernel a y ≤ 5 * realZeroKernel b y := by
…

    Mentions: OAI.Ostmann.realZeroKernel

  6. theorem OAI.Ostmann.realZeroKernel_gap line 53