Finite Abel foundation for a weak Dirichlet-L strip

For every nonprincipal complex Dirichlet character modulo q, this module proves the explicit prefix bound ‖∑ k < N, χ k‖ ≤ q and exact finite Abel identities for the Dirichlet-series and derivative weights. No strip source predicate is assumed.

theorem DirichletLWeakStripDerivative.character_norm_le_one {q : ℕ} (χ : DirichletCharacter ℂ q) (n : ℕ) : ‖χ ↑n‖ ≤ 1

theorem DirichletLWeakStripDerivative.sum_one_period_eq_zero {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) : ∑ n ∈ Finset.range q, χ ↑n = 0

theorem DirichletLWeakStripDerivative.sum_aligned_period_eq_zero {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (k : ℕ) : ∑ i ∈ Finset.range q, χ (↑k * ↑q + ↑i) = 0

theorem DirichletLWeakStripDerivative.sum_mul_period_eq_zero {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (k : ℕ) : ∑ i ∈ Finset.range (k * q), χ ↑i = 0

theorem DirichletLWeakStripDerivative.norm_sum_range_character_le_modulus {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (N : ℕ) : ‖∑ n ∈ Finset.range N, χ ↑n‖ ≤ ↑q

A nonprincipal character has every prefix sum bounded by its modulus.

theorem DirichletLWeakStripDerivative.abel_Ico {q : ℕ} (χ : DirichletCharacter ℂ q) (f : ℕ → ℂ) {m n : ℕ} (hmn : m < n) : ∑ i ∈ Finset.Ico m n, f i * χ ↑i = f (n - 1) * ∑ i ∈ Finset.range n, χ ↑i - f m * ∑ i ∈ Finset.range m, χ ↑i - ∑ i ∈ Finset.Ico m (n - 1), (f (i + 1) - f i) * ∑ j ∈ Finset.range (i + 1), χ ↑j

Finite Abel summation for a Dirichlet character.

theorem DirichletLWeakStripDerivative.dirichlet_cpow_abel_Ico {q : ℕ} (χ : DirichletCharacter ℂ q) (s : ℂ) {m n : ℕ} (hmn : m < n) : ∑ k ∈ Finset.Ico m n, ↑k ^ (-s) * χ ↑k = ↑(n - 1) ^ (-s) * ∑ k ∈ Finset.range n, χ ↑k - ↑m ^ (-s) * ∑ k ∈ Finset.range m, χ ↑k - ∑ k ∈ Finset.Ico m (n - 1), (↑(k + 1) ^ (-s) - ↑k ^ (-s)) * ∑ j ∈ Finset.range (k + 1), χ ↑j

Exact finite partial summation for the weight k ↦ k⁻ˢ.

theorem DirichletLWeakStripDerivative.dirichlet_derivative_weight_abel_Ico {q : ℕ} (χ : DirichletCharacter ℂ q) (s : ℂ) {m n : ℕ} (hmn : m < n) : ∑ k ∈ Finset.Ico m n, -Complex.log ↑k * ↑k ^ (-s) * χ ↑k = -Complex.log ↑(n - 1) * ↑(n - 1) ^ (-s) * ∑ k ∈ Finset.range n, χ ↑k - -Complex.log ↑m * ↑m ^ (-s) * ∑ k ∈ Finset.range m, χ ↑k - ∑ k ∈ Finset.Ico m (n - 1), (-Complex.log ↑(k + 1) * ↑(k + 1) ^ (-s) - -Complex.log ↑k * ↑k ^ (-s)) * ∑ j ∈ Finset.range (k + 1), χ ↑j

Exact finite Abel summation for the derivative weight -log(k) k⁻ˢ.