Lemmas 3 and 4 of [I71, §3]

• Lemma 3: ψ(s) = s⁻¹ e^{s-3} (1 + 3 log (3/(s-1))) satisfies ψ(s) ≤ ψ(2) on [2, 4].
• Lemma 4: with a = sup_{2 ≤ s ≤ 4} g₂(s) s⁻¹ eˢ (gLead) and A = (e/3) ψ(2) = (1 + 3 log 3)/6 < 0.72 (gRatio), g_{2n+1}(s) ≤ a (e/3) A^{n-1} s e^{-s} for s ≥ 1, n ≥ 1 (3.4), and g_{2n+2}(s) ≤ a Aⁿ s e^{-s} for s ≥ 2, n ≥ 0 (3.5).

Numerical facts

theorem IwaniecLinearSieve.log_three_sub_log_two_lt : Real.log 3 - Real.log 2 < 5 / 12

theorem IwaniecLinearSieve.one_lt_log_three : 1 < Real.log 3

theorem IwaniecLinearSieve.exp_one_sq_lt : Real.exp 1 ^ 2 < 2 + 6 * Real.log 3

theorem IwaniecLinearSieve.mul_exp_neg_le_of_one_le {u v : ℝ} (hu : 1 ≤ u) (huv : u ≤ v) : v * Real.exp (-v) ≤ u * Real.exp (-u)

s e^{-s} is decreasing for s ≥ 1.

Lemma 3

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

Iwaniec's ψ(s) = s⁻¹ e^{s-3} (1 + 3 log (3/(s-1))) [I71, Lemma 3].

Equations

• IwaniecLinearSieve.psi s = s⁻¹ * Real.exp (s - 3) * (1 + 3 * Real.log (3 / (s - 1)))

theorem IwaniecLinearSieve.psi_two : psi 2 = (1 + 3 * Real.log 3) / (2 * Real.exp 1)

theorem IwaniecLinearSieve.psi_deriv_aux {x : ℝ} (hx : 2 < x) : (x - 1) * (1 + 3 * Real.log (3 / (x - 1))) ≤ 3 * x / (x - 1)

The key inequality behind Lemma 3: (x-1)(1 + 3 log (3/(x-1))) ≤ 3x/(x-1) on (2, 4).

theorem IwaniecLinearSieve.hasDerivAt_psi {x : ℝ} (hx : 1 < x) : HasDerivAt psi (Real.exp (x - 3) * ((x - 1) * (1 + 3 * Real.log (3 / (x - 1))) - 3 * x / (x - 1)) / x ^ 2) x

theorem IwaniecLinearSieve.psi_le_psi_two {s : ℝ} (hs : s ∈ Set.Icc 2 4) : psi s ≤ psi 2

[I71, Lemma 3]: ψ(s) ≤ ψ(2) for 2 ≤ s ≤ 4.

Lemma 4

noncomputable def IwaniecLinearSieve.gLead : ℝ

Iwaniec's constant a = sup_{2 ≤ s ≤ 4} g₂(s) s⁻¹ eˢ [I71, Lemma 4].

Equations

• IwaniecLinearSieve.gLead = sSup ((fun (s : ℝ) => IwaniecLinearSieve.g 2 s * s⁻¹ * Real.exp s) '' Set.Icc 2 4)

noncomputable def IwaniecLinearSieve.gRatio : ℝ

Iwaniec's constant A = (e/3) ψ(2) = (1 + 3 log 3)/6 [I71, Lemma 4].

Equations

• IwaniecLinearSieve.gRatio = (1 + 3 * Real.log 3) / 6

theorem IwaniecLinearSieve.gRatio_eq : gRatio = Real.exp 1 / 3 * psi 2

theorem IwaniecLinearSieve.gRatio_lt : gRatio < 0.72

theorem IwaniecLinearSieve.gRatio_pos : 0 < gRatio

theorem IwaniecLinearSieve.gRatio_lt_one : gRatio < 1

theorem IwaniecLinearSieve.bddAbove_gLead : BddAbove ((fun (s : ℝ) => g 2 s * s⁻¹ * Real.exp s) '' Set.Icc 2 4)

theorem IwaniecLinearSieve.le_gLead {s : ℝ} (hs : s ∈ Set.Icc 2 4) : g 2 s * s⁻¹ * Real.exp s ≤ gLead

theorem IwaniecLinearSieve.gLead_nonneg : 0 ≤ gLead

theorem IwaniecLinearSieve.integral_shift_le {h : ℝ → ℝ} (hh : Continuous h) {C s b : ℝ} (hC : 0 ≤ C) (hs : 2 ≤ s) (hsb : s ≤ b) (hb : ∀ (u : ℝ), s - 1 ≤ u → h u ≤ C * u * Real.exp (-u)) : ∫ (t : ℝ) in s..b, h (t - 1) / (t - 1) ≤ C * Real.exp (1 - s)

If h(u) ≤ C u e^{-u} for u ≥ s - 1, then ∫_s^b h(t-1)/(t-1) dt ≤ C e^{1-s}.

theorem IwaniecLinearSieve.g_add_three_le {n : ℕ} {C s : ℝ} (hC : 0 ≤ C) (hs : gLower (n + 3) ≤ s) (hb : ∀ (u : ℝ), s - 1 ≤ u → g (n + 2) u ≤ C * u * Real.exp (-u)) : g (n + 3) s ≤ C * Real.exp (1 - s)

The inductive step of [I71, Lemma 4] in uniform form.

theorem IwaniecLinearSieve.gLower_two_mul_add_three (n : ℕ) : gLower (2 * n + 3) = 3

theorem IwaniecLinearSieve.gLower_two_mul_add_four (n : ℕ) : gLower (2 * n + 1 + 3) = 2

theorem IwaniecLinearSieve.g_even_eq_on_Icc (n : ℕ) {s : ℝ} (hs : s ∈ Set.Icc 2 4) : g (2 * n + 4) s = g (2 * n + 4) 4 + g (2 * n + 3) 3 * Real.log (3 / (s - 1))

For 2 ≤ s ≤ 4: g_{2n+4}(s) = g_{2n+4}(4) + g_{2n+3}(3) log (3/(s-1)) (proof of [I71, Lemma 4]).

theorem IwaniecLinearSieve.g_even_le (n : ℕ) {s : ℝ} (hs : 2 ≤ s) : g (2 * n + 2) s ≤ gLead * gRatio ^ n * s * Real.exp (-s)

(3.5) of [I71, Lemma 4]: g_{2n+2}(s) ≤ a Aⁿ s e^{-s} for s ≥ 2, n ≥ 0.

theorem IwaniecLinearSieve.g_odd_le (n : ℕ) {s : ℝ} (hs : 1 ≤ s) : g (2 * n + 3) s ≤ gLead * (Real.exp 1 / 3) * gRatio ^ n * s * Real.exp (-s)

(3.4) of [I71, Lemma 4] (with n shifted by one): g_{2n+3}(s) ≤ a (e/3) Aⁿ s e^{-s} for s ≥ 1.

theorem IwaniecLinearSieve.g_odd_le' {n : ℕ} (hn : 1 ≤ n) {s : ℝ} (hs : 1 ≤ s) : g (2 * n + 1) s ≤ gLead * (Real.exp 1 / 3) * gRatio ^ (n - 1) * s * Real.exp (-s)

(3.4) of [I71, Lemma 4]: g_{2n+1}(s) ≤ a (e/3) A^{n-1} s e^{-s} for s ≥ 1, n ≥ 1.