Quantitative control of a zero-free local explicit-formula remainder

The derivative estimate below is the Borel--Carathéodory replacement for the exponentially wasteful Cauchy estimate on g itself. Its input is an actual holomorphic logarithm h of the nonvanishing factor. Crucially, the numerical input is the additive oscillation of log ‖g‖; no circle maximum/interior minimum ratio is assumed.

theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.norm_deriv_holomorphicLog_le (h : ℂ → ℂ) (c : ℂ) {R A : ℝ} (hR : 0 < R) (hA : 0 < A) (hh : DifferentiableOn ℂ h (Metric.ball c R)) (hosc : ∀ z ∈ Metric.ball c R, (h z).re - (h c).re ≤ A) : ‖deriv h c‖ ≤ 4 * A / R

Borel--Carathéodory controls the derivative of a holomorphic logarithm by its real-part oscillation. The constant 4 comes from applying the theorem on the outer disk and Cauchy's estimate on the half-radius circle.

theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.norm_logDeriv_le_of_holomorphicLog_oscillation (g h : ℂ → ℂ) (c : ℂ) {R A : ℝ} (hR : 0 < R) (hA : 0 < A) (_hg : DifferentiableOn ℂ g (Metric.ball c R)) (hh : DifferentiableOn ℂ h (Metric.ball c R)) (hexp : Set.EqOn (fun (z : ℂ) => Complex.exp (h z)) g (Metric.ball c R)) (hosc : ∀ z ∈ Metric.ball c R, (h z).re - (h c).re ≤ A) : ‖logDeriv g c‖ ≤ 4 * A / R

If h is a holomorphic logarithm of g, the preceding additive estimate is exactly an O(A/R) estimate for the nonzero local explicit-formula remainder g'/g.