Low primitive conductor source with independent (q, χ, a) endpoints. The whole coefficient sum remains inside the norm in the exported estimate.

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

Conductor one is deliberately absent. Every character on this carrier is primitive and nonprincipal. The prime cofactor is fixed, not averaged.

Equations

• Wu2004MeanValue.lowMovingSource f t S h Q = ∑ q ∈ Finset.Icc 2 Q, (↑q.totient)⁻¹ * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖∑ a ∈ S, f a * ↑χ ↑a * AnalyticNumberTheory.LargeSieve.PanLow.coprimePrimePrefix (↑χ) (t q χ a) h‖

theorem Wu2004MeanValue.low_source_nat_moving (A b F : ℝ) (hA : 0 < A) (hb : 0 ≤ b) (hF : 0 ≤ F) : ∃ (C : ℝ), 0 < C ∧ ∃ (N₀ : ℕ), ∀ N ≥ N₀, ∀ (h U Q : ℕ) (S : Finset ℕ) (f : ℕ → ℂ) (t : (q : ℕ) → AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q → ℕ → ℕ), 1 ≤ h → ↑h ≤ √↑N → ↑U ≤ ↑N ^ (2 / 3) → S ⊆ Finset.Icc 1 U → ↑Q ≤ Real.log ↑N ^ b → (∀ a ∈ S, ‖f a‖ ≤ F) → (∀ q ∈ Finset.Icc 2 Q, ∀ (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q), ∀ a ∈ S, t q χ a ≤ N / a) → lowMovingSource f t S h Q ≤ C * ↑N / Real.log ↑N ^ A

Unconditional low-conductor estimate for arbitrary bounded coefficients, arbitrary finite support, and independently moving natural prime endpoints. All analytic constants precede the support, cofactor, weights and endpoints. The support may extend to N^(2/3); there is no logarithmic lower cutoff.