An explicit envelope for the remaining secondary base sum

This coarse envelope uses gcd(s,|A|) <= s; the sharper occupied mean remains separately available. Divisor coefficients are paid by a proved uniform power bound, not an assumed arithmetic-error estimate.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryNumeratorMax (a : ℤ) (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) : ℕ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryNumeratorMax a K F j = a.natAbs * K.1.2.1 * 2 ^ (j 0 + 1) * (F / K.1.1)

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryBaseCountBound (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryBaseCountBound K F j = ↑(2 ^ j 2) * ↑(F / K.1.1) ^ 2 * (4 * ↑(2 ^ (j 0 + 1)) * ↑(2 ^ j 4) * (1 + Real.log ↑(2 ^ (j 0 + 1))))

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryScaleEnvelope (ε δ C Cτ : ℝ) (a : ℤ) (R S : ℝ) (K : WExtractedKey) (F : ℕ) (j cap : Fin 5 → ℕ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryScaleEnvelope ε δ C Cτ a R S K F 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 + ε) * (↑(2 ^ (j 3 + 1) - 1) * √(↑(2 ^ (j 2 + 1) * 2 ^ (j 4 + 1) * 2 ^ (j 4 + 1)) * (Cτ * ↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryNumeratorMax a K F j) ^ δ)))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryScaleEnvelope_nonneg {C : ℝ} (hC : 0 ≤ C) (ε δ Cτ : ℝ) (a : ℤ) (R S : ℝ) (K : WExtractedKey) (F : ℕ) (j cap : Fin 5 → ℕ) : 0 ≤ wGramSecondaryScaleEnvelope ε δ C Cτ a R S K F j cap

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryBases_numerator_le {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 (ℕ × ℕ)} {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))) : (iv3SecondaryNumerator K.1.2.1 v.2.1.1 v.2.2.1 a v.2.1.2.2).natAbs ≤ wGramSecondaryNumeratorMax a K F j

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryBases_mean_le_scaleEnvelope {δ : ℝ} (hδ : 0 < δ) : ∃ (Cτ : ℝ), 0 < Cτ ∧ ∀ (ε C : ℝ) (N : Finset ℕ) (F : ℕ) (a : ℤ) (x η R S M Z : ℝ) (K : WExtractedKey) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)), 0 ≤ ε → 0 ≤ C → (∀ n ∈ N, 0 < n) → (∀ n ∈ N, n ≤ F) → 0 ≤ R → 0 ≤ S → 0 < M → 0 < Z → ∀ v ∈ wGramSecondaryBases (wGramSecondaryLabels K a (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c)), wGramSecondaryGcdDyadicMean ε C a R S K j cap v ≤ wGramSecondaryScaleEnvelope ε δ C Cτ a R S K F j cap

The power-bound constant precedes all residue, coefficient, support and dyadic choices. The nonzero divisor argument is derived from occupation.