A genuine weak-strip bound for the continued Dirichlet-L derivative

This module joins the continued ordered derivative series to its finite truncation at ⌊|t|⌋₊ + 1. The Abel tail is retained explicitly, so no absolute-convergence argument is used in the weak strip.

theorem DirichletLWeakStripDerivativeBound.abs_lt_natFloor_add_one {t : ℝ} : |t| < ↑(⌊|t|⌋₊ + 1)

The canonical cutoff lies strictly above the height.

theorem DirichletLWeakStripDerivativeBound.natFloor_add_one_le_abs_add_one {t : ℝ} : ↑(⌊|t|⌋₊ + 1) ≤ |t| + 1

The canonical cutoff is at most one above the height.

theorem DirichletLWeakStripDerivativeBound.one_half_lt_sigma {A σ t : ℝ} (hA : A ∈ Set.Ioc 0 (1 / 2)) (ht : 3 < |t|) (hσ : 1 - A / Real.log |t| ≤ σ) : 1 / 2 < σ

In the requested weak strip the real part stays above one half.

theorem DirichletLWeakStripDerivativeBound.norm_sigma_add_tI_le_abs_add_two {A σ t : ℝ} (hA : A ∈ Set.Ioc 0 (1 / 2)) (ht : 3 < |t|) (hσ : 1 - A / Real.log |t| ≤ σ) (hσ2 : σ ≤ 2) : ‖↑σ + ↑t * Complex.I‖ ≤ |t| + 2

The continued argument has norm at most |t| + 2 in the requested strip.

theorem DirichletLWeakStripDerivativeBound.log_natFloor_add_one_le_two_mul_log_abs {t : ℝ} (ht : 3 < |t|) : Real.log ↑(⌊|t|⌋₊ + 1) ≤ 2 * Real.log |t|

The logarithm of the canonical cutoff costs at most twice log |t|.

theorem DirichletLWeakStripDerivativeBound.natFloor_add_one_rpow_one_sub_sigma_le {A σ t : ℝ} (hA : A ∈ Set.Ioc 0 (1 / 2)) (ht : 3 < |t|) (hσ : 1 - A / Real.log |t| ≤ σ) : ↑(⌊|t|⌋₊ + 1) ^ (1 - σ) ≤ 3 * Real.exp A

The potentially dangerous weak-strip power at the canonical cutoff is uniformly paid by a fixed multiple of exp A.

theorem DirichletLWeakStripDerivativeBound.sum_logCpowWeight_eq_derivative_truncation {q : ℕ} (χ : DirichletCharacter ℂ q) (σ t : ℝ) (m : ℕ) : ∑ n ∈ Finset.range m, DirichletLAbelWeightVariation.logCpowWeight (↑σ + ↑t * Complex.I) ↑n * χ ↑n = ∑ n ∈ Finset.range m, -Complex.log ↑n * ↑n ^ (-(↑σ + ↑t * Complex.I)) * χ ↑n

Exact calibration of the multiplication order in the finite derivative sum. The zero term is handled separately; positive terms use the existing logCpowWeight_nat_eq bridge.

theorem DirichletLWeakStripDerivativeBound.norm_deriv_LFunction_le_truncation_add_tail {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) {A C σ t : ℝ} (hA : A ∈ Set.Ioc 0 (1 / 2)) (hσ : 1 - A / Real.log |t| ≤ σ) (ht : 3 < |t|) (hC : 2 ≤ C) : have m := ⌊|t|⌋₊ + 1; ‖deriv (DirichletCharacter.LFunction χ) (↑σ + ↑t * Complex.I)‖ ≤ Real.exp A * C * Real.log |t| ^ 2 + ↑q * (‖DirichletLAbelWeightVariation.logCpowWeight (↑σ + ↑t * Complex.I) ↑m‖ + DirichletLAbelWeightVariation.logVariationBudget (↑σ + ↑t * Complex.I) ↑m)

Assembly theorem for the continued derivative in the weak strip. This is the honest tail-budget interface: the first summand is the proved finite truncation estimate and the second is exactly the paid Abel tail at m = ⌊|t|⌋₊ + 1.

theorem DirichletLWeakStripDerivativeBound.canonical_tail_le_fixed_log_sq {q : ℕ} {A σ t : ℝ} (hA : A ∈ Set.Ioc 0 (1 / 2)) (hσ : 1 - A / Real.log |t| ≤ σ) (hσ2 : σ ≤ 2) (ht : 3 < |t|) : have m := ⌊|t|⌋₊ + 1; ↑q * (‖DirichletLAbelWeightVariation.logCpowWeight (↑σ + ↑t * Complex.I) ↑m‖ + DirichletLAbelWeightVariation.logVariationBudget (↑σ + ↑t * Complex.I) ↑m) ≤ Real.exp A * (100 * ↑q) * Real.log |t| ^ 2

At the canonical cutoff the entire explicit Abel tail is absorbed by a fixed numerical multiple of the weak-strip logarithmic budget.

theorem DirichletLWeakStripDerivativeBound.norm_deriv_LFunction_le_fixed_log_sq {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) {A C σ t : ℝ} (hA : A ∈ Set.Ioc 0 (1 / 2)) (hσ : 1 - A / Real.log |t| ≤ σ) (hσ2 : σ ≤ 2) (ht : 3 < |t|) (hC : 2 ≤ C) : ‖deriv (DirichletCharacter.LFunction χ) (↑σ + ↑t * Complex.I)‖ ≤ Real.exp A * (C + 100 * ↑q) * Real.log |t| ^ 2

Fully explicit weak-strip derivative bound, with the Abel tail absorbed.