Harmonic tails from a uniform character-prefix bound

This is the partial-summation bridge needed after Pólya--Vinogradov. Unlike the elementary period estimate, the loss is the supplied prefix amplitude P, not the modulus. No lower bound for L(1, χ) is asserted here.

theorem DirichletCharacter.norm_LFunction_sub_sum_le_of_prefix_bound {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (s : ℂ) (hs : 0 < s.re) (P : ℝ) (hP : ∀ (N : ℕ), ‖∑ k ∈ Finset.range N, χ ↑k‖ ≤ P) {m : ℕ} (hm : 1 ≤ m) : ‖LFunction χ s - ∑ k ∈ Finset.range m, DirichletLAbelWeightVariation.cpowWeight s ↑k * χ ↑k‖ ≤ P * (↑m ^ (-s.re) + ‖s‖ / s.re * ↑m ^ (-s.re))

General-s Abel tail with an arbitrary uniform prefix bound. This is the source-level bridge needed before specializing Pólya--Vinogradov in Chen 1973, Lemma 3.

theorem DirichletCharacter.norm_LFunction_one_sub_harmonic_sum_le_of_prefix_bound {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (P : ℝ) (hP : ∀ (N : ℕ), ‖∑ k ∈ Finset.range N, χ ↑k‖ ≤ P) {m : ℕ} (hm : 1 ≤ m) : ‖LFunction χ 1 - ∑ k ∈ Finset.range m, DirichletLAbelWeightVariation.cpowWeight 1 ↑k * χ ↑k‖ ≤ 2 * P / ↑m

Partial summation improves the harmonic truncation tail from 2q/m to 2P/m whenever every ordinary character prefix has norm at most P.

theorem DirichletCharacter.abs_LFunction_one_re_sub_quadraticHarmonicTruncation_le_of_prefix_bound {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (P : ℝ) (hP : ∀ (N : ℕ), ‖∑ k ∈ Finset.range N, χ ↑k‖ ≤ P) {m : ℕ} (hm : 1 ≤ m) : |(LFunction χ 1).re - χ.quadraticHarmonicTruncation m| ≤ 2 * P / ↑m

Real quadratic form of the prefix-bounded harmonic tail.