theorem AnalyticNumberTheory.LargeSieve.tsum_nat_add_one_rpow_neg_le (σ : ℝ) (hσ : 1 < σ) : ∑' (n : ℕ), ↑(n + 1) ^ (-σ) ≤ 1 + 1 / (σ - 1)

Explicit integral-comparison bound for the real zeta majorant.

theorem AnalyticNumberTheory.LargeSieve.tsum_nat_rpow_neg_le (σ : ℝ) (hσ : 1 < σ) : ∑' (n : ℕ), ↑n ^ (-σ) ≤ 1 + 1 / (σ - 1)

The same majorant indexed from zero; its zero term vanishes.

theorem AnalyticNumberTheory.LargeSieve.norm_dirichletLSeries_le {q : ℕ} (χ : DirichletCharacter ℂ q) (σ t : ℝ) (hσ : 1 < σ) : ‖LSeries (fun (n : ℕ) => χ ↑n) (↑σ + Complex.I * ↑t)‖ ≤ 1 + 1 / (σ - 1)

A Dirichlet L-series in its absolute half-plane is bounded by the elementary zeta majorant, uniformly in the modulus, character and height.

theorem AnalyticNumberTheory.LargeSieve.norm_dirichletLFunction_le {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (σ t : ℝ) (hσ : 1 < σ) : ‖DirichletCharacter.LFunction χ (↑σ + Complex.I * ↑t)‖ ≤ 1 + 1 / (σ - 1)

Explicit uniform right-half-plane bound for the continued L-function.