theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport_primeFactors {N m : ℕ} (hm : m ∈ goldbachG12ActiveProductSupport N) : (∀ p ∈ m.primeFactors, ↑N ^ (4 / 53) ≤ ↑p) ∧ m.primeFactors = largePrimeDivisors m (↑N ^ (4 / 53)) ∧ m.primeFactors.card ≤ 20

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeWindowWeight (N : ℕ) (ε : ℝ) (m : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeWindowWeight N ε m = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N m * ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedPrimeWindow N ε m).card

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeWindowMainMass N ε = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeWindowWeight N ε m

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeWindowGateLoss N ε d = (∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N with ¬m.Coprime d, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeWindowWeight N ε m) / ↑d.totient

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeWindowWeight_nonneg (N m : ℕ) (ε : ℝ) : 0 ≤ goldbachG12PrimeWindowWeight N ε m

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeWindowMainMass_nonneg (N : ℕ) (ε : ℝ) : 0 ≤ goldbachG12PrimeWindowMainMass N ε

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeWindowGateLoss_nonneg (N d : ℕ) (ε : ℝ) : 0 ≤ goldbachG12PrimeWindowGateLoss N ε d

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedPrimeWindow_card_le {N m : ℕ} {ε : ℝ} (hm : m ∈ goldbachG12ActiveProductSupport N) : ↑(goldbachG11LinkedPrimeWindow N ε m).card ≤ ↑N / ↑m

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeWindowWeight_le {N m : ℕ} {ε : ℝ} (hm : m ∈ goldbachG12ActiveProductSupport N) : |goldbachG12PrimeWindowWeight N ε m| ≤ ↑N / ↑m

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeWindowGateLoss_sum_le {N Q : ℕ} (ε : ℝ) (hN : 2 ≤ N) (hQ : Q ≤ N) : ∑ d ∈ Finset.Icc 1 Q, goldbachG12PrimeWindowGateLoss N ε d ≤ 40 * ↑N / ↑N ^ (4 / 53) * (1 + Real.log ↑N) ^ 3

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeWindowGateLoss_log_saving (U : ℝ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (ε : ℝ), ∀ Q ≤ N, ∑ d ∈ Finset.Icc 1 Q, goldbachG12PrimeWindowGateLoss N ε d ≤ ↑N / Real.log ↑N ^ U

The threshold is chosen before both the window parameter and the modulus cutoff.