@[instance_reducible]

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidable_mathlibNt_1 (P : Prop) : Decidable P

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidable_mathlibNt_1 P = Classical.propDecidable P

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.survivesSieve_iff_coprime_siftingProduct (M n : ℕ) (x : ℝ) : SurvivesSieve M x n ↔ ((JurkatRichert1965ChenGammaOneQOne.siftingPrimes M x).prod id).Coprime n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalH_real_eq_siftedCount (A : Finset ℕ) (M d : ℕ) (x : ℝ) : ↑(literalH A M d x) = JurkatRichert1965ChenGammaOneQOne.siftedCount ({n ∈ A | d ∣ n}) M x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalH_filter_one (A : Finset ℕ) (M d : ℕ) (x : ℝ) : literalH ({n ∈ A | d ∣ n}) M 1 x = literalH A M d x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalH_filter_trivialCarrier (A : Finset ℕ) (M d : ℕ) (x : ℝ) : literalH ({n ∈ A | 1 ∣ n}) M d x = literalH A M d x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalH_filter_mul_of_coprime (A : Finset ℕ) (M d e : ℕ) (x : ℝ) (hde : d.Coprime e) : literalH ({n ∈ A | d ∣ n}) M e x = literalH A M (d * e) x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalH_buchstab_interval (A : Finset ℕ) (M d : ℕ) {u v : ℝ} (huv : u ≤ v) : literalH A M d u - literalH A M d v = ∑ p ∈ JurkatRichert1965ChenGammaOneQOne.siftingPrimes M v with u ≤ ↑p, literalH ({n ∈ A | d ∣ n}) M p ↑p

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachHalfOpenPrimes (N : ℕ) (z y : ℝ) : Finset ℕ

The half-open prime interval z ≤ p < y, with p prime and p ∤ N.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachHalfOpenPrimes N z y = {p ∈ MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftingPrimes N y | z ≤ ↑p}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3HalfOpen (A : Finset ℕ) (N : ℕ) (z y : ℝ) : ℤ

The literal half-open sum S3h = Σ_{z≤s<y, s∈P(N)} H(A,N,s;z).

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3HalfOpen A N z y = ∑ s ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachHalfOpenPrimes N z y, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalH A N s z

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachUStrict (A : Finset ℕ) (N : ℕ) (z y : ℝ) : ℤ

The literal strict double sum U = Σ_{z≤r<s<y, r,s∈P(N)} H(A,N,rs;r).

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachUStrict A N z y = ∑ s ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachHalfOpenPrimes N z y, ∑ r ∈ MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftingPrimes N ↑s with z ≤ ↑r, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalH A N (r * s) ↑r

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1_two_buchstab_exact (A : Finset ℕ) (N : ℕ) {z y : ℝ} (hzy : z ≤ y) : goldbachS1 A N y = goldbachS1 A N z - goldbachS3HalfOpen A N z y + goldbachUStrict A N z y