Real moving endpoints and the manuscript's prime-endpoint domain

The natural product profile a * floor(r(a)) exactly retains every prime at the real endpoint r(a). On every nonempty manuscript block both prime endpoints are at least the source prime, hence at least 2. No extension of the logarithmic integral below 2 is used.

noncomputable def Wu2004MeanValue.realMovingAmplitude {q : ℕ} (A D : ℕ → ℂ) (r : ℕ → ℝ) (L U : ℕ) (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) : ℂ

Equations

• Wu2004MeanValue.realMovingAmplitude A D r L U χ = ∑ a ∈ Finset.Ioc L U, A a * ↑χ ↑a * ∑ p ∈ Finset.Icc 1 ⌊r a⌋₊, D p * ↑χ ↑p

theorem Wu2004MeanValue.realMovingAmplitude_eq_natural {q : ℕ} (A D : ℕ → ℂ) (r : ℕ → ℝ) (L U : ℕ) (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) : realMovingAmplitude A D r L U χ = movingAmplitude A D (fun (a : ℕ) => a * ⌊r a⌋₊) L U χ

theorem Wu2004MeanValue.naturalProfile_le {x a : ℕ} {r : ℝ} (hr : 0 ≤ r) (har : ↑a * r ≤ ↑x) : a * ⌊r⌋₊ ≤ x

noncomputable def Wu2004MeanValue.realMovingHighSource (f : ℕ → ℂ) (r : ℕ → ℝ) (h x L U : ℕ) (B : ℝ) : ℝ

Equations

• Wu2004MeanValue.realMovingHighSource f r h x L U B = ∑ q ∈ Finset.Ioc ⌊AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.lowConductor x B⌋₊ ⌊AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.upperConductor x B⌋₊, (↑q.totient)⁻¹ * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖Wu2004MeanValue.realMovingAmplitude (AnalyticNumberTheory.LargeSieve.panSourceG f h) (AnalyticNumberTheory.LargeSieve.panSourceD h) r L U χ‖

theorem Wu2004MeanValue.chosen_high_source_real_moving_profile_log_saving : ∃ (C : ℝ), 0 < C ∧ ∀ (B ε : ℝ), 0 ≤ B → 0 < ε → ∃ (X₀ : ℕ), ∀ (x : ℕ), X₀ ≤ x → ∀ (h L U : ℕ) (f : ℕ → ℂ) (r : ℕ → ℝ), (∀ a ∈ Finset.Ioc L U, 0 ≤ r a ∧ ↑a * r a ≤ ↑x) → U ≤ x → ↑U ≤ ↑x ^ (1 - ε) → Real.log ↑x ^ (2 * B) ≤ ↑L → (∀ (n : ℕ), ‖f n‖ ≤ 1) → realMovingHighSource f r h x L U B ≤ C * ↑x * Real.log ↑x ^ (6 - B) + 6984 * Real.log ↑x ^ 2 / ↑x

Actual real prime cutoffs, common across the modulus sum, with no rounding error and constants before the entire endpoint profile.

def Wu2004MeanValue.blockLower (H : ℝ) (m : ℕ) : ℝ

Equations

• Wu2004MeanValue.blockLower H m = max H (↑m ^ 2)

noncomputable def Wu2004MeanValue.blockUpper (H N a η : ℝ) (m : ℕ) : ℝ

Equations

• Wu2004MeanValue.blockUpper H N a η m = min (min (2 * H) (↑m ^ (a / (a - 1)))) (η * N)

theorem Wu2004MeanValue.block_prime_endpoint_domain (H N a η : ℝ) (m : ℕ) (hm : Nat.Prime m) (hne : blockLower H m < blockUpper H N a η m) : (2 ≤ blockLower H m / ↑m ∧ ↑m * (blockLower H m / ↑m) ≤ 2 * H) ∧ 2 ≤ blockUpper H N a η m / ↑m ∧ ↑m * (blockUpper H N a η m / ↑m) ≤ 2 * H

On the manuscript's nonempty prime block, both actual li arguments lie in the accepted domain, and both product endpoints are at most 2H. No asymptotic hypothesis or positive-power convention is needed for this finite implication.

theorem Wu2004MeanValue.tail_prime_endpoint_domain (x η : ℝ) (hη : 0 < η) (hη1 : η ≤ 1) (hx : (2 / η) ^ 2 ≤ x) (m : ℕ) (hm : 0 < m) (hmx : ↑m ≤ √x) : 2 ≤ η * x / ↑m ∧ 2 ≤ x / ↑m

The W1 tail's two prime endpoints are also at least 2 once x >= (2/eta)^2, uniformly over m <= sqrt(x).