Real harmonic truncations for quadratic Dirichlet L-values

This module turns the natural-order Abel theory into a finite, real-valued approximation to L(1, χ). It is the first elementary reduction used in the large-conductor Landau--Siegel argument: after this point the missing input is a lower bound for an explicit finite quadratic-character harmonic sum.

noncomputable def DirichletCharacter.quadraticHarmonicTruncation {q : ℕ} (χ : DirichletCharacter ℂ q) (m : ℕ) : ℝ

The real harmonic truncation of a Dirichlet character at m. Keeping the finite sum in cpowWeight form makes its relation with the already established natural-order conditional series literal.

Equations

• χ.quadraticHarmonicTruncation m = (∑ n ∈ Finset.range m, DirichletLAbelWeightVariation.cpowWeight 1 ↑n * χ ↑n).re

theorem DirichletCharacter.quadratic_harmonic_sum_im_eq_zero_of_sq_eq_one {q : ℕ} (χ : DirichletCharacter ℂ q) (hquad : χ ^ 2 = 1) (m : ℕ) : (∑ n ∈ Finset.range m, DirichletLAbelWeightVariation.cpowWeight 1 ↑n * χ ↑n).im = 0

A finite harmonic truncation of a quadratic character is itself real as a complex number. This uses the pointwise quadratic reality of the character, not positivity of L(1, χ).

theorem DirichletCharacter.norm_LFunction_one_sub_harmonic_sum_le {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) {m : ℕ} (hm : 1 ≤ m) : ‖LFunction χ 1 - ∑ n ∈ Finset.range m, DirichletLAbelWeightVariation.cpowWeight 1 ↑n * χ ↑n‖ ≤ 2 * ↑q / ↑m

Abel truncation at the real point 1: the error in approximating a nonprincipal Dirichlet L-value by its first m natural terms is at most 2q/m.

theorem DirichletCharacter.abs_LFunction_one_re_sub_quadraticHarmonicTruncation_le {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) {m : ℕ} (hm : 1 ≤ m) : |(LFunction χ 1).re - χ.quadraticHarmonicTruncation m| ≤ 2 * ↑q / ↑m

Real form of the quadratic harmonic truncation theorem. It exposes the precise finite inequality that a classical large-conductor Siegel argument must strengthen: any lower bound for the displayed finite sum transfers to Re L(1, χ) with the explicit loss 2q/m.

theorem DirichletCharacter.quadraticHarmonicTruncation_sub_error_le_LFunction_one_re {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) {m : ℕ} (hm : 1 ≤ m) : χ.quadraticHarmonicTruncation m - 2 * ↑q / ↑m ≤ (LFunction χ 1).re

One-sided transfer from a finite harmonic-sum estimate to L(1, χ). This is convenient for the next large-conductor lower-bound module.