Whole primitive source for a common real prime profile

The conductor split exponent is independent of any later modulus exponent. Both source and prime variables retain their cofactor coprimality screens.

noncomputable def Wu2004MeanValue.commonPrimitiveSource (f : ℕ → ℂ) (r : ℕ → ℝ) (h Q L U : ℕ) : ℝ

Equations

• Wu2004MeanValue.commonPrimitiveSource f r h Q L U = ∑ q ∈ Finset.Icc 2 Q, (↑q.totient)⁻¹ * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖Wu2004MeanValue.realMovingAmplitude (AnalyticNumberTheory.LargeSieve.panSourceG f h) (AnalyticNumberTheory.LargeSieve.panSourceD h) r L U χ‖

theorem Wu2004MeanValue.commonPrimitiveSource_nonneg (f : ℕ → ℂ) (r : ℕ → ℝ) (h Q L U : ℕ) : 0 ≤ commonPrimitiveSource f r h Q L U

theorem Wu2004MeanValue.panSourceD_sum_eq_lowPrimeSet {q : ℕ} (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) (h : ℕ) (r : ℝ) : ∑ p ∈ Finset.Icc 1 ⌊r⌋₊, AnalyticNumberTheory.LargeSieve.panSourceD h p * ↑χ ↑p = ∑ p ∈ lowPrimeSet r h, ↑χ ↑p

theorem Wu2004MeanValue.commonPrimitiveSource_eq_lowRealMovingSource (f : ℕ → ℂ) (r : ℕ → ℝ) (h Q L U : ℕ) : commonPrimitiveSource f r h Q L U = lowRealMovingSource (AnalyticNumberTheory.LargeSieve.panSourceG f h) (fun (x : ℕ) (x_1 : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter x) => r) (Finset.Ioc L U) h Q

theorem Wu2004MeanValue.commonPrimitiveSource_mono (f : ℕ → ℂ) (r : ℕ → ℝ) (h L U : ℕ) {Q R : ℕ} (hQR : Q ≤ R) : commonPrimitiveSource f r h Q L U ≤ commonPrimitiveSource f r h R L U

theorem Wu2004MeanValue.commonPrimitiveSource_split (f : ℕ → ℂ) (r : ℕ → ℝ) (h Q L U T : ℕ) (hT : 1 ≤ T) : commonPrimitiveSource f r h Q L U = commonPrimitiveSource f r h (min Q T) L U + ∑ q ∈ Finset.Ioc T Q, (↑q.totient)⁻¹ * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖realMovingAmplitude (AnalyticNumberTheory.LargeSieve.panSourceG f h) (AnalyticNumberTheory.LargeSieve.panSourceD h) r L U χ‖

theorem Wu2004MeanValue.commonPrimitiveSource_le_low_add_high (f : ℕ → ℂ) (r : ℕ → ℝ) (h x Q L U : ℕ) (b : ℝ) (hlog : 1 ≤ Real.log ↑x) (hb : 0 ≤ b) (hQ : ↑Q ≤ √↑x / Real.log ↑x ^ b) : commonPrimitiveSource f r h Q L U ≤ lowRealMovingSource (AnalyticNumberTheory.LargeSieve.panSourceG f h) (fun (x : ℕ) (x_1 : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter x) => r) (Finset.Ioc L U) h ⌊Real.log ↑x ^ b⌋₊ + realMovingHighSource f r h x L U b

theorem Wu2004MeanValue.commonPrimitiveSource_log_saving_of_split (A b : ℝ) (hA : 0 < A) (hb : 0 ≤ b) (hAb : A + 6 ≤ b) : ∃ (C : ℝ), 0 < C ∧ ∃ (x₀ : ℕ), ∀ x ≥ x₀, ∀ (h Q L U : ℕ) (f : ℕ → ℂ) (r : ℕ → ℝ), 1 ≤ h → ↑h ≤ √↑x → ↑U ≤ √↑x → ↑Q ≤ √↑x / Real.log ↑x ^ b → Real.log ↑x ^ (2 * b) ≤ ↑L → (∀ (n : ℕ), ‖f n‖ ≤ 1) → (∀ m ∈ Finset.Ioc L U, 0 ≤ r m ∧ ↑m * r m ≤ ↑x) → commonPrimitiveSource f r h Q L U ≤ C * ↑x / Real.log ↑x ^ A

The source cutoff uses the conductor split exponent b, not a subsequent modulus-level exponent. The low and high analytic producers are both consumed with the same screened coefficients and common real prime profile.

theorem Wu2004MeanValue.commonPrimitiveSource_log_saving (A : ℝ) (hA : 0 < A) : ∃ (b : ℝ) (C : ℝ), 0 ≤ b ∧ 0 < C ∧ ∃ (x₀ : ℕ), ∀ x ≥ x₀, ∀ (h Q L U : ℕ) (f : ℕ → ℂ) (r : ℕ → ℝ), 1 ≤ h → ↑h ≤ √↑x → ↑U ≤ √↑x → ↑Q ≤ √↑x / Real.log ↑x ^ b → Real.log ↑x ^ (2 * b) ≤ ↑L → (∀ (n : ℕ), ‖f n‖ ≤ 1) → (∀ m ∈ Finset.Ioc L U, 0 ≤ r m ∧ ↑m * r m ≤ ↑x) → commonPrimitiveSource f r h Q L U ≤ C * ↑x / Real.log ↑x ^ A

Arbitrary logarithmic saving with constants and split exponent chosen before the cofactor, modulus bound, source interval, coefficients and profile.

theorem Wu2004MeanValue.commonPrimitiveSource_log_saving_uniform_level (A : ℝ) (hA : 0 < A) : ∃ (b : ℝ) (C : ℝ), 0 ≤ b ∧ 0 < C ∧ ∃ (x₀ : ℕ), ∀ x ≥ x₀, ∀ (B : ℝ), b ≤ B → ∀ (h Q L U : ℕ) (f : ℕ → ℂ) (r : ℕ → ℝ), 1 ≤ h → ↑h ≤ √↑x → ↑U ≤ √↑x → ↑Q ≤ √↑x / Real.log ↑x ^ B → Real.log ↑x ^ (2 * b) ≤ ↑L → (∀ (n : ℕ), ‖f n‖ ≤ 1) → (∀ m ∈ Finset.Ioc L U, 0 ≤ r m ∧ ↑m * r m ≤ ↑x) → commonPrimitiveSource f r h Q L U ≤ C * ↑x / Real.log ↑x ^ A

A later modulus-level exponent may be increased arbitrarily without changing the source support cutoff or the constants already chosen.