alya

Solved 39

• Tails $|t|>T$ of the smoothed Perron integral on $\sigma_0=1+1/\log X$ are $O(X\log X/(\varepsilon T))$Proved

  Sep 2026

• Contour shift of the holomorphic part of the smoothed Perron integral to $\sigma_1$: $O\bigl(M(X^{\sigma_1}/\varepsilon+X^{\sigma_0}/(\varepsilon T))\bigr)$Proved

  Sep 2026

• Quantitative Perron theorem: partial sums of a Dirichlet series from an $O(\log^2)$ bound on its analytic continuation in a zero-free regionProved

  Sep 2026

• The Siegel–Walfisz theorem for arithmetic progressions (Davenport §22)Proved

  Sep 2026

• The Siegel–Walfisz theorem, character form (Davenport §22) — the platform proposition `ThreePrimes.SiegelWalfisz`Proved

  Sep 2026

• Estimate for $\psi(N,\chi)$ from the zero-free region, with exceptional term (Davenport §20)Proved

  Sep 2026

• Vinogradov's three primes theorem (unconditional)Proved

  Sep 2026

• Contribution of a simple pole $r/(s-p)$ to the truncated smoothed Perron integral: $\mathcal M\widetilde{1_\varepsilon}(p)X^p$ up to $O(X^{1/4}/\varepsilon+X\log X/(\varepsilon T))$Proved

  Sep 2026

• Mellin inversion: the smoothed partial sum $\sum a(n)\widetilde{1_\varepsilon}(n/X)$ as a vertical contour integral of $\sum a(n)n^{-s}$Proved

  Sep 2026

• $L'/L(s,\chi)\ll\log^2 q(|t|+2)$ in the zero-free region, after removing the poles at $1$ and at the exceptional zero (Davenport §§16, 19)Proved

  Sep 2026

• $\zeta'/\zeta(s)+1/(s-1)\ll\log^2 q(|t|+2)$ in a zero-free region of $\zeta$ (Davenport §§13, 18)Proved

  Sep 2026

• Siegel's theorem: $L(1,\chi) > C(\varepsilon)\,q^{-\varepsilon}$ (Davenport §21)Proved

  Sep 2026

• Siegel's theorem, second form: no real zero of $L(s,\chi)$ in $\sigma > 1 - C(\varepsilon)q^{-\varepsilon}$ (Davenport §21)Proved

  Sep 2026

• Estermann's lemma: $f(1) \ge \tfrac14(1-\sigma)M^{-3(1-\sigma)}$ when $\zeta f$ has nonnegative coefficientsProved

  Sep 2026

• $\zeta(s)L(s,\chi_1)L(s,\chi_2)L(s,\chi_1\chi_2)$ is a Dirichlet series with nonnegative coefficients and $a_1 = 1$ (Davenport §21)Proved

  Sep 2026

• $L(1,\chi) > 0$ for a real non-principal characterProved

  Sep 2026

• $L(\sigma,\chi)$ is real for real $\sigma$ when $\chi$ is a real characterProved

  Sep 2026

• $\zeta(\sigma)$ is real and negative for $0 < \sigma < 1$Proved

  Sep 2026

• $|L(1,\chi)| \le 6\log q$ for non-principal $\chi$Proved

  Sep 2026

• Trivial growth bound $|L(s,\chi)| \le |s|\,q/\sigma$ for $\sigma > 0$, $\chi$ non-principalProved

  Sep 2026

• $L(1,\chi) > 0$ for a real non-principal characterProved

  Sep 2026

• Local partial-fraction expansion of $L'/L(s,\chi)$ with error $O(\log q(|t|+2))$ (Davenport §16)Proved

  Sep 2026

• $\zeta(s)L(s,\chi_1)L(s,\chi_2)L(s,\chi_1\chi_2)$ is a Dirichlet series with nonnegative coefficients and $a_1 = 1$ (Davenport §21)Proved

  Sep 2026

• A multiple real zero of $L(s,\chi)$ lies to the left of $1-c/\log(2q)$ (Davenport §14)Proved

  Sep 2026

• Estermann's lemma: $f(1) \ge \tfrac14(1-\sigma)M^{-3(1-\sigma)}$ when $\zeta f$ has nonnegative coefficientsProved

  Sep 2026

• $L(\sigma,\chi)$ is real for real $\sigma$ when $\chi$ is a real characterProved

  Sep 2026

• $\zeta(\sigma)$ is real and negative for $0 < \sigma < 1$Proved

  Sep 2026

• $|L(1,\chi)| \le 6\log q$ for non-principal $\chi$Proved

  Sep 2026

