noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryRectangleResidual (N : ℕ) (ε ρ : ℝ) (k : ℕ × ℕ) (d b : ℕ) : ℝ

Two complete ordinary prime-centered prefixes, with the original G11 coefficient. The main term here counts all short primes, not prime/copN.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryRectangleResidual N ε ρ k d b = Wu2004MeanValue.primeCenteredAPSum (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridLong N ε ρ k) (fun (m : ℕ) => ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) m)) (fun (x : ℕ) => MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridProfileHi ρ k) d b - Wu2004MeanValue.primeCenteredAPSum (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridLong N ε ρ k) (fun (m : ℕ) => ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) m)) (fun (x : ℕ) => MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridProfileLo N ρ k) d b

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryRectangleResidual_weighted (A : ℝ) (hA : 0 < A) : ∃ (B : ℝ) (C : ℝ), 0 < B ∧ 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (ε ρ : ℝ), 1 < ρ → ρ ≤ 5 / 4 → ∀ k ∈ goldbachG11GridUsed N ε ρ, ∀ (Q : ℕ) (b : ℕ → ℕ), ↑Q ≤ √(4 * ↑N) / Real.log (4 * ↑N) ^ B → (∀ d ∈ Finset.Icc 1 Q, (b d).Coprime d) → ∑ d ∈ Finset.Icc 1 Q, Wu2004MeanValue.wuModulusWeight d * |goldbachG11OrdinaryRectangleResidual N ε ρ k d (b d)| ≤ C * ↑N / Real.log (4 * ↑N) ^ A

Reuse the frozen ordinary source at size 4N. All endpoint and coefficient conditions are supplied; the residues remain arbitrary reduced residues.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryRectangleResidual_squarefree (A : ℝ) (hA : 0 < A) : ∃ (B : ℝ) (C : ℝ), 0 < B ∧ 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (ε ρ : ℝ), 1 < ρ → ρ ≤ 5 / 4 → ∀ k ∈ goldbachG11GridUsed N ε ρ, ∀ (Q : ℕ), ↑Q ≤ √(4 * ↑N) / Real.log (4 * ↑N) ^ B → ∑ d ∈ goldbachG11LinkedModuli N Q, |goldbachG11OrdinaryRectangleResidual N ε ρ k d N| ≤ C * ↑N / Real.log (4 * ↑N) ^ A

Unweight only squarefree moduli and keep the on-carrier residue equal to N.