theorem G11FiniteGate.inv_totient_prime_le {p : ℕ} {z : ℝ} (hp : Nat.Prime p) (hz : 0 < z) (hzp : z ≤ ↑p) : (↑p.totient)⁻¹ ≤ 2 / z

theorem G11FiniteGate.bad_inverseTotientMass_le {N Q m K : ℕ} {z : ℝ} (hQ : Q ≤ N) (hm : 0 < m) (hz : 0 < z) (hf : ∀ p ∈ m.primeFactors, z ≤ ↑p) (hK : m.primeFactors.card ≤ K) : (∑ d ∈ Finset.Icc 1 Q, if ¬m.Coprime d then (↑d.totient)⁻¹ else 0) ≤ 2 * ↑K / z * AnalyticNumberTheory.LargeSieve.conductorHarmonicFactor N ^ 2

Union bound over all distinct prime factors, including those of a composite cofactor.

theorem G11FiniteGate.weightMass_le {N : ℕ} {S : Finset ℕ} {T : ℝ} {w : ℕ → ℝ} (hS : S ⊆ Finset.Icc 1 N) (hT : 0 ≤ T) (hw : ∀ m ∈ S, |w m| ≤ T / ↑m) : ∑ m ∈ S, |w m| ≤ T * AnalyticNumberTheory.LargeSieve.conductorHarmonicFactor N

theorem G11FiniteGate.sum_gate_le_logCube {N Q K : ℕ} {S : Finset ℕ} {z T : ℝ} {w : ℕ → ℝ} (hN : 2 ≤ N) (hQ : Q ≤ N) (hz : 0 < z) (hT : 0 ≤ T) (hS : S ⊆ Finset.Icc 1 N) (hf : ∀ m ∈ S, ∀ p ∈ m.primeFactors, z ≤ ↑p) (hK : ∀ m ∈ S, m.primeFactors.card ≤ K) (hw : ∀ m ∈ S, |w m| ≤ T / ↑m) : ∑ d ∈ Finset.Icc 1 Q, |(∑ m ∈ S with ¬m.Coprime d, w m) / ↑d.totient| ≤ 2 * ↑K * T / z * (1 + Real.log ↑N) ^ 3

A finite main-term gate budget, not a termwise estimate on AP errors.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11EffectiveProductSupport_primeFactors {N m : ℕ} {ε : ℝ} (hm : m ∈ goldbachG11EffectiveProductSupport 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.goldbachG11PrimeWindowWeight (N : ℕ) (ε : ℝ) (m : ℕ) : ℝ

Equations

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

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeWindowMainMass N ε = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11EffectiveProductSupport N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeWindowWeight N ε m

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeWindowGateLoss N ε d = (∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11EffectiveProductSupport N ε with ¬m.Coprime d, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeWindowWeight N ε m) / ↑d.totient

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeWindowMainMass_nonneg (N : ℕ) (ε : ℝ) : 0 ≤ goldbachG11PrimeWindowMainMass N ε

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

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeWindowWeight_le {N m : ℕ} {ε : ℝ} (hm : m ∈ goldbachG11EffectiveProductSupport N ε) : |goldbachG11PrimeWindowWeight N ε m| ≤ ↑N / ↑m

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

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

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