OAI/NumberTheory/Ostmann/ZeroDensity/RealZeroSum.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.realZeroKernel_le_inv line 13
2. theorem OAI.Ostmann.realZeroKernel_zero_free line 20
3. theorem OAI.Ostmann.realZeroKernel_sum_bound line 37

   Source documentation

   An arbitrary zero family may retain finitely many exceptions. The comparison proves summability at s as well as the bound; summability at s is not assumed. Multiplicities are represented by repeated indices.

   theorem realZeroKernel_sum_bound {ι : Type*} (ρ : ι → ℂ) (E : Finset ι)
       (s s₀ c δ C : ℝ) (hρ : ∀ i, 0 ≤ (ρ i).re ∧ (ρ i).re < 1)
       (hs : 1 < s) (hss : s ≤ s₀) (hs₀ : s₀ ≤ 2) (hc : 0 < c)
       (hC5 : 5 ≤ C) (hCc : 1 + c⁻¹ ≤ C) (hgap : s₀ - s ≤ δ)
       (hregion : ∀ i ∉ E, (ρ i).im ^ 2 < 1 → c * δ ≤ s - (ρ i).re)
       (hsum : Summable (fun i => realZeroKernel (s₀ - (ρ i).re) (ρ i).im)) :
       Summable (fun i => realZeroKernel (s - (ρ i).re) (ρ i).im) ∧
         (∑' i, realZeroKernel (s - (ρ i).re) (ρ i).im) ≤
           C * (∑' i, realZeroKernel (s₀ - (ρ i).re) (ρ i).im) +
             ∑ i ∈ E, (s - (ρ i).re)⁻¹ := by
   …

   Mentions: OAI.Ostmann.realZeroKernel