Fully summed main cost on the actual Gram carrier

The local denominator is retained before taking the arithmetic mean. In particular neither the D' term nor span/q is discarded. No joint-arithmetic bound is assumed: its constants come from the proved restricted mean.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramDirectMainCostFactor (κ C : ℝ) (a : ℤ) (R S : ℝ) (K : WExtractedKey) (j cap : Fin 5 → ℕ) : ℝ

Local analytic factor, with both completion terms and the dyadic modulus.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramDirectMainCostFactor κ C a R S K j cap = C * ↑a.natAbs.divisors.card * (↑K.D' + ↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionGridUpper R S K j cap + 1) / ↑(2 ^ j 2 * 2 ^ j 3 * 2 ^ j 4 * 2 ^ j 4)) * ↑(2 ^ (j 2 + 1) * (2 ^ (j 3 + 1) - 1) * 2 ^ (j 4 + 1) * 2 ^ (j 4 + 1)) ^ (1 / 2 + κ)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramDirectMainCostFactor_nonneg {C : ℝ} (hC : 0 ≤ C) (κ : ℝ) (a : ℤ) (R S : ℝ) (K : WExtractedKey) (j cap : Fin 5 → ℕ) : 0 ≤ wGramDirectMainCostFactor κ C a R S K j cap

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramDirectMain_cost_le {κ C : ℝ} (hκ : 0 ≤ κ) (hC : 0 ≤ C) {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) {F : ℕ} (hNF : ∀ n ∈ N, n ≤ F) {a : ℤ} {x η R S M Z : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S) (hM : 0 < M) (hZ : 0 < Z) {K : WExtractedKey} {b : ℕ} {j cap : Fin 5 → ℕ} {positive : Bool} {c : Finset (ℕ × ℕ)} {L : WGramLabel} (hL : L ∈ wGramLabels (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c)) : wGramFouvryCost κ C a R S M Z K j cap L ≤ wGramDirectMainCostFactor κ C a R S K j cap * √↑((wGramModulus L).gcd (wGramNumerator K a L).natAbs)

Pointwise cost extraction uses actual occupied dyadic coordinates.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramDirectMain_weighted_cost_sum {δ : ℝ} (hδ : 0 < δ) : ∃ (Cτ : ℝ) (Cjoint : ℝ), 0 < Cτ ∧ 0 < Cjoint ∧ ∀ (κ C : ℝ) (N : Finset ℕ) (F : ℕ) (a : ℤ) (x η R S M Z T : ℝ) (K : WExtractedKey) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) (β ζ : ℕ → ℝ) (Bβ Bζ : ℝ), 0 ≤ κ → 0 ≤ C → a ≠ 0 → (∀ n ∈ N, 0 < n) → (∀ n ∈ N, n ≤ F) → 0 ≤ R → 0 ≤ S → 0 < M → 0 < Z → (∀ n ∈ N, T ≤ ↑n) → x ^ η < T → 0 ≤ Bβ → 0 ≤ Bζ → (∀ n ∈ N, |β n| ≤ Bβ) → (∀ s ∈ Finset.Ioc 0 ⌊S⌋₊, |ζ s| ≤ Bζ) → ∑ L ∈ wGramMainLabels K a (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c), |wGramWeight K β ζ L| * wGramFouvryCost κ C a R S M Z K j cap L ≤ (Bβ * Bζ) ^ 2 * wGramDirectMainCostFactor κ C a R S K j cap * wGramMainJointMean δ Cτ Cjoint a K F j

All main labels, including both ordered beta and frequency coordinates, are summed. Constants precede the coefficient family and all scales.