[I71, Lemma 7]: f_r(s) < M(s) < 4 𝔐(s) for s ≥ 2

Here M = MSieve = f + F + (3 - ·)⁺. On [2, 3], M(s) = (F(3) + 3)(1 - log (s - 1)) by (3.9), and F(3) + 3 < 4 by fSieve_four_add. For s > 3 we follow [I71]: at a first crossing s, (s-1) M(s) = ∫_{s-1}^s M ≤ 4 ∫_{s-1}^s 𝔐 ≤ 4 (s-1)² 𝔐(s) / s < 4 (s-1) 𝔐(s), using lemma5Q = 0 and (3.12).

The bound M(s) ≤ 4𝔐(s) fails for s < 2, where M(s) = 5 + F(3) - s grows and 𝔐 = 3.

Consequences used in the induction of [I71, §4] (with Lemma 8 and the Corollary to Lemma 6): mainMaj_le_errMaj : 2 ≤ s → M lower (s) ≤ 12 G lower' (s) and mainMaj_sub_one_le : 1 ≤ s → M lower (s - 1) ≤ 48 s² G lower' (s).

theorem IwaniecLinearSieve.FSieve_three_add_lt_four : FSieve 3 + 3 < 4

F(3) + 3 < 4, from f(4) + (F(3) + 3) log 3 = 4.

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

theorem IwaniecLinearSieve.MSieve_lt_four_mul_bigM_of_le_three {s : ℝ} (hs : s ∈ Set.Icc 2 3) : MSieve s < 4 * bigM s

theorem IwaniecLinearSieve.sub_one_mul_MSieve {s : ℝ} (hs : 3 ≤ s) : (s - 1) * MSieve s = ∫ (x : ℝ) in s - 1..s, MSieve x

(s - 1) M(s) = ∫_{s-1}^s M for s ≥ 3 (this is lemma5Q s = 0).

theorem IwaniecLinearSieve.integral_bigM_le {s : ℝ} (hs : 3 ≤ s) : ∫ (x : ℝ) in s - 1..s, bigM x ≤ (s - 1) ^ 2 * bigM s / s

∫_{s-1}^s 𝔐 ≤ (s-1)² 𝔐(s)/s for s ≥ 3, from (3.12).

theorem IwaniecLinearSieve.MSieve_lt_four_mul_bigM {s : ℝ} (hs : 2 ≤ s) : MSieve s < 4 * bigM s

[I71, Lemma 7], upper bound: M(s) < 4 𝔐(s) for s ≥ 2.

theorem IwaniecLinearSieve.lemma7 (r : ℕ) {s : ℝ} (hs : 2 ≤ s) : fr r s < MSieve s ∧ MSieve s ≤ 4 * bigM s

[I71, Lemma 7]: f_r(s) < M(s) ≤ 4 𝔐(s) for s ≥ 2.

theorem IwaniecLinearSieve.mainMaj_lt_four_mul_bigM (lower : Bool) {s : ℝ} (hs : 2 ≤ s) : mainMaj lower s < 4 * bigM s

theorem IwaniecLinearSieve.mainMaj_le_errMaj (lower lower' : Bool) {s : ℝ} (hs : 2 ≤ s) : mainMaj lower s ≤ 12 * errMaj lower' s

M lower (s) ≤ 12 G lower' (s) for s ≥ 2.

theorem IwaniecLinearSieve.MSieve_sub_one_lt {s : ℝ} (hs : 3 ≤ s) : MSieve (s - 1) < 16 * s ^ 2 * bigM s

M(s - 1) < 16 s² 𝔐(s) for s ≥ 3 (Lemmas 7 and 8).

theorem IwaniecLinearSieve.bigM_three_gt : 3 / 2 < bigM 3

theorem IwaniecLinearSieve.mainMaj_sub_one_le (lower lower' : Bool) {s : ℝ} (hs : 1 ≤ s) : mainMaj lower (s - 1) ≤ 48 * s ^ 2 * errMaj lower' s

The comparison of Corollary 1's error term with the error majorant: M lower (s - 1) ≤ 48 s² G lower' (s) for s ≥ 1 (any flags).