theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Linked_outputDivisors_empty {N m d : ℕ} {ε : ℝ} (hm : m ∈ goldbachG11EffectiveProductSupport N ε) (hNd : N.Coprime d) (hmd : ¬m.Coprime d) : {r ∈ goldbachG11LinkedPrimeWindow N ε m | d ∣ N - r * m} = ∅

An inadmissible cofactor contributes no actual output divisible by d.

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

Literal weighted divisor count of the geometric output mother, minus its coprime-gated prime-window main term. The counting sum runs over the whole E.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedDivisorResidual N ε d = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11EffectiveProductSupport N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11EffectiveProductCoefficient N ε m * ↑{r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedPrimeWindow N ε m | d ∣ N - r * m}.card - (∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11EffectiveProductSupport N ε with m.Coprime d, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11EffectiveProductCoefficient N ε m * (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.goldbachG11LinkedDivisorResidual_eq {N : ℕ} (hN : 2 ≤ N) (ε : ℝ) (d : ℕ) (hNd : N.Coprime d) : goldbachG11LinkedDivisorResidual N ε d = goldbachG11LinkedWindowResidual N ε d N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedDivisorResidual_log_saving (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, |goldbachG11LinkedDivisorResidual N ε d| ≤ C * ↑N / Real.log ↑N ^ A

An unconditional distribution estimate for the actual output-divisor count. The sole remaining level restriction is the proved source's sqrt(N)/log(N)^B.