[I71, Lemma 13] and [I71, Lemma 14]

For b ≥ 0 monotone on [B, A], 2 ≤ B ≤ A, ∑_{B ≤ p ≤ A} b(p)/p = ∫_B^A b(x) / (x log x) dx + O(b(A) exp(-κ √(log B))), and the analogous statement with b(B) for b antitone.

The proof is Iwaniec's: summation by parts against S(n) (in the abstract form abs_sum_sub_integral_le) at the points B, ⌊B⌋ + 1, …, ⌊A⌋, A, using S_asymp.

Elementary facts about log ∘ log

theorem IwaniecLinearSieve.continuousOn_inv_mul_log {u v : ℝ} (hu : 1 < u) : ContinuousOn (fun (x : ℝ) => (x * Real.log x)⁻¹) (Set.Icc u v)

theorem IwaniecLinearSieve.integral_inv_mul_log {u v : ℝ} (hu : 1 < u) (huv : u ≤ v) : ∫ (x : ℝ) in u..v, (x * Real.log x)⁻¹ = Real.log (Real.log v) - Real.log (Real.log u)

theorem IwaniecLinearSieve.log_log_sub_log_log_le {u v : ℝ} (hu : 1 < u) (huv : u ≤ v) : Real.log (Real.log v) - Real.log (Real.log u) ≤ (v - u) / (u * Real.log u)

The partition B, ⌊B⌋ + 1, …, ⌊A⌋, A of [B, A]

noncomputable def IwaniecLinearSieve.clampPt (B A : ℝ) (j : ℕ) : ℝ

The points B = a 0 ≤ ⌊B⌋ + 1 ≤ ⋯ ≤ ⌊A⌋ ≤ A = a (⌊A⌋ - ⌊B⌋ + 1).

Equations

• IwaniecLinearSieve.clampPt B A j = max B (min (↑(⌊B⌋₊ + j)) A)

theorem IwaniecLinearSieve.clampPt_mono (B A : ℝ) : Monotone (clampPt B A)

theorem IwaniecLinearSieve.clampPt_zero {B A : ℝ} (hB : 0 ≤ B) : clampPt B A 0 = B

theorem IwaniecLinearSieve.clampPt_last {B A : ℝ} (hBA : B ≤ A) : clampPt B A (⌊A⌋₊ - ⌊B⌋₊ + 1) = A

theorem IwaniecLinearSieve.le_clampPt (B A : ℝ) (j : ℕ) : B ≤ clampPt B A j

theorem IwaniecLinearSieve.clampPt_le {B A : ℝ} (hBA : B ≤ A) (j : ℕ) : clampPt B A j ≤ A

theorem IwaniecLinearSieve.clampPt_succ_le (B A : ℝ) (j : ℕ) : clampPt B A (j + 1) ≤ clampPt B A j + 1

theorem IwaniecLinearSieve.clampPt_eq {B A : ℝ} {j : ℕ} (hj : 1 ≤ j) (hjA : ↑(⌊B⌋₊ + j) ≤ A) : clampPt B A j = ↑(⌊B⌋₊ + j)

theorem IwaniecLinearSieve.floor_clampPt {B A : ℝ} (hB : 0 ≤ B) (hBA : B ≤ A) (j : ℕ) : ⌊clampPt B A j⌋₊ = min (⌊B⌋₊ + j) ⌊A⌋₊

theorem IwaniecLinearSieve.S_eq_S_floor (x : ℝ) : S x = S ↑⌊x⌋₊

S x only depends on ⌊x⌋₊.

theorem IwaniecLinearSieve.S_succ_sub (k : ℕ) : S ↑(k + 1) - S ↑k = if Nat.Prime (k + 1) then (↑(k + 1))⁻¹ else 0

noncomputable def IwaniecLinearSieve.primesIoc (B A : ℝ) : Finset ℕ

The primes p with B < p ≤ A.

Equations

• IwaniecLinearSieve.primesIoc B A = {p ∈ Finset.Ioc ⌊B⌋₊ ⌊A⌋₊ | Nat.Prime p}

noncomputable def IwaniecLinearSieve.primesIcc (B A : ℝ) : Finset ℕ

The primes p with B ≤ p ≤ A.

Equations

