noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Discrepancy (N : ℕ) (eps : ℝ) (Q : Finset ℕ) (c : ℕ → ℝ) : ℝ

The original signed modulus sum, before any absolute value or approximation.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Discrepancy N eps Q c = ∑ d ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q ↑N, c d * ((∑ x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LowPositivePrefixAtoms N eps, if ↑(x.fst.1 * x.fst.2 * x.snd) ≡ ↑N [ZMOD ↑d] then 1 else 0) - (∑ x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LowPositivePrefixAtoms N eps, if (x.fst.1 * x.fst.2 * x.snd).Coprime d then 1 else 0) / ↑d.totient)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Discrepancy_eq_reindexed (N : ℕ) (eps : ℝ) (Q : Finset ℕ) (c : ℕ → ℝ) : fouvryG9Discrepancy N eps Q c = ∑ d ∈ AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q ↑N, c d * ((∑ y ∈ fouvryG9Carrier N eps, if ↑(y.2.2 * y.1) ≡ ↑N [ZMOD ↑d] then 1 else 0) - (∑ y ∈ fouvryG9Carrier N eps, if (y.2.2 * y.1).Coprime d then 1 else 0) / ↑d.totient)

The complete coprime-mass centering and the external signed weight are preserved.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9_output_dvd_iff {N : ℕ} {eps : ℝ} {x : (_ : ℕ × ℕ) × ℕ} (hx : x ∈ goldbachB9LowPositivePrefixAtoms N eps) (d : ℕ) : d ∣ goldbachPi10Output N x ↔ ↑(x.fst.1 * x.fst.2 * x.snd) ≡ ↑N [ZMOD ↑d]

The actual natural subtraction output agrees with the integer congruence.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9_actual_divisor_count (N : ℕ) (eps : ℝ) (d : ℕ) : ↑{x ∈ goldbachB9LowPositivePrefixAtoms N eps | d ∣ goldbachPi10Output N x}.card = ∑ y ∈ fouvryG9Carrier N eps, if ↑(y.2.2 * y.1) ≡ ↑N [ZMOD ↑d] then 1 else 0

This is the divisor count of the existing mother, not a replacement carrier.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Multiplicity_le_tau_two (N : ℕ) (eps : ℝ) (n m : ℕ) : ↑(fouvryG9Multiplicity N eps n m) ≤ ↑((AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau 2) m)

A repeated long product is counted with its original prime-label multiplicity.