The complete restricted main arithmetic aggregate

Cauchy--Schwarz is applied jointly over the common index and all ordered bases, after the r mean. The two resulting sums use different fiberings of the same retained carrier. No unrestricted common-index residual is used.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainRestricted_sqrt_gcd_sum {δ : ℝ} (hδ : 0 < δ) : ∃ (Cτ : ℝ) (Cjoint : ℝ), 0 < Cτ ∧ 0 < Cjoint ∧ ∀ (d N M Hmax S R : ℕ) (a : ℤ) (H : Finset ℤ) (G : Finset WGramSecondaryBase), a ≠ 0 → 0 < S → (∀ h ∈ H, h ≠ 0 ∧ h.natAbs ≤ Hmax) → (∀ v ∈ G, mainRestrictedData d a N M S H v) → ∑ v ∈ G, ∑ r ∈ Finset.Ioc 0 R, √↑((v.1 * r * v.2.1.2.1 * v.2.2.2.1).gcd (iv3CorrelationNumerator d v.1 v.2.1.1 v.2.2.1 v.2.1.2.1 v.2.2.2.1 a v.2.1.2.2 v.2.2.2.2).natAbs) ≤ ↑R * (√(↑N * ↑M ^ 2 * ↑S ^ 2 * ↑H.card ^ 2 * (Cτ * ↑(mainRestrictedMax a d N M Hmax S) ^ δ)) * √(↑N * ↑M ^ 2 * ↑H.card ^ 2 * (Cjoint * ↑S ^ 2 * (1 + Real.log ↑S) * ↑(mainRestrictedMax a d N M Hmax S) ^ δ)))

An explicit bound with no remaining arithmetic or base sum. The constants are chosen before every coefficient and every finite carrier.