theorem Eq21LocalLog.norm_LFunction_le_growth {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (z : ℂ) (hz : 0 < z.re) : ‖DirichletCharacter.LFunction χ z‖ ≤ ↑q * (1 + ‖z‖ / z.re)

The elementary conditional-series estimate, with no height restriction.

theorem Eq21LocalLog.delta_quarter_le_norm_LFunction_anchor {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) {δ : ℝ} (hδ : 0 < δ) (hδ1 : δ ≤ 1 / 4) (t : ℝ) : δ / 4 ≤ ‖DirichletCharacter.LFunction χ (↑(1 + δ / 2) + Complex.I * ↑t)‖

The absolute-convergence anchor, valid also for quadratic characters.

theorem Eq21LocalLog.norm_deriv_le_small_disk (h : ℂ → ℂ) (a z : ℂ) {δ A : ℝ} (hδ : 0 < δ) (hA : 0 < A) (hh : DifferentiableOn ℂ h (Metric.ball a (3 * δ / 2))) (hosc : ∀ w ∈ Metric.ball a (3 * δ / 2), (h w).re - (h a).re ≤ A) (hz : dist z a ≤ δ) : ‖deriv h z‖ ≤ 40 * A / δ

Interior derivative bound from a real-part oscillation at a nearby anchor.

theorem Eq21LocalLog.norm_logDeriv_le_small_disk (g : ℂ → ℂ) (a z : ℂ) {δ B b : ℝ} (hδ : 0 < δ) (hb : 0 < b) (hbB : b < B) (hg : DifferentiableOn ℂ g (Metric.ball a (3 * δ / 2))) (hg0 : ∀ w ∈ Metric.ball a (3 * δ / 2), g w ≠ 0) (hbound : ∀ w ∈ Metric.ball a (3 * δ / 2), ‖g w‖ ≤ B) (hanchor : b ≤ ‖g a‖) (hz : dist z a ≤ δ) : ‖logDeriv g z‖ ≤ 40 * Real.log (B / b) / δ

The logarithm and its amplitude are constructed internally from nonvanishing, a growth bound and a single lower anchor. No logarithm branch is assumed.

theorem Eq21LocalLog.anchor_disk_re_lower {δ : ℝ} (_hδ : 0 < δ) (t : ℝ) {w : ℂ} (hw : w ∈ Metric.ball (↑(1 + δ / 2) + Complex.I * ↑t) (3 * δ / 2)) : 1 - δ < w.re

The small anchor disk lies in the asserted zero-free half-plane.

theorem Eq21LocalLog.norm_LFunction_le_on_anchor_disk {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) {δ : ℝ} (hδ : 0 < δ) (hδ1 : δ ≤ 1 / 4) (t : ℝ) {w : ℂ} (hw : w ∈ Metric.ball (↑(1 + δ / 2) + Complex.I * ↑t) (3 * δ / 2)) : ‖DirichletCharacter.LFunction χ w‖ ≤ 8 * ↑q * (1 + |t|)

Linear height growth on the small disk, paid for by the conditional series.

theorem Eq21LocalLog.norm_logDeriv_LFunction_le_of_zeroFree_halfPlane {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) {δ : ℝ} (hδ : 0 < δ) (hδ1 : δ ≤ 1 / 4) (hzero : ∀ (z : ℂ), 1 - δ ≤ z.re → DirichletCharacter.LFunction χ z ≠ 0) (t β : ℝ) (hβlo : 1 - δ / 2 ≤ β) (hβhi : β ≤ 1 + δ) : ‖logDeriv (DirichletCharacter.LFunction χ) (↑β + Complex.I * ↑t)‖ ≤ 40 / δ * Real.log (32 * ↑q * (1 + |t|) / δ)

Quantitative logarithmic derivative in a zero-free half-plane. The only conditional analytic input is the displayed nonvanishing hypothesis. The explicit cost is one inverse width, uniformly in all real heights.