High primitive conductors with one common moving profile

The entire source sum is inside the norm. The cutoff may vary arbitrarily with its source coordinate, but is the same for every modulus and character.

noncomputable def Wu2004MeanValue.movingHighSource (f : ℕ → ℂ) (v : ℕ → ℕ) (m x A₁ A₂ : ℕ) (B : ℝ) : ℝ

Equations

• Wu2004MeanValue.movingHighSource f v m x A₁ A₂ B = ∑ q ∈ Finset.Ioc ⌊AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.lowConductor x B⌋₊ ⌊AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.upperConductor x B⌋₊, (↑q.totient)⁻¹ * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖Wu2004MeanValue.movingAmplitude (AnalyticNumberTheory.LargeSieve.panSourceG f m) (AnalyticNumberTheory.LargeSieve.panSourceD m) v A₁ A₂ χ‖

theorem Wu2004MeanValue.movingAmplitude_eq_sum_dyadicCells {q : ℕ} (A D : ℕ → ℂ) (v : ℕ → ℕ) (A₁ A₂ : ℕ) (hA₁ : 0 < A₁) (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) : movingAmplitude A D v A₁ A₂ χ = ∑ k ∈ Finset.range (AnalyticNumberTheory.LargeSieve.panDyadicDepth A₁ A₂), movingAmplitude A D v (A₁ * 2 ^ k) (min (2 * (A₁ * 2 ^ k)) A₂) χ

The moving cutoff remains unchanged throughout the exact dyadic partition.

theorem Wu2004MeanValue.movingHighSource_le_sum_active_cells (f : ℕ → ℂ) (v : ℕ → ℕ) (m x A₁ A₂ : ℕ) (B : ℝ) (hx : 1 ≤ Real.log ↑x) (hB : 0 ≤ B) (hA₁ : 0 < A₁) : movingHighSource f v m x A₁ A₂ B ≤ ∑ j ∈ Finset.range (Nat.log 2 x + 1) with AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.conductorRadius x B j ≤ AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.upperConductor x B, ∑ k ∈ Finset.range (AnalyticNumberTheory.LargeSieve.panDyadicDepth A₁ A₂), movingSourceCell f v m A₁ A₂ k (AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.conductorRadius x B j)

theorem Wu2004MeanValue.chosen_high_source_common_moving_profile_log_saving : ∃ (C : ℝ), 0 < C ∧ ∀ (B ε : ℝ), 0 ≤ B → 0 < ε → ∃ (X₀ : ℕ), ∀ (x : ℕ), X₀ ≤ x → ∀ (m A₁ A₂ : ℕ) (f : ℕ → ℂ) (v : ℕ → ℕ), (∀ a ∈ Finset.Ioc A₁ A₂, v a ≤ x) → A₂ ≤ x → ↑A₂ ≤ ↑x ^ (1 - ε) → Real.log ↑x ^ (2 * B) ≤ ↑A₁ → (∀ (n : ℕ), ‖f n‖ ≤ 1) → movingHighSource f v m x A₁ A₂ B ≤ C * ↑x * Real.log ↑x ^ (6 - B) + 6984 * Real.log ↑x ^ 2 / ↑x

A complete high-conductor producer for an arbitrary COMMON moving profile. Only values on the source interval are constrained; zero cutoffs are allowed. This does not allow a profile selected separately by modulus.