theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12Linked_balanced_support {N m : ℕ} (hm : m ∈ goldbachG12ActiveProductSupport N) : ↑N ^ (4 / 53) ≤ ↑m ∧ ↑m ≤ ↑N ^ (1 - 4 / 53)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12Linked_profiles_and_coefficient {N m : ℕ} {ε : ℝ} (hN : 2 ≤ N) (hz : 2 ≤ ↑N ^ (4 / 53)) (hm : m ∈ goldbachG12ActiveProductSupport N) : (2 ≤ goldbachG11PiLiHi N m ∧ ↑m * goldbachG11PiLiHi N m ≤ ↑N) ∧ (2 ≤ goldbachG11PiLiLo N ε m ∧ ↑m * goldbachG11PiLiLo N ε m ≤ ↑N) ∧ |goldbachG12NormalizedCoefficient N m| ≤ 1

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedWindowResidual (N : ℕ) (ε : ℝ) (d b : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedWindowResidual N ε d b = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N with m.Coprime d, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N m * (↑(AnalyticNumberTheory.Sieve.primesInAP ⌊MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiHi N m⌋₊ d (AnalyticNumberTheory.Sieve.natInvMod d m * b % d)) - ↑(AnalyticNumberTheory.Sieve.primesInAP ⌊MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiLo N ε m⌋₊ d (AnalyticNumberTheory.Sieve.natInvMod d m * b % d)) - (AnalyticNumberTheory.LargeSieve.PanPrincipal.primeCount ⌊MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiHi N m⌋₊ - AnalyticNumberTheory.LargeSieve.PanPrincipal.primeCount ⌊MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiLo N ε m⌋₊) / ↑d.totient)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedWindowResidual_eq_prefix_sub {N : ℕ} (hN : 2 ≤ N) (ε : ℝ) (d b : ℕ) : goldbachG12LinkedWindowResidual N ε d b = Wu2004MeanValue.primeCenteredAPSum (goldbachG12ActiveProductSupport N) (goldbachG12NormalizedCoefficient N) (goldbachG11PiLiHi N) d b - Wu2004MeanValue.primeCenteredAPSum (goldbachG12ActiveProductSupport N) (goldbachG12NormalizedCoefficient N) (goldbachG11PiLiLo N ε) d b

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedWindowResidual_weighted (A : ℝ) (hA : 0 < A) : ∃ (B : ℝ) (C : ℝ), 0 < B ∧ 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (ε : ℝ) (Q : ℕ) (b : ℕ → ℕ), ↑Q ≤ √↑N / Real.log ↑N ^ B → (∀ d ∈ Finset.Icc 1 Q, (b d).Coprime d) → ∑ d ∈ Finset.Icc 1 Q, Wu2004MeanValue.wuModulusWeight d * |goldbachG12LinkedWindowResidual N ε d (b d)| ≤ C * ↑N / Real.log ↑N ^ A

A single source witness pays for both complete prefixes, uniformly in epsilon.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedWindowResidual_squarefree (A : ℝ) (hA : 0 < A) : ∃ (B : ℝ) (C : ℝ), 0 < B ∧ 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (ε : ℝ) (Q : ℕ), ↑Q ≤ √↑N / Real.log ↑N ^ B → ∑ d ∈ goldbachG11LinkedModuli N Q, |goldbachG12LinkedWindowResidual N ε d N| ≤ C * ↑N / Real.log ↑N ^ A

Unweighting is restricted to squarefree moduli; the on-carrier residue stays N.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedWindowResidual_epsilon_one (N d b : ℕ) : goldbachG12LinkedWindowResidual N 1 d b = 0