@[instance_reducible]

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

Equations

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

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedCoeff (N : ℕ) (T : ℝ) (r : ℕ) : ℝ

The bounded coefficient selecting the actual S2 large-prime source.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedCoeff N T r = if r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2Primes N T then 1 else 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedCoeff_eq_one_of_mem {N r : ℕ} {T : ℝ} (hr : r ∈ goldbachS2Primes N T) : goldbachS2SwitchedCoeff N T r = 1

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedCoeff_eq_zero_of_not_mem {N r : ℕ} {T : ℝ} (hr : r ∉ goldbachS2Primes N T) : goldbachS2SwitchedCoeff N T r = 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.abs_goldbachS2SwitchedCoeff_le_one (N : ℕ) (T : ℝ) (r : ℕ) : |goldbachS2SwitchedCoeff N T r| ≤ 1

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedGatedMainMass (N : ℕ) (T : ℝ) (d : ℕ) : ℝ

The gated switched mass at modulus d.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedGatedMainMass N T d = ∑ r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2Primes N T, if r.Coprime d then MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) (↑N / ↑r) else 0

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedRemainder (N : ℕ) (T : ℝ) (d : ℕ) : ℝ

The actual switched remainder at modulus d, with the coprimality gate retained in the main term.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedRemainder N T d = ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedDivCount N T d) - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedGatedMainMass N T d / ↑d.totient

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedPanAPPrefixCount (N Y A₁ A₂ d l : ℕ) (T : ℝ) : ℝ

The Pan counting prefix attached to the bounded large-prime coefficient.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedPanAPPrefixCount N Y A₁ A₂ d l T = ∑ r ∈ Finset.Ioc A₁ A₂, if r.Coprime d then MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedCoeff N T r * ↑(AnalyticNumberTheory.Sieve.primesInAPBelow Y r d l) else 0

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedPanMainPrefix (N Y A₁ A₂ d : ℕ) (T : ℝ) : ℝ

The corresponding Pan main prefix.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedPanMainPrefix N Y A₁ A₂ d T = ∑ r ∈ Finset.Ioc A₁ A₂, if r.Coprime d then MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedCoeff N T r * (MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) (↑Y / ↑r) / ↑d.totient) else 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedDivCount_eq_panAPPrefixCount {N d A₁ A₂ : ℕ} {T : ℝ} (hd : 1 ≤ d) (hdN : d.Coprime N) (hsupp : ∀ ⦃r : ℕ⦄, r ∈ goldbachS2Primes N T → r ∈ Finset.Ioc A₁ A₂) : ↑(goldbachS2SwitchedDivCount N T d) = goldbachS2SwitchedPanAPPrefixCount N N A₁ A₂ d (N % d) T

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedPanMainPrefix_eq_div_gatedMainMass {N A₁ A₂ d : ℕ} {T : ℝ} (hsupp : ∀ ⦃r : ℕ⦄, r ∈ goldbachS2Primes N T → r ∈ Finset.Ioc A₁ A₂) : goldbachS2SwitchedPanMainPrefix N N A₁ A₂ d T = goldbachS2SwitchedGatedMainMass N T d / ↑d.totient

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.liuMainPanCoprimeIntervalSum_eq_goldbachS2SwitchedPrefixCount_sub_mainPrefix (N Y A₁ A₂ d l : ℕ) (T : ℝ) : LiuWeight.liuMainPanCoprimeIntervalSum (LiuWeight.liuLogarithmicIntegral (2 / Real.log 2)) Y A₁ A₂ d l (goldbachS2SwitchedCoeff N T) = goldbachS2SwitchedPanAPPrefixCount N Y A₁ A₂ d l T - goldbachS2SwitchedPanMainPrefix N Y A₁ A₂ d T

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedRemainder_eq_panError {N d A₁ A₂ : ℕ} {T : ℝ} (hd : 1 ≤ d) (hdN : d.Coprime N) (hsupp : ∀ ⦃r : ℕ⦄, r ∈ goldbachS2Primes N T → r ∈ Finset.Ioc A₁ A₂) : goldbachS2SwitchedRemainder N T d = LiuWeight.liuMainPanCoprimeIntervalSum (LiuWeight.liuLogarithmicIntegral (2 / Real.log 2)) N A₁ A₂ d (N % d) (goldbachS2SwitchedCoeff N T)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedRemainder_log_saving (U : ℝ) (hU : 0 < U) : ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (ε : ℝ), 0 < ε → ε < 2 / 15 → ∀ (N : ℕ), N₀ ≤ N → have T := ↑N ^ (9 / 19 - ε); ∑ d ∈ Finset.Icc 1 (LiuWeight.panModulusCutoff N B) with d.Coprime N, |goldbachS2SwitchedRemainder N T d| ≤ C * ↑N / Real.log ↑N ^ U

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedGatedMainMass_eq_mainMass_of_dvd_prodPrimes (N : ℕ) {ε Z : ℝ} (hN : 1 ≤ N) (hεu : ε < 2 / 15) {d : ℕ} (hZ : Z ≤ ↑N ^ (1 / 4)) (hd : d ∣ goldbachS1ProdPrimes N Z) : goldbachS2SwitchedGatedMainMass N (↑N ^ (9 / 19 - ε)) d = goldbachS2SwitchedMainMass N (↑N ^ (9 / 19 - ε))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedBoundingSieve_rem_eq_remainder_of_dvd_prodPrimes {N : ℕ} (hEven : Even N) {ε Z : ℝ} {d : ℕ} (hN : 1 ≤ N) (hεu : ε < 2 / 15) (hZ : Z ≤ ↑N ^ (1 / 4)) (hd : d ∣ goldbachS1ProdPrimes N Z) : have T := ↑N ^ (9 / 19 - ε); BoundingSieve.rem d = goldbachS2SwitchedRemainder N T d