Refined secondary means on the original occupied fibers

All fixed-data multiplicities and the original signed weights are retained. The new bound is no worse than the earlier dyadic mean on every occupied base.

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

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryGcdDyadicMean ε C a R S K j cap v = MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramRCostEnvelope ε C a R S K j cap v.1 v.2.1.2.1 v.2.2.2.1 (2 ^ j 3 - 1) (2 ^ (j 3 + 1) - 1) * (↑(2 ^ (j 3 + 1) - 1) * √↑(v.1 * v.2.2.2.1 * (v.2.1.2.1.gcd (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3SecondaryNumerator K.1.2.1 v.2.1.1 v.2.2.1 a v.2.1.2.2).natAbs * (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3SecondaryNumerator K.1.2.1 v.2.1.1 v.2.2.1 a v.2.1.2.2).natAbs.divisors.card)))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryGcdDyadicMean_nonneg {C : ℝ} (hC : 0 ≤ C) (ε : ℝ) (a : ℤ) (R S : ℝ) (K : WExtractedKey) (j cap : Fin 5 → ℕ) (v : WGramSecondaryBase) : 0 ≤ wGramSecondaryGcdDyadicMean ε C a R S K j cap v

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryGcdDyadicMean_le_old {C : ℝ} (hC : 0 ≤ C) (ε : ℝ) (a : ℤ) (R S : ℝ) (K : WExtractedKey) (j cap : Fin 5 → ℕ) (v : WGramSecondaryBase) (hs : 0 < v.2.1.2.1) : wGramSecondaryGcdDyadicMean ε C a R S K j cap v ≤ wGramSecondaryDyadicMean ε C a R S K j cap v

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryFiber_cost_le_gcdMean {ε C : ℝ} (hε : 0 ≤ ε) (hC : 0 ≤ C) {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) {a : ℤ} {x η R S M Z : ℝ} {K : WExtractedKey} {b : ℕ} {j cap : Fin 5 → ℕ} {positive : Bool} {c : Finset (ℕ × ℕ)} {v : WGramSecondaryBase} (hv : v ∈ wGramSecondaryBases (wGramSecondaryLabels K a (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c))) : ∑ r ∈ wGramSecondaryFiber (wGramSecondaryLabels K a (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c)) v, wGramFouvryCost ε C a R S M Z K j cap (wGramSecondaryJoin v r) ≤ wGramSecondaryGcdDyadicMean ε C a R S K j cap v

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryLabels_weighted_cost_le_gcdMean {ε C : ℝ} (hε : 0 ≤ ε) (hC : 0 ≤ C) {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (a : ℤ) (x η R S M Z : ℝ) (K : WExtractedKey) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) (β ζ : ℕ → ℝ) : ∑ L ∈ wGramSecondaryLabels 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 ≤ ∑ 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 ε C a R S K j cap v