- 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
The base lower sieve and its Goldbach distribution estimate imply, for every \(\eta {\gt}0\), \((8(\log 4+J)-\eta )\mathcal X_N\le |\mathcal S(N)|\) eventually for even \(N\). Mertens normalization is supplied internally.
Inspect dependencies
Distribution closes the base lower bound · compiled type and proof/definition references.
The base lower asymptotic and the two standard upper inputs imply \(W_{\rm src}(N)\ge (2.6408-\eta )\mathcal X_N\) eventually for even \(N\), for every \(\eta {\gt}0\). The proof uses the exact source weight identity and the integral estimate.
Inspect dependencies
Subtract half the medium-prime upper bound · compiled type and proof/definition references.
If \(z{\lt}y\) and every corrected candidate complement is below \(y^3\), then \(|\mathcal C(N)|-(P(N)+T(N))/2\le |\mathcal C(N)\cap G(N)|\). The proof sums the pointwise weight bound.
Inspect dependencies
Chen finite counting inequality · compiled type and proof/definition references.
For \(N{\gt}1\) and \(\epsilon {\lt}1/60\), \(H(N)\le \mathcal M_q(N,\epsilon )+\mathcal R_q(N,\epsilon )\), using exact conditioned sources and levels \(d{\lt}\lfloor N^{1/2-\epsilon }/q\rfloor +1\).
Inspect dependencies
Sum the conditioned finite upper sieves · compiled type and proof/definition references.
The source lower-density lemma implies that for every \(\delta {\gt}0\) some fixed \(0{\lt}\epsilon {\lt}1/2\) gives \((f(5)-\delta )XV_N-\mathcal R_0(N,\epsilon )\le |\mathcal S(N)|\) eventually for even \(N\). The actual finite remainder is retained.
Inspect dependencies
Lower Rosser density gives the actual base sieve · compiled type and proof/definition references.
If \(2\le z{\lt}y\), \(1\le n{\lt}y^3\), no prime below \(z\) divides \(n\), and \(w(n){\gt}0\), then \(n=1\), \(n\) is prime, or \(n=rs\) for primes \(r,s\ge z\).
Inspect dependencies
Positive weight detects at most two factors · compiled type and proof/definition references.
For even \(N{\gt}2^{110}\), \(P(N)\le \sum _{p\in \mathcal C(N)}\# \{ r\in [z,y):r\text{ prime},\ r\mid N-p\} +60N^{9/10}\). Square-divisibility counts and a valuation bound pay the correction.
Inspect dependencies
Bound the proper-prime-power correction · compiled type and proof/definition references.
For every sufficiently large even \(N\), \(0.67\, \mathfrak S_{\mathrm{Liu}}(N)N/(\log N)^2\le |G(N)|\), where \(G(N)\) is the original set of primes \(p{\lt}N\) with \(N-p\ge 2\) and at most two prime factors counted with multiplicity.
Inspect dependencies
Chen: 0.67 representation bound · compiled type and proof/definition references.
For all \(N,\epsilon ,\lambda \), \(\mathcal B_\lambda =\sum _{d_1,d_2\in \mathcal D}\lambda _{d_1}\lambda _{d_2}\sum _a b(a)\pi (N;a,[d_1,d_2],N\bmod [d_1,d_2])\). The proof is finite sum interchange and least-common-multiple divisibility.
Inspect dependencies
Expand the square into progression counts · compiled type and proof/definition references.
For every fixed \(\kappa \ge 0\) and \(0{\lt}\epsilon \le 10^{-10}\), eventually along even \(N\), the optimal main term \(H_{\kappa }(N)/\mathcal G\) is at most \(3.94033\mathcal X_N\), where \(H_{\kappa }(N)=\sum _a b(a)\operatorname {li}_{\kappa }(N/a)\). The actual source integral is \(I_{\rm Liu}=\int _{1/10}^{1/3}\int _{1/3}^{(1-\alpha )/2}[\alpha \beta (1-\alpha -\beta )]^{-1}\, d\beta \, d\alpha {\lt}0.49254\). The producer transfers the exact reciprocal-log pair sum to this integral, then pays the genuine-li-minus-proxy correction to obtain \(0\le H_{\kappa }(N)\le (0.49254+\eta )N/\log N\) for each fixed \(\eta {\gt}0\) eventually. This is multiplied by the denominator estimate; the proof fixes \(\delta =\eta =10^{-7}\).
Inspect dependencies
Bound the optimized Selberg main term · compiled type and proof/definition references.
For even \(N\) and \(R\ge 1\), the corrected triple slice at a fixed pair is bounded by its optimal Selberg square sum plus the residual counting candidate primes \(N-rsu\mid Q\). Away from this residual only divisor \(1\) contributes.
Inspect dependencies
A candidate prime contributes a unit Selberg packet · compiled type and proof/definition references.
Under the canonical coprime theorem, for every \(\epsilon ,A{\gt}0\), filter \(\mathcal F\le \mathrm{atTop}\) and eventually admissible family \(\lambda _N\), there is \(C{\gt}0\) with \(|\mathcal E_{\lambda _N}(N)|\le CN/(\log N)^A\) eventually in \(\mathcal F\). The full majorant includes the noncoprime part.
Inspect dependencies
Pay the actual signed Selberg remainder · compiled type and proof/definition references.
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.
There exists \(N_0\in \mathbb N\) such that every even \(N\ge N_0\) admits \(N=p+q\), with \(p\) prime and either \(q\) prime or \(q=rs\) for primes \(r,s\), which may coincide.
Inspect dependencies
Chen prime plus at most two primes · compiled type and proof/definition references.
For \(N\ge 1\) and \(\lfloor N^{1/10}\rfloor \ge 2\), \(T(N)\le T_{\rm src}(N)+13N^{9/10}\). An injective selected-factor map isolates the two integer cutoff fibres.
Inspect dependencies
Inject first-factor witnesses into source triples and endpoints · compiled type and proof/definition references.
Under the canonical coprime theorem, for every \(0{\lt}\epsilon \le 10^{-10}\) and \(A{\gt}0\) there is \(C{\gt}0\) such that eventually for even \(N\), \(T(N)\le 3.94033\mathcal X_N+CN/(\log N)^A\). Both cutoff and paper-modulus residuals are included.
Inspect dependencies
Chen triple-penalty upper bound · compiled type and proof/definition references.
The uniform upper density theorem and weighted BV imply, for every \(\eta {\gt}0\), \(H(N)\le (8(\log 8+K/2)+\eta )\mathcal X_N\) eventually for even \(N\). Prime partial summation is internal.
Inspect dependencies
Close the varying-prime upper asymptotic · compiled type and proof/definition references.
The distinct source weighted lower bound implies \(W(N)\ge (2.6408-\eta )\mathcal X_N\) eventually for even \(N\), for every \(\eta {\gt}0\). Source-boundary and valuation losses are absorbed using \(\mathfrak S_{\mathrm{Liu}}(N)\ge U{\gt}0\).
Inspect dependencies
Chen weighted lower bound · 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 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.
\(\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.
\(\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.