theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedPrimeWindow_card_eq_primeCount {N m : ℕ} {ε : ℝ} (hN : 2 ≤ N) (hm : m ∈ goldbachG12ActiveProductSupport N) : ↑(goldbachG11LinkedPrimeWindow N ε m).card = AnalyticNumberTheory.LargeSieve.PanPrincipal.primeCount ⌊goldbachG11PiLiHi N m⌋₊ - AnalyticNumberTheory.LargeSieve.PanPrincipal.primeCount ⌊goldbachG11PiLiLo N ε m⌋₊

The literal prime-window cardinality, obtained from the actual AP count at modulus one.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeWindowMainMass_eq_gated_add (N d : ℕ) (ε : ℝ) : goldbachG12PrimeWindowMainMass N ε = ∑ m ∈ goldbachG12ActiveProductSupport N with m.Coprime d, goldbachG12PrimeWindowWeight N ε m + ∑ m ∈ goldbachG12ActiveProductSupport N with ¬m.Coprime d, goldbachG12PrimeWindowWeight N ε m

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

Actual output-divisor count minus one main mass independent of the modulus.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12CommonDivisorResidual N ε d = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N m * ↑{r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedPrimeWindow N ε m | d ∣ N - r * m}.card - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeWindowMainMass N ε / ↑d.totient

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12CommonDivisorResidual_eq {N : ℕ} (hN : 2 ≤ N) (ε : ℝ) (d : ℕ) : goldbachG12CommonDivisorResidual N ε d = goldbachG12LinkedDivisorResidual N ε d - goldbachG12PrimeWindowGateLoss N ε d

Removing the coprime gate increases the main term, hence the minus sign.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12CommonDivisorResidual_sum_le {N Q : ℕ} (hN : 2 ≤ N) (ε : ℝ) : ∑ d ∈ goldbachG11LinkedModuli N Q, |goldbachG12CommonDivisorResidual N ε d| ≤ ∑ d ∈ goldbachG11LinkedModuli N Q, |goldbachG12LinkedDivisorResidual N ε d| + ∑ d ∈ Finset.Icc 1 Q, goldbachG12PrimeWindowGateLoss N ε d

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

Unconditional common-main-mass distribution on the existing squarefree, coprime-to-N modulus carrier; all thresholds precede epsilon and Q.