• IwaniecLinearSieve.primesIcc B A = {p ∈ Finset.Icc ⌈B⌉₊ ⌊A⌋₊ | Nat.Prime p}

noncomputable def IwaniecLinearSieve.primesIoo (B A : ℝ) : Finset ℕ

The primes p with B < p < A.

Equations

• IwaniecLinearSieve.primesIoo B A = {p ∈ Finset.Ioo ⌊B⌋₊ ⌈A⌉₊ | Nat.Prime p}

theorem IwaniecLinearSieve.le_floor_iff_of_prime {p : ℕ} (hp : Nat.Prime p) {A : ℝ} : p ≤ ⌊A⌋₊ ↔ ↑p ≤ A

theorem IwaniecLinearSieve.floor_lt_iff_of_prime {p : ℕ} (hp : Nat.Prime p) {B : ℝ} : ⌊B⌋₊ < p ↔ B < ↑p

theorem IwaniecLinearSieve.mem_primesIoc {B A : ℝ} {p : ℕ} : p ∈ primesIoc B A ↔ Nat.Prime p ∧ B < ↑p ∧ ↑p ≤ A

theorem IwaniecLinearSieve.mem_primesIcc {B A : ℝ} {p : ℕ} : p ∈ primesIcc B A ↔ Nat.Prime p ∧ B ≤ ↑p ∧ ↑p ≤ A

theorem IwaniecLinearSieve.mem_primesIoo {B A : ℝ} {p : ℕ} : p ∈ primesIoo B A ↔ Nat.Prime p ∧ B < ↑p ∧ ↑p < A

theorem IwaniecLinearSieve.sum_clampPt_eq (b : ℝ → ℝ) {B A : ℝ} (hB : 0 ≤ B) (hBA : B ≤ A) : ∑ j ∈ Finset.range (⌊A⌋₊ - ⌊B⌋₊ + 1), b (clampPt B A (j + 1)) * (S (clampPt B A (j + 1)) - S (clampPt B A j)) = ∑ p ∈ primesIoc B A, b ↑p / ↑p

Summation by parts identity: the Stieltjes sum against S over the partition clampPt is the sum over primes in (B, A].

theorem IwaniecLinearSieve.S_asymp_nonneg : ∃ (c₅ : ℝ) (C : ℝ), 0 ≤ C ∧ ∀ x ≥ 2, |S x - Real.log (Real.log x) - c₅| ≤ C * pntE x

Lemma 13

theorem IwaniecLinearSieve.lemma13_Ioc : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (b : ℝ → ℝ) (A B : ℝ), 2 ≤ B → B ≤ A → MonotoneOn b (Set.Icc B A) → (∀ x ∈ Set.Icc B A, 0 ≤ b x) → |∑ p ∈ primesIoc B A, b ↑p / ↑p - ∫ (x : ℝ) in B..A, b x / (x * Real.log x)| ≤ C * b A * pntE B

[I71, Lemma 13] for the primes in (B, A].

theorem IwaniecLinearSieve.sum_of_forall_cast_eq {t : Finset ℕ} {v : ℝ} (h : ∀ p ∈ t, ↑p = v) (φ : ℝ → ℝ) (hφ : 0 ≤ φ v) : 0 ≤ ∑ p ∈ t, φ ↑p ∧ ∑ p ∈ t, φ ↑p ≤ φ v

theorem IwaniecLinearSieve.lemma13_mono_of_subset : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (b : ℝ → ℝ) (A B : ℝ) (s : Finset ℕ), 2 ≤ B → B ≤ A → MonotoneOn b (Set.Icc B A) → (∀ x ∈ Set.Icc B A, 0 ≤ b x) → (∀ p ∈ s, Nat.Prime p ∧ B ≤ ↑p ∧ ↑p ≤ A) → (∀ (p : ℕ), Nat.Prime p → B < ↑p → ↑p < A → p ∈ s) → |∑ p ∈ s, b ↑p / ↑p - ∫ (x : ℝ) in B..A, b x / (x * Real.log x)| ≤ C * b A * pntE B

[I71, Lemma 13], increasing case, for any set of primes between those in (B, A) and those in [B, A].