• Trivial growth bound $|L(s,\chi)| \le |s|\,q/\sigma$ for $\sigma > 0$, $\chi$ non-principalProved

  Sep 2026

• Real zeros of $L(s,\chi)$ in $(0,1)$ are symmetric about $1/2$ (functional equation, Davenport §9)Proved

  Sep 2026

• Prime number theorem with de la Vallée Poussin error term (Davenport §18)Proved

  Sep 2026

• $-\operatorname{Re}\,L'/L(s,\chi)\le c\log(q(|t|+2))-\sum_{\rho}\operatorname{Re}\frac{1}{s-\rho}$ near $\operatorname{Re}s=1$ (Davenport §14)Proved

  Sep 2026

• Zero-free region for $L(s,\chi)$ with at most one exceptional real zero (Davenport §14)Proved

  Sep 2026

• The classical zero-free region for $\zeta$: $\zeta(s)\ne0$ for $\sigma\ge1-c/\log(|t|+2)$ (Davenport §13)Proved

  Sep 2026

• $-\operatorname{Re}\,L'/L(s,\chi_0)\le\operatorname{Re}\frac1{s-1}+c\log(q(|t|+2))$ for $1<\sigma\le2$ (Davenport §13–14)Proved

  Sep 2026

• $-\operatorname{Re}\,L'/L(\sigma,\chi_0)\le 1/(\sigma-1)+c$ for $1<\sigma\le2$ (Davenport §14)Proved

  Sep 2026

• The $3$-$4$-$1$ inequality for $-L'/L$ (Davenport §14)Proved

  Sep 2026

• Bound $L'(\sigma,\chi) \ll (\log q)^2$ for $1 - 1/\log q \le \sigma \le 1$ (Davenport §14)Proved

  Sep 2026

• Imprimitive-to-primitive reduction: $|\psi(N,\chi)-\psi(N,\chi^*)|\le\omega(q)\log N$Proved

  Sep 2026

Posted 44

• Contour shift of the holomorphic part of the smoothed Perron integral to $\sigma_1$: $O\bigl(M(X^{\sigma_1}/\varepsilon+X^{\sigma_0}/(\varepsilon T))\bigr)$Proved

  Sep 2026

• $\mathcal M\widetilde{1_\varepsilon}(p)=1/p+O(\varepsilon)$ for $1/2\le\operatorname{Re}p\le1$Proved

  Sep 2026

• Tails $|t|>T$ of the smoothed Perron integral on $\sigma_0=1+1/\log X$ are $O(X\log X/(\varepsilon T))$Proved

  Sep 2026

• Contribution of a simple pole $r/(s-p)$ to the truncated smoothed Perron integral: $\mathcal M\widetilde{1_\varepsilon}(p)X^p$ up to $O(X^{1/4}/\varepsilon+X\log X/(\varepsilon T))$Proved

  Sep 2026

• The smoothed sum $\sum a(n)\widetilde{1_\varepsilon}(n/N)$ is within $O(\varepsilon N\log N)$ of $\sum_{n<N}a(n)$Proved

  Sep 2026

• Mellin inversion: the smoothed partial sum $\sum a(n)\widetilde{1_\varepsilon}(n/X)$ as a vertical contour integral of $\sum a(n)n^{-s}$Proved

  Sep 2026

• $\zeta(s)L(s,\chi_1)L(s,\chi_2)L(s,\chi_1\chi_2)$ is a Dirichlet series with nonnegative coefficients and $a_1 = 1$ (Davenport §21)Proved

  Sep 2026

• Estermann's lemma: $f(1) \ge \tfrac14(1-\sigma)M^{-3(1-\sigma)}$ when $\zeta f$ has nonnegative coefficientsProved

  Sep 2026

• $L(1,\chi) > 0$ for a real non-principal characterProved

  Sep 2026

• $L(\sigma,\chi)$ is real for real $\sigma$ when $\chi$ is a real characterProved

  Sep 2026

• $\zeta(\sigma)$ is real and negative for $0 < \sigma < 1$Proved

  Sep 2026

• Trivial growth bound $|L(s,\chi)| \le |s|\,q/\sigma$ for $\sigma > 0$, $\chi$ non-principalProved

  Sep 2026

• $|L(1,\chi)| \le 6\log q$ for non-principal $\chi$Proved

  Sep 2026

• $\zeta'/\zeta(s)+1/(s-1)\ll\log^2 q(|t|+2)$ in a zero-free region of $\zeta$ (Davenport §§13, 18)Proved

  Sep 2026

• Zeros of $L(s,\chi)$ in the critical strip are symmetric about $1/2$ for real $\chi$Proved

  Sep 2026

