Actual real prime endpoints in the low primitive conductor source. The scale x is natural; endpoints and the fixed product constant are real.

noncomputable def Wu2004MeanValue.lowPrimeSet (r : ℝ) (h : ℕ) : Finset ℕ

Equations

• Wu2004MeanValue.lowPrimeSet r h = {p ∈ Finset.range (⌊r⌋₊ + 1) | Nat.Prime p ∧ p.Coprime h}

theorem Wu2004MeanValue.mem_lowPrimeSet {r : ℝ} {h p : ℕ} (hr : 0 ≤ r) : p ∈ lowPrimeSet r h ↔ Nat.Prime p ∧ p.Coprime h ∧ ↑p ≤ r

The floor in the implementation introduces no endpoint error.

noncomputable def Wu2004MeanValue.lowRealMovingSource (f : ℕ → ℂ) (r : (q : ℕ) → AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q → ℕ → ℝ) (S : Finset ℕ) (h Q : ℕ) : ℝ

Equations

• Wu2004MeanValue.lowRealMovingSource f r S h Q = ∑ q ∈ Finset.Icc 2 Q, (↑q.totient)⁻¹ * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖∑ a ∈ S, f a * ↑χ ↑a * ∑ p ∈ Wu2004MeanValue.lowPrimeSet (r q χ a) h, ↑χ ↑p‖

theorem Wu2004MeanValue.lowRealMovingSource_eq_natural (f : ℕ → ℂ) (r : (q : ℕ) → AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q → ℕ → ℝ) (S : Finset ℕ) (h Q : ℕ) : lowRealMovingSource f r S h Q = lowMovingSource f (fun (q : ℕ) (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) (a : ℕ) => ⌊r q χ a⌋₊) S h Q

theorem Wu2004MeanValue.low_source_real_moving (A b F K : ℝ) (hA : 0 < A) (hb : 0 ≤ b) (hF : 0 ≤ F) (_hK : 0 < K) : ∃ (C : ℝ), 0 < C ∧ ∃ (x₀ : ℕ), ∀ x ≥ x₀, ∀ (h Q : ℕ) (S : Finset ℕ) (f : ℕ → ℂ) (r : (q : ℕ) → AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q → ℕ → ℝ), 1 ≤ h → ↑h ≤ √↑x → (∀ a ∈ S, 1 ≤ a ∧ ↑a ≤ √↑x) → ↑Q ≤ Real.log ↑x ^ b → (∀ a ∈ S, ‖f a‖ ≤ F) → (∀ q ∈ Finset.Icc 2 Q, ∀ (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q), ∀ a ∈ S, 0 ≤ r q χ a ∧ ↑a * r q χ a ≤ K * ↑x) → lowRealMovingSource f r S h Q ≤ C * ↑x / Real.log ↑x ^ A

For every fixed saving, conductor exponent, coefficient bound and product constant, the constants are uniform in the finite support, cofactor, weights, and independent real endpoints r(q, χ, a).

Only actual primes coprime to h occur; conductor one is excluded. Endpoints may be any nonnegative reals (in particular the manuscript's endpoints ≥ 2). This is the low-conductor source estimate, not the full weighted W1/W3 sum.