theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedPrimeWindow_card_eq_primeCount {N m : ℕ} {ε : ℝ} (hN : 2 ≤ N) (hm : m ∈ goldbachG11EffectiveProductSupport 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.goldbachG11PrimeWindowMainMass_eq_gated_add (N d : ℕ) (ε : ℝ) : goldbachG11PrimeWindowMainMass N ε = ∑ m ∈ goldbachG11EffectiveProductSupport N ε with m.Coprime d, goldbachG11PrimeWindowWeight N ε m + ∑ m ∈ goldbachG11EffectiveProductSupport N ε with ¬m.Coprime d, goldbachG11PrimeWindowWeight N ε m

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

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11CommonDivisorResidual 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 - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeWindowMainMass N ε / ↑d.totient

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11CommonDivisorResidual_eq {N : ℕ} (hN : 2 ≤ N) (ε : ℝ) (d : ℕ) : goldbachG11CommonDivisorResidual N ε d = goldbachG11LinkedDivisorResidual N ε d - goldbachG11PrimeWindowGateLoss N ε d

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11CommonDivisorResidual_sum_le {N Q : ℕ} (hN : 2 ≤ N) (ε : ℝ) : ∑ d ∈ goldbachG11LinkedModuli N Q, |goldbachG11CommonDivisorResidual N ε d| ≤ ∑ d ∈ goldbachG11LinkedModuli N Q, |goldbachG11LinkedDivisorResidual N ε d| + ∑ d ∈ Finset.Icc 1 Q, goldbachG11PrimeWindowGateLoss N ε d

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedLevel_le {N Q : ℕ} {B : ℝ} (hN : 2 ≤ N) (hB : 0 < B) (hl : 1 ≤ Real.log ↑N) (hQ : ↑Q ≤ √↑N / Real.log ↑N ^ B) : Q ≤ N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11CommonDivisorResidual_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, |goldbachG11CommonDivisorResidual 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.