- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
One \(C_9{\gt}0\), fixed before \(\kappa ,N,B\), bounds \((\sum _{q{\lt}L}\mu (q)^2 3^{\omega (q)}E_q(\kappa ))^2\) by \(C_9(\log (N+2))^9 C_\kappa N(1+\log N)^2\sum _{q{\lt}L}E_q(\kappa )\) for \(N\ge 2\), \(\log N\ge 1\), and \(B\ge 0\).
Inspect dependencies
Pay the switched modulus weight by finite Cauchy · compiled type and proof/definition references.
Ordinary BV implies that for each fixed \(0{\lt}\epsilon {\lt}1/6\) and \(A{\gt}0\) some \(C{\gt}0\) gives \(\sum _{q\in \mathcal Q(N),\ q\nmid N}\sum _{d\mid \mathcal P_N,\ d\le N^{1/2-\epsilon }/q}3^{\omega (d)}E_{\rm prime}(N,qd)\le CN/(\log N)^A\) eventually. Here \(E_{\rm prime}(N,m)=\max _l|\pi (N;m,l)-L_*(N)/\varphi (m)|\) over canonical reduced residues, \(L_*=\operatorname {li}_{2/\log 2}\), and \(E_{\rm prime}(N,m)\le E^*(N,m)\). Modulus zero has error zero and modulus one uses residue zero. The proof requests ordinary prefix-maximal saving \(2A+10\).
Inspect dependencies
Pay combined-modulus weighted prime errors · compiled type and proof/definition references.
For every \(A{\gt}0\) there are \(B\ge 0\), \(C{\gt}0\) and \(N_0\) such that \(\sum _{1\le q\le Q_B(N)}E^*(N,q)\le CN/(\log N)^A\) for integers \(N\ge N_0\), where \(Q_B(N)=\lfloor N^{1/2}/(\log N)^B\rfloor \) and \(E^*(N,q)=\max _{y\in \{ 0,\ldots ,N\} }\max _{0\le a{\lt}q,\, (a,q)=1}|\pi (y;q,a)-L_*(y)/\varphi (q)|\). Here \(L_*(x)=2/\log 2+\int _2^xdt/\log t\) for \(x{\gt}1\), while \(L_*(0)=L_*(1)=2/\log 2\) by the totalized interval-integral convention, not a principal value; \(E^*(N,0)=0\).
Inspect dependencies
Bombieri–Vinogradov for primes · compiled type and proof/definition references.
For each requested logarithmic saving, one common pair of Vaughan cutoffs pays the Type I, Type II and small-term means on the chosen high-conductor family, including the prefix and cofactor amplification factors.
Inspect dependencies
Large-conductor Vaughan estimates · compiled type and proof/definition references.
The constructed smoothing function and the proved uniform Landau–Siegel lower bound supply the nonprincipal primitive Siegel–Walfisz estimate required by the ordinary BV producer.
Inspect dependencies
Small-conductor Siegel–Walfisz input · compiled type and proof/definition references.
Fix \(i,j,A\in \mathbb N\), \(C_{\rm scale}\ge 1\) and \(\zeta {\gt}0\). There is a threshold \(x_0\) depending only on these parameters such that for every real \(x\ge x_0\) the bound \(|\mathcal E_{\rm rect}|\le x/(\log x)^A\) holds uniformly in the following data: \(M,T\ge 1\), \(4MT=x\), \(T=x^\nu \), \(\zeta \le \nu \le 1/10+\zeta /10\); an integer residue \(0{\lt}N\le C_{\rm scale}x\); a finite set \(\mathcal U\subset [M,2M]\cap \mathbb N\) and interval \(J=(u,v]\cap \mathbb N\) with \(T\le u\le v\le 2T\); coefficients \(|\alpha (m)|\le \tau _i(m)\) on \(\mathcal U\), the short coefficient \(\beta _N(n)=\mathbf1_{n\ \text{ prime},\, (n,N)=1}\), and a signed well-factorable coefficient \(c\) of order \(j\) at \(Q=x^{(5-5\nu )/9-\zeta }\). Here \(\tau _i\) is the ordered \(i\)-fold divisor function, and \(\mathcal E_{\rm rect}\) is the signed sum over \(1\le q\le \lfloor Q\rfloor \), \((q,N)=1\), of \(c(q)\) times the \(\alpha \beta _N\) bilinear progression mass at \(mn\equiv N\pmod q\) minus its coprime mass divided by \(\varphi (q)\). The threshold precedes all rectangle, residue and coefficient choices.
Inspect dependencies
Well-factorable rectangular Goldbach distribution · compiled type and proof/definition references.
For the constructed Jurkat–Richert functions \(F,f\), let \(c_\gamma =2e^\gamma \). On \(s{\gt}0\), define \(\widehat T^+(s)=s^{-2}\) for \(s\le 3\) and \([F(s)-f(s-1)]/(c_\gamma s)\) for \(s{\gt}3\); define \(\widehat T^-(s)=2s^{-2}\) for \(s\le 2\) and \([F(s-1)-f(s)]/(c_\gamma s)\) for \(s{\gt}2\). These positive extensions of the normalized derivatives \(-F'/c_\gamma \) and \(f'/c_\gamma \) satisfy the complete Suzuki source properties with \(\widehat\beta =2\): positivity, continuity, the initial formulas, weighted delay derivatives, and weighted and exponential decay.
Inspect dependencies
Constructed Jurkat--Richert comparison functions · compiled type and proof/definition references.
\(\exists \kappa \ \forall U{\gt}0\ \exists C{\gt}0,B\ge 0,N_0:\ \sum _{q{\lt}N^{1/2}/(\log N)^B}M_{a_N,I_N,\kappa }(N;q)\le CN/(\log N)^U\) for \(N\ge N_0\); the proof chooses \(\kappa =2/\log 2\).
Inspect dependencies
Liu--Pan distribution for the actual convolution · compiled type and proof/definition references.
\(\forall \epsilon ,A{\gt}0\ \exists C{\gt}0,B\ge 0,N_0:\) the canonical \(L_2\) coprime weighted remainder majorant is \(\le CN/(\log N)^A\) for \(N\ge N_0\).
Inspect dependencies
Liu–Pan convolution distribution · compiled type and proof/definition references.
\(\exists K{\gt}1:\ \prod _{p\in \mathcal P}(1-1/(p-1))^{-1}\le (\log z_2/\log z_1)(1+K/\log z_1)\) for every finite set of odd primes \(\mathcal P\subset [z_1,z_2)\), \(2\le z_1\le z_2\).
Inspect dependencies
Uniform dimension-one Goldbach local product · compiled type and proof/definition references.
\(\forall U{\gt}0\ \exists C{\gt}0,B\ge 0,N_0\ \forall N\ge N_0,I,a:\ \sum _{1\le q\le Q_B(N)}M_{a,I,*}(N;q)\le CN/(\log N)^U\), provided \(|a|\le 1\), \(A_2\le N^{2/3}\), \((\log N)^{2B}\le A_1\).
Inspect dependencies
Pan distribution for varying weights · compiled type and proof/definition references.
\(\epsilon {\lt}1/2\implies G(N,\epsilon )\mathfrak S_{\mathrm{Liu}}(N)/\log N\to (1/4-\epsilon /2)/2\) along the even integers.
Inspect dependencies
Asymptotic of the optimized Selberg denominator · compiled type and proof/definition references.
\(|\mathcal R_{\lambda }(N,\epsilon )|\le \mathcal M_{\mathrm{full}}(N,\epsilon )\) for \(N\ge 1\) and admissible supported \(\lambda \); the majorant has lcm weight \(3^{\omega (d)}\).
Inspect dependencies
Paying the signed Selberg remainder · compiled type and proof/definition references.
Fix hats satisfying the Suzuki source properties and real \(d,\Delta ,\Theta \) with \(0{\lt}\Delta {\lt}1\), \(d{\gt}7/(1-\Delta )\), \(\Theta {\gt}0\), \(2/d{\lt}1/\Theta \) and \(2/\Theta +3/d{\lt}1-\Delta \). The source selects its auxiliary constants, and in particular \(C\ge 3\), before the bounding sieve \(S\) varies. For each \(K\ge 2\) satisfying its dimension-one local-product bound, each integer \(D\ge 2\) and \(4\le s\le 6\), put \(z=\lceil D^{1/s}\rceil \ge 2\) and assume \(s\le \sigma _{\rm src}(D;d)=(\log D)^{1/d}\log \log (27D)\). With \(\mathcal P_S(z)\) the supported primes below \(z\), \(P=\prod _{p\in \mathcal P_S(z)}p\), \(m=2(|\mathcal P_S(z)|+1)\) and \(V_S(z)=\prod _{p\in \mathcal P_S(z)}(1-g_S(p))\), one has \(V_S(z)[f(s)-C e^{\sqrt K}E_m(D,s;d)(\log D)^{-\Delta }]\le \sum _{e\mid P}\lambda _e^-g_S(e)\). The weights are the finite lower Rosser weights of natural level \(D\), and \(E_m(D,s;d)=(1+s^d/\log D)^s s\widehat T^{\eta _m}(s)\), with \(\eta _m=+\) for odd \(m\) and \(-\) for even \(m\).
Inspect dependencies
Lower Rosser comparison uniform in the sieve · compiled type and proof/definition references.
Given hats satisfying the Suzuki source properties and fixed \(d,\Delta ,\Theta \) with \(0{\lt}\Delta {\lt}1\), \(d{\gt}7/(1-\Delta )\), \(\Theta {\gt}0\), \(2/d{\lt}1/\Theta \) and \(2/\Theta +3/d{\lt}1-\Delta \), for every \(K{\gt}1\) and \(\rho {\gt}0\) there is \(z_0\) before the bounding sieve \(S\) varies. If \(z\ge \max (2,z_0)\), \(D_{\rm real}{\gt}0\), \(S\) satisfies the dimension-one local-product bound with \(K\), every sifting prime is at most \(z\), and \(s=\log D_{\rm real}/\log z\in [3/2,4]\), then \(\sum _{e\mid P}\lambda _e^+g_S(e)\le (F(s)+\rho )\prod _{p\mid P}(1-g_S(p))\). Here \(P\) is the product of the sifting primes, the product on the right is over primes, and \(\lambda ^+\) is the finite upper Rosser weight at natural level \(\lfloor D_{\rm real}\rfloor +1\).
Inspect dependencies
Modern upper Rosser comparison · compiled type and proof/definition references.
For fixed \(0{\lt}\epsilon {\lt}1/6\) and \(A{\gt}0\), let \(P_N=\prod _{2{\lt}p\le N^{1/10},\, p\nmid N}p\). Eventually, \(\sum _{N^{1/10}{\lt}q\le N^{1/3},\ q\ \text{ prime},\ q\nmid N}\sum _{d\mid P_N,\ d{\lt}\lfloor N^{1/2-\epsilon }/q\rfloor +1}3^{\omega (d)}E_{\rm prime}(N,qd)\ll _{\epsilon ,A}N/(\log N)^A\). The fixed-endpoint error is \(E_{\rm prime}(N,h)=\max _{0\le a{\lt}h,\, (a,h)=1}|\pi (N;h,a)-L_*(N)/\varphi (h)|\le E^*(N,h)\); all products run over primes. The constants and threshold depend only on the fixed parameters.
Inspect dependencies
The actual weighted conditioned Chen error · compiled type and proof/definition references.