@[instance_reducible]

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

Equations

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

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2PrimeProduct (N : ℕ) (Z : ℝ) : ℝ

The actual S2 switched sieve uses the standard Goldbach Euler product.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2PrimeProduct N Z = MathlibNt.SieveTheory.MertensTheorem.goldbachSieveProduct N ⌈Z⌉₊

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2PrimeProduct_eq_sieveProductPrimeFactors (N : ℕ) (_hEven : Even N) (T Z : ℝ) : goldbachS2PrimeProduct N Z = AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (goldbachS2SwitchedBoundingSieve N _hEven T Z)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.exists_goldbachS2SwitchedBoundingSieve_dimensionOneLocalProductBound : ∃ (K : ℝ), 1 < K ∧ ∀ (N : ℕ) (hEven : Even N) (T Z : ℝ), SwitchingPrinciple.HasDimensionOneLocalProductBound (goldbachS2SwitchedBoundingSieve N hEven T Z) K

A single Mertens constant controls the genuine switched S2 bounding sieve, since its local density and sifting prime product are the same standard Goldbach ones used elsewhere in the production branch.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedSiftedCount_le_rosserFactor_add_upperErrSum (ρ : ℝ) (hρ : 0 < ρ) : ∃ (z₀ : ℝ), ∀ (N : ℕ) (hEven : Even N) (ε Z Δ s : ℝ), z₀ ≤ Z → 2 ≤ Z → 0 < Δ → s = Real.log Δ / Real.log Z → 3 / 2 ≤ s → s ≤ 4 → have T := ↑N ^ (9 / 19 - ε); have S := goldbachS2SwitchedBoundingSieve N hEven T Z; have P := goldbachS1ProdPrimes N Z; ↑(goldbachS2SwitchedSiftedCount N T Z) ≤ goldbachS2SwitchedMainMass N T * (SwitchingPrinciple.jurkatRichertUpperLinearSieveFactor s + ρ) * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S + LinearSieve.upperErrSum S (⌊Δ⌋₊ + 1) (LinearSieve.upperRosserWeight P (⌊Δ⌋₊ + 1))

The genuine switched S2 sifted count is controlled by the honest upper Rosser factor plus the exact finite upper remainder sum.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2_upperErrSum_le_remainderModulusSum (N : ℕ) (hEven : Even N) (ε Z : ℝ) (Q : ℕ) (hN : 1 ≤ N) (hεu : ε < 2 / 15) (hZ : Z ≤ ↑N ^ (1 / 4)) : have T := ↑N ^ (9 / 19 - ε); have S := goldbachS2SwitchedBoundingSieve N hEven T Z; LinearSieve.upperErrSum S (Q + 1) (LinearSieve.upperRosserWeight S.prodPrimes (Q + 1)) ≤ ∑ d ∈ Finset.Icc 1 Q with d.Coprime N, |goldbachS2SwitchedRemainder N T d|

For Z ≤ N^(1/4), the Rosser upper remainder is supported inside the actual coprime switched remainder sum.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedSiftedCount_le_rosserFactor_add_remainderModulusSum (ρ : ℝ) (hρ : 0 < ρ) : ∃ (z₀ : ℝ), ∀ (N : ℕ) (hEven : Even N) (ε Z Δ s : ℝ), z₀ ≤ Z → 2 ≤ Z → 0 < Δ → s = Real.log Δ / Real.log Z → 3 / 2 ≤ s → s ≤ 4 → 1 ≤ N → ε < 2 / 15 → Z ≤ ↑N ^ (1 / 4) → have T := ↑N ^ (9 / 19 - ε); have S := goldbachS2SwitchedBoundingSieve N hEven T Z; ↑(goldbachS2SwitchedSiftedCount N T Z) ≤ goldbachS2SwitchedMainMass N T * (SwitchingPrinciple.jurkatRichertUpperLinearSieveFactor s + ρ) * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S + ∑ d ∈ Finset.Icc 1 ⌊Δ⌋₊ with d.Coprime N, |goldbachS2SwitchedRemainder N T d|

The genuine switched S2 sifted count is bounded by the Rosser main term plus the actual remainder sum on the moduli d ≤ floor Δ.