The frozen short and long large-sieve means apply pointwise to the same Mellin coefficient for every modulus and character.

noncomputable def Wu2004MeanValue.movingSourceCell (f : ℕ → ℂ) (v : ℕ → ℕ) (m A₁ A₂ k : ℕ) (R : ℝ) : ℝ

Equations

• Wu2004MeanValue.movingSourceCell f v m A₁ A₂ k R = ∑ q ∈ AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.conductorCell R, (↑q.totient)⁻¹ * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖Wu2004MeanValue.movingAmplitude (AnalyticNumberTheory.LargeSieve.panSourceG f m) (AnalyticNumberTheory.LargeSieve.panSourceD m) v (2 ^ k * A₁) (min (2 ^ (k + 1) * A₁) A₂) χ‖

theorem Wu2004MeanValue.chosen_source_moving_cell_log_saving : ∃ (C : ℝ), 0 < C ∧ ∀ (B ε : ℝ), 0 ≤ B → 0 < ε → ∃ (X₀ : ℕ), ∀ (x : ℕ), X₀ ≤ x → ∀ (j m A₁ A₂ k : ℕ) (f : ℕ → ℂ) (v : ℕ → ℕ), (∀ (a : ℕ), 1 ≤ v a ∧ v a ≤ x) → A₂ ≤ x → AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.conductorRadius x B j ≤ AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.upperConductor x B → ↑A₂ ≤ ↑x ^ (1 - ε) → Real.log ↑x ^ (2 * B) ≤ ↑A₁ → (∀ (n : ℕ), ‖f n‖ ≤ 1) → movingSourceCell f v m A₁ A₂ k (AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.conductorRadius x B j) ≤ C * ↑x * Real.log ↑x ^ (4 - B) + 776 / ↑x

An unconditional moving-profile source-cell producer. Constants and thresholds precede the arbitrary common coefficient and common profile.