theorem IwaniecLinearSieve.lemma13_mono : ∃ (C : ℝ), ∀ (b : ℝ → ℝ) (A B : ℝ), 2 ≤ B → B ≤ A → MonotoneOn b (Set.Icc B A) → (∀ x ∈ Set.Icc B A, 0 ≤ b x) → |∑ p ∈ primesIcc B A, b ↑p / ↑p - ∫ (x : ℝ) in B..A, b x / (x * Real.log x)| ≤ C * b A * pntE B

[I71, Lemma 13]: for b ≥ 0 increasing on [B, A], 2 ≤ B ≤ A, |∑_{B ≤ p ≤ A} b(p)/p - ∫_B^A b(x)/(x log x) dx| ≤ C b(A) exp(-κ √(log B)).

theorem IwaniecLinearSieve.intervalIntegrable_div_mul_log {b : ℝ → ℝ} {A B : ℝ} (hB : 1 < B) (hBA : B ≤ A) (hb : MonotoneOn b (Set.Icc B A) ∨ AntitoneOn b (Set.Icc B A)) : IntervalIntegrable (fun (x : ℝ) => b x / (x * Real.log x)) MeasureTheory.volume B A

theorem IwaniecLinearSieve.lemma13_anti_of_subset : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (b : ℝ → ℝ) (A B : ℝ) (s : Finset ℕ), 2 ≤ B → B ≤ A → AntitoneOn b (Set.Icc B A) → (∀ x ∈ Set.Icc B A, 0 ≤ b x) → (∀ p ∈ s, Nat.Prime p ∧ B ≤ ↑p ∧ ↑p ≤ A) → (∀ (p : ℕ), Nat.Prime p → B < ↑p → ↑p < A → p ∈ s) → |∑ p ∈ s, b ↑p / ↑p - ∫ (x : ℝ) in B..A, b x / (x * Real.log x)| ≤ C * b B * pntE B

[I71, Lemma 13], decreasing case, for any set of primes between those in (B, A) and those in [B, A].

theorem IwaniecLinearSieve.lemma13_anti : ∃ (C : ℝ), ∀ (b : ℝ → ℝ) (A B : ℝ), 2 ≤ B → B ≤ A → AntitoneOn b (Set.Icc B A) → (∀ x ∈ Set.Icc B A, 0 ≤ b x) → |∑ p ∈ primesIcc B A, b ↑p / ↑p - ∫ (x : ℝ) in B..A, b x / (x * Real.log x)| ≤ C * b B * pntE B

[I71, Lemma 13], decreasing case: for b ≥ 0 decreasing on [B, A], 2 ≤ B ≤ A, |∑_{B ≤ p ≤ A} b(p)/p - ∫_B^A b(x)/(x log x) dx| ≤ C b(B) exp(-κ √(log B)).

Lemma 14

theorem IwaniecLinearSieve.integral_inv_log_div_mul_log {u v : ℝ} (hu : 1 < u) (huv : u ≤ v) : ∫ (x : ℝ) in u..v, (Real.log x)⁻¹ / (x * Real.log x) = 1 / Real.log u - 1 / Real.log v

theorem IwaniecLinearSieve.lemma14_of_subset : ∃ (C : ℝ), ∀ (A B : ℝ) (s : Finset ℕ), 2 ≤ B → B ≤ A → (∀ p ∈ s, Nat.Prime p ∧ B ≤ ↑p ∧ ↑p ≤ A) → (∀ (p : ℕ), Nat.Prime p → B < ↑p → ↑p < A → p ∈ s) → |∑ p ∈ s, 1 / (↑p * Real.log ↑p) - (1 / Real.log B - 1 / Real.log A)| ≤ C * pntE B

[I71, Lemma 14]: ∑_{B < p < A} 1/(p log p) = 1/log B - 1/log A + O(exp(-κ √(log B))), for any set of primes between those in (B, A) and those in [B, A].

theorem IwaniecLinearSieve.lemma14 : ∃ (C : ℝ), ∀ (A B : ℝ), 2 ≤ B → B ≤ A → |∑ p ∈ primesIoo B A, 1 / (↑p * Real.log ↑p) - (1 / Real.log B - 1 / Real.log A)| ≤ C * pntE B

[I71, Lemma 14]: ∑_{B < p < A} 1/(p log p) = 1/log B - 1/log A + O(exp(-κ √(log B))).