theorem Eq21FiniteLogDerivative.anchor_disk_subset_rectangle {δ T t : ℝ} (hδ : 0 < δ) (hδ1 : δ ≤ 1 / 4) (ht : |t| ≤ T) {w : ℂ} (hw : w ∈ Metric.ball (↑(1 + δ / 2) + Complex.I * ↑t) (3 * δ / 2)) : 1 - δ ≤ w.re ∧ w.re ≤ 2 ∧ |w.im| ≤ T + 1

The entire anchor disk fits inside the finite enlarged rectangle.

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

Only finite-rectangle nonvanishing is assumed; growth, anchor and the holomorphic logarithm are supplied by the genuine small-disk theorem.