f(2) = 2 ([I71, Lemma 5], the part we need)

We prove (3.9), f(s) = f(4) + (F(3) + 3) log (3/(s-1)) + s - 4 on [2, 4], and f(2) = 2, following Iwaniec: M = f + F satisfies M'(s) = -M(s-1)/(s-1) for s > 3 once it is extended to [2, 3] by M(s) = 3 + F(3) - s + f(s) (MSieve). Then Q(s) = (s-1) M(s) - ∫_{s-1}^s M has derivative 0 on (3, 4) ∪ (4, ∞), so it is constant on [3, ∞), and it tends to 0 because M(s) = O(s e^{-s}). Evaluating Q(3) = 0 gives f(4) + (F(3) + 3) log 3 = 4, i.e. f(s) = s - (F(3) + 3) log (s - 1) on [2, 4].

The value F(3) = 2e^γ - 3 is not needed; only F(3) ≥ 0 is used for the final inequality 1 - f(s)/s ≥ 3 log (s - 1) / s on [2, 4]. The rest of Lemma 5 (F(3) = 2e^γ - 3 via Buchstab's function) is in IwaniecLinearSieve.EulerGamma.LemmaFive.

(3.9)

theorem IwaniecLinearSieve.fSieve_eq_on_Icc' {s : ℝ} (hs : s ∈ Set.Icc 2 4) : fSieve s = fSieve 4 + (FSieve 3 + 3) * Real.log (3 / (s - 1)) + s - 4

[I71, (3.9)]: f(s) = f(4) + (F(3) + 3) log (3/(s-1)) + s - 4 for 2 ≤ s ≤ 4.

Derivatives

theorem IwaniecLinearSieve.hasDerivAt_integral_Ioi {k : ℝ → ℝ} {a s : ℝ} (hint : MeasureTheory.IntegrableOn k (Set.Ioi a) MeasureTheory.volume) (hc : ContinuousOn k (Set.Ioi a)) (has : a < s) : HasDerivAt (fun (u : ℝ) => ∫ (t : ℝ) in Set.Ioi u, k t) (-k s) s

Derivative of u ↦ ∫_u^∞ k.

theorem IwaniecLinearSieve.continuousOn_shift {h : ℝ → ℝ} (hh : Continuous h) : ContinuousOn (fun (t : ℝ) => h (t - 1) / (t - 1)) (Set.Ioi 1)

theorem IwaniecLinearSieve.hasDerivAt_FSieve {s : ℝ} (hs : 3 < s) : HasDerivAt FSieve (-(fSieve (s - 1) / (s - 1))) s

F'(s) = -f(s-1)/(s-1) for s > 3.

theorem IwaniecLinearSieve.hasDerivAt_fSieve_of_four_lt {s : ℝ} (hs : 4 < s) : HasDerivAt fSieve (-(FSieve (s - 1) / (s - 1))) s

f'(s) = -F(s-1)/(s-1) for s > 4.

theorem IwaniecLinearSieve.hasDerivAt_fSieve_of_lt_four {s : ℝ} (hs2 : 2 < s) (hs4 : s < 4) : HasDerivAt fSieve (1 - (FSieve 3 + 3) / (s - 1)) s

f'(s) = 1 - (F(3) + 3)/(s-1) for 2 < s < 4.

Iwaniec's M

noncomputable def IwaniecLinearSieve.MSieve (s : ℝ) : ℝ

Iwaniec's M(s): f(s) + F(s) for s ≥ 3, extended by M(s) = 3 + F(3) - s + f(s) for s ≤ 3 (which is -s M'(s+1) on [2, 3]).

Equations

• IwaniecLinearSieve.MSieve s = IwaniecLinearSieve.fSieve s + IwaniecLinearSieve.FSieve s + max (3 - s) 0

theorem IwaniecLinearSieve.MSieve_of_three_le {s : ℝ} (hs : 3 ≤ s) : MSieve s = fSieve s + FSieve s

theorem IwaniecLinearSieve.MSieve_of_le_three {s : ℝ} (hs : s ≤ 3) : MSieve s = 3 + FSieve 3 - s + fSieve s

theorem IwaniecLinearSieve.continuous_MSieve : Continuous MSieve

theorem IwaniecLinearSieve.MSieve_nonneg (s : ℝ) : 0 ≤ MSieve s

theorem IwaniecLinearSieve.MSieve_antitone : Antitone MSieve

theorem IwaniecLinearSieve.hasSum_g_MSieve {s : ℝ} (hs : 3 ≤ s) : HasSum (fun (k : ℕ) => g (k + 2) s) (MSieve s)

Σ_{k ≥ 2} g_k(s) = M(s) for s ≥ 3.

