ResidueComparison.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Integrating the logarithmic derivative

The calculus step in lem:residue of paper 031-01. After the zero comparison bounds the logarithmic derivative of F(σ) = (σ-1) ζ_K(σ), this lemma compares F(1+h) with its residue F(1) on an interval of length at most 4/log D. The analytic continuation and the zeta identities are separate inputs.

theorem OAI.DukePrimeDegree.comparison_of_log_deriv_bound line 24

Source documentation

Integrating a uniform bound on the logarithmic derivative gives a multiplicative comparison of the endpoint values.

theorem comparison_of_log_deriv_bound
    (F : ℝ → ℝ) {a b C : ℝ} (hab : a < b)
    (ha : 0 < F a) (hb : 0 < F b)
    (hcont : ContinuousOn (fun x => Real.log (F x)) (Icc a b))
    (hdiff : DifferentiableOn ℝ (fun x => Real.log (F x)) (Ioo a b))
    (hbound : ∀ x ∈ Ioo a b, |deriv (fun y => Real.log (F y)) x| ≤ C) :
    Real.exp (-C * (b - a)) * F a ≤ F b ∧
      F b ≤ Real.exp (C * (b - a)) * F a := by
…

theorem OAI.DukePrimeDegree.residue_comparison_on_short_interval line 53

Source documentation

The uniform form used at h ≤ 4/log D. The comparison constant is independent of L and of h, including arbitrarily small h.

theorem residue_comparison_on_short_interval
    (F : ℝ → ℝ) {L h C : ℝ} (hL : 0 < L) (hh : 0 < h)
    (hC : 0 ≤ C) (hlength : h ≤ 4 / L)
    (hresidue : 0 < F 1) (hvalue : 0 < F (1 + h))
    (hcont : ContinuousOn (fun x => Real.log (F x)) (Icc 1 (1 + h)))
    (hdiff : DifferentiableOn ℝ (fun x => Real.log (F x)) (Ioo 1 (1 + h)))
    (hbound : ∀ x ∈ Ioo 1 (1 + h), |deriv (fun y => Real.log (F y)) x| ≤ C * L) :
    Real.exp (-4 * C) * F 1 ≤ F (1 + h) ∧
      F (1 + h) ≤ Real.exp (4 * C) * F 1 := by
…

lemma OAI.DukePrimeDegree.log_derivative_bound_from_hadamard line 77

Source documentation

The elementary estimate after applying the real Hadamard identity. Here S is the nonnegative zero sum and G is the gamma-factor term.

lemma log_derivative_bound_from_hadamard
    {L σ A B S G d : ℝ} (hL : 1 ≤ L) (hσ : 1 ≤ σ)
    (hB : 0 ≤ B) (hS : 0 ≤ S) (hSup : S ≤ A * L)
    (hG : |G| ≤ B) (hd : d = S - 1 / σ - L / 2 - G) :
    |d| ≤ (A + B + 2) * L := by
…

lemma OAI.DukePrimeDegree.reciprocal_residue_bound line 92
Source documentation
Evaluating at h = 1/L and using ζ(1+h) ≥ 1 bounds the reciprocal residue. hupper is the upper endpoint comparison just proved.
```
lemma reciprocal_residue_bound {κ F L C : ℝ}
    (hκ : 0 < κ) (hL : 0 < L)
    (hvalue : 1 / L ≤ F) (hupper : F ≤ Real.exp (4 * C) * κ) :
    1 / κ ≤ Real.exp (4 * C) * L := by
…
```