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)
:
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)
:
Real quadratic form of the prefix-bounded harmonic tail.