The refined secondary arithmetic mean in the complete original energy

Constants are selected before the varying residue, support and coefficients. The secondary fixed-data sum and the primary nonzero sum remain explicit. This is not the fully aggregated estimate (4.10).

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wSeparatedCorrelationEnergy_secondary_gcdMean {ε κ : ℝ} (hε : 0 < ε) (hκ : 0 < κ) : ∃ (Czero : ℝ) (Cnonzero : ℝ), 0 < Czero ∧ 0 < Cnonzero ∧ ∀ (N : Finset ℕ) (F : ℕ) (a : ℤ) (x η R S M Z T εSupport : ℝ) (K : WExtractedKey) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) (β ζ : ℕ → ℝ) (Bβ Bζ : ℝ), a ≠ 0 → 0 ≤ R → 0 ≤ S → 0 < M → 0 < Z → (∀ n ∈ N, T ≤ ↑n) → (∀ n ∈ N, n ≤ F) → 1 < x → η < εSupport → x ^ εSupport ≤ T → 0 ≤ Bβ → 0 ≤ Bζ → (∀ n ∈ N, |β n| ≤ Bβ) → (∀ s ∈ Finset.Ioc 0 ⌊S⌋₊, |ζ s| ≤ Bζ) → wSeparatedCorrelationEnergy x N S (wGramPrefix N a x η R S M Z K b j cap positive) c K β ζ a ≤ (Bβ * Bζ) ^ 2 * ↑(2 ^ j 1) * Czero * ↑(wGramResonanceScaleBoxCard K F j) * wGramResonanceScaleEnvelope K F j ε + (∑ v ∈ wGramSecondaryBases (wGramSecondaryLabels K a (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c)), |wGramWeight K β ζ (wGramSecondaryJoin v 0)| * wGramSecondaryGcdDyadicMean κ Cnonzero a R S K j cap v + ∑ L ∈ wGramLabels (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c) with wGramNumerator K a L ≠ 0 ∧ ¬wGramSecondaryResonant L, |wGramWeight K β ζ L| * wGramFouvryCost κ Cnonzero a R S M Z K j cap L)