theorem IwaniecLinearSieve.fr_lt_MSieve (r : ℕ) (s : ℝ) : fr r s < MSieve s

f_r(s) < M(s) (first step of [I71, Lemma 7]).

theorem IwaniecLinearSieve.MSieve_le {s : ℝ} (hs : 3 ≤ s) : MSieve s ≤ (gLead * (1 - gRatio)⁻¹ + gLead * (Real.exp 1 / 3) * (1 - gRatio)⁻¹) * s * Real.exp (-s)

M(s) = O(s e^{-s}): M(s) ≤ C s e^{-s} for s ≥ 3.

theorem IwaniecLinearSieve.hasDerivAt_MSieve {s : ℝ} (hs3 : 3 < s) (hs4 : s ≠ 4) : HasDerivAt MSieve (-(MSieve (s - 1) / (s - 1))) s

The derivative of M for s > 3, s ≠ 4: (s - 1) M'(s) = -M(s - 1).

The conserved quantity

noncomputable def IwaniecLinearSieve.lemma5Q (s : ℝ) : ℝ

Q(s) = (s - 1) M(s) - ∫_{s-1}^s M.

Equations

• IwaniecLinearSieve.lemma5Q s = (s - 1) * IwaniecLinearSieve.MSieve s - ∫ (x : ℝ) in s - 1..s, IwaniecLinearSieve.MSieve x

theorem IwaniecLinearSieve.lemma5Q_eq (s : ℝ) : lemma5Q s = (s - 1) * MSieve s - ((∫ (x : ℝ) in 0..s, MSieve x) - ∫ (x : ℝ) in 0..s - 1, MSieve x)

theorem IwaniecLinearSieve.continuous_lemma5Q : Continuous lemma5Q

theorem IwaniecLinearSieve.hasDerivAt_lemma5Q {s : ℝ} (hs3 : 3 < s) (hs4 : s ≠ 4) : HasDerivAt lemma5Q 0 s

theorem IwaniecLinearSieve.lemma5Q_eq_of_deriv {a b : ℝ} (hab : a ≤ b) (hd : ∀ x ∈ Set.Ioo a b, HasDerivAt lemma5Q 0 x) : lemma5Q b = lemma5Q a

theorem IwaniecLinearSieve.lemma5Q_const {b : ℝ} (hb : 3 ≤ b) : lemma5Q b = lemma5Q 3

theorem IwaniecLinearSieve.abs_lemma5Q_le {b : ℝ} (hb : 4 ≤ b) : |lemma5Q b| ≤ (gLead * (1 - gRatio)⁻¹ + gLead * (Real.exp 1 / 3) * (1 - gRatio)⁻¹) * Real.exp 1 * (b ^ 2 * Real.exp (-b))

theorem IwaniecLinearSieve.lemma5Q_three : lemma5Q 3 = 0

f(2) = 2

theorem IwaniecLinearSieve.integral_MSieve_two_three : ∫ (x : ℝ) in 2..3, MSieve x = FSieve 3 - 1 + fSieve 4 + (FSieve 3 + 3) * (2 * (Real.log 3 - Real.log 2) - Real.log 3 + 1)

∫_2^3 M = F(3) - 1 + f(4) + (F(3) + 3)(2 log (3/2) - log 3 + 1).

theorem IwaniecLinearSieve.fSieve_four_add : fSieve 4 + (FSieve 3 + 3) * Real.log 3 = 4

The key identity f(4) + (F(3) + 3) log 3 = 4.

theorem IwaniecLinearSieve.fSieve_eq_on_Icc {s : ℝ} (hs : s ∈ Set.Icc 2 4) : fSieve s = s - (FSieve 3 + 3) * Real.log (s - 1)

[I71, Lemma 5] in the form we need: f(s) = s - (F(3) + 3) log (s - 1) for 2 ≤ s ≤ 4 (Iwaniec: F(3) + 3 = 2e^γ).

theorem IwaniecLinearSieve.fSieve_two : fSieve 2 = 2

[I71, (3.10)]: f(2) = 2.

theorem IwaniecLinearSieve.le_one_sub_fSieve_div {s : ℝ} (hs : s ∈ Set.Icc 2 4) : 3 * Real.log (s - 1) / s ≤ 1 - fSieve s / s

The consequence of Lemma 5 used for the sieve: 1 - f(s)/s ≥ 3 log (s - 1) / s on [2, 4].

theorem IwaniecLinearSieve.one_sub_fSieve_div_ge (s : ℝ) : s ∈ Set.Icc 2 4 → 1 - fSieve s / s ≥ 3 * Real.log (s - 1) / s

le_one_sub_fSieve_div in the form used by the linear-sieve modules.