Finite Dirichlet-L derivative truncation bound

The finite derivative sum is bounded by majorizing every twisted summand. In particular, this does not compare the norm of a twisted sum with the norm of the corresponding untwisted sum.

theorem DirichletLFiniteDerivativeTruncationBound.norm_derivative_truncation_le {q : ℕ} (χ : DirichletCharacter ℂ q) {A C σ t : ℝ} (hA : A ∈ Set.Ioc 0 (1 / 2)) (σ_ge : 1 - A / Real.log |t| ≤ σ) (t_gt : 3 < |t|) (hC : 2 ≤ C) : have N := ⌊|t|⌋₊; ‖∑ n ∈ Finset.range (N + 1), -Complex.log ↑n * ↑n ^ (-(↑σ + ↑t * Complex.I)) * χ ↑n‖ ≤ Real.exp A * C * Real.log |t| ^ 2

The finite derivative truncation has the same elementary majorant as the zeta truncation, uniformly in the Dirichlet character.