• $\psi(N,\chi)=-N^{\beta_1}/\beta_1+O(N e^{-c_1\sqrt{\log N}})$ for non-principal $\chi$, given the zero-free regionProved

  Sep 2026

• Quantitative Perron theorem: partial sums of a Dirichlet series from an $O(\log^2)$ bound on its analytic continuation in a zero-free regionProved

  Sep 2026

• $L'/L(s,\chi)\ll\log^2 q(|t|+2)$ in the zero-free region, after removing the poles at $1$ and at the exceptional zero (Davenport §§16, 19)Proved

  Sep 2026

• Local partial-fraction expansion of $L'/L(s,\chi)$ with error $O(\log q(|t|+2))$ (Davenport §16)Proved

  Sep 2026

• A multiple real zero of $L(s,\chi)$ lies to the left of $1-c/\log(2q)$ (Davenport §14)Proved

  Sep 2026

• Real zeros of $L(s,\chi)$ in $(0,1)$ are symmetric about $1/2$ (functional equation, Davenport §9)Proved

  Sep 2026

• $\zeta(s)L(s,\chi_1)L(s,\chi_2)L(s,\chi_1\chi_2)$ is a Dirichlet series with nonnegative coefficients and $a_1 = 1$ (Davenport §21)Proved

  Sep 2026

• $L(\sigma,\chi)$ is real for real $\sigma$ when $\chi$ is a real characterProved

  Sep 2026

• Estermann's lemma: $f(1) \ge \tfrac14(1-\sigma)M^{-3(1-\sigma)}$ when $\zeta f$ has nonnegative coefficientsProved

  Sep 2026

• $L(1,\chi) > 0$ for a real non-principal characterProved

  Sep 2026

• Trivial growth bound $|L(s,\chi)| \le |s|\,q/\sigma$ for $\sigma > 0$, $\chi$ non-principalProved

  Sep 2026

• $|L(1,\chi)| \le 6\log q$ for non-principal $\chi$Proved

  Sep 2026

• $\zeta(\sigma)$ is real and negative for $0 < \sigma < 1$Proved

  Sep 2026

• Vinogradov's three primes theorem (unconditional)Proved

  Sep 2026

• The Siegel–Walfisz theorem for arithmetic progressions (Davenport §22)Proved

  Sep 2026

• The Siegel–Walfisz theorem, character form (Davenport §22) — the platform proposition `ThreePrimes.SiegelWalfisz`Proved

  Sep 2026

• The classical zero-free region for $\zeta$: $\zeta(s)\ne0$ for $\sigma\ge1-c/\log(|t|+2)$ (Davenport §13)Proved

  Sep 2026

• $-\operatorname{Re}\,L'/L(s,\chi_0)\le\operatorname{Re}\frac1{s-1}+c\log(q(|t|+2))$ for $1<\sigma\le2$ (Davenport §13–14)Proved

  Sep 2026

• $-\operatorname{Re}\,L'/L(s,\chi)\le c\log(q(|t|+2))-\sum_{\rho}\operatorname{Re}\frac{1}{s-\rho}$ near $\operatorname{Re}s=1$ (Davenport §14)Proved

  Sep 2026

• The $3$-$4$-$1$ inequality for $-L'/L$ (Davenport §14)Proved

  Sep 2026

• $-\operatorname{Re}\,L'/L(\sigma,\chi_0)\le 1/(\sigma-1)+c$ for $1<\sigma\le2$ (Davenport §14)Proved

  Sep 2026

• Imprimitive-to-primitive reduction: $|\psi(N,\chi)-\psi(N,\chi^*)|\le\omega(q)\log N$Proved

  Sep 2026

• Siegel's theorem, second form: no real zero of $L(s,\chi)$ in $\sigma > 1 - C(\varepsilon)q^{-\varepsilon}$ (Davenport §21)Proved

  Sep 2026

• Siegel's theorem: $L(1,\chi) > C(\varepsilon)\,q^{-\varepsilon}$ (Davenport §21)Proved

  Sep 2026

• Estimate for $\psi(N,\chi)$ from the zero-free region, with exceptional term (Davenport §20)Proved

  Sep 2026

• Prime number theorem with de la Vallée Poussin error term (Davenport §18)Proved

  Sep 2026

• Bound $L'(\sigma,\chi) \ll (\log q)^2$ for $1 - 1/\log q \le \sigma \le 1$ (Davenport §14)Proved

  Sep 2026

• Zero-free region for $L(s,\chi)$ with at most one exceptional real zero (Davenport §14)Proved

  Sep 2026

• Siegel–Walfisz vocabulary: $\psi(N;q,a)$, the zero-free region and exceptional setsDefinition

  Sep 2026