noncomputable def G12ClippedWindow.residual (N : ℕ) (g L U : ℕ → ℝ) (d b : ℕ) : ℝ

Equations

• G12ClippedWindow.residual N g L U d b = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N with m.Coprime d, g m * (↑(AnalyticNumberTheory.Sieve.primesInAP ⌊U m⌋₊ d (AnalyticNumberTheory.Sieve.natInvMod d m * b % d)) - ↑(AnalyticNumberTheory.Sieve.primesInAP ⌊L m⌋₊ d (AnalyticNumberTheory.Sieve.natInvMod d m * b % d)) - (AnalyticNumberTheory.LargeSieve.PanPrincipal.primeCount ⌊U m⌋₊ - AnalyticNumberTheory.LargeSieve.PanPrincipal.primeCount ⌊L m⌋₊) / ↑d.totient)

theorem G12ClippedWindow.residual_eq_prefix_sub {N : ℕ} (hN : 2 ≤ N) {ε : ℝ} {g L U : ℕ → ℝ} (h : Admissible N ε g L U) (d b : ℕ) : residual N g L U d b = Wu2004MeanValue.primeCenteredAPSum (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N) g U d b - Wu2004MeanValue.primeCenteredAPSum (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N) g L d b

theorem G12ClippedWindow.residual_weighted (A : ℝ) (hA : 0 < A) : ∃ (B : ℝ) (C : ℝ), 0 < B ∧ 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (g L U : ℕ → ℝ) (ε : ℝ) (Q : ℕ) (b : ℕ → ℕ), Admissible N ε g L U → ↑Q ≤ √↑N / Real.log ↑N ^ B → (∀ d ∈ Finset.Icc 1 Q, (b d).Coprime d) → ∑ d ∈ Finset.Icc 1 Q, Wu2004MeanValue.wuModulusWeight d * |residual N g L U d (b d)| ≤ C * ↑N / Real.log ↑N ^ A

A single source witness pays for both complete prefixes, uniformly in epsilon.

theorem G12ClippedWindow.residual_squarefree (A : ℝ) (hA : 0 < A) : ∃ (B : ℝ) (C : ℝ), 0 < B ∧ 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (g L U : ℕ → ℝ) (ε : ℝ) (Q : ℕ), Admissible N ε g L U → ↑Q ≤ √↑N / Real.log ↑N ^ B → ∑ d ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedModuli N Q, |residual N g L U d N| ≤ C * ↑N / Real.log ↑N ^ A

Unweighting is restricted to squarefree moduli; the on-carrier residue stays N.