The functions 𝔣, 𝔉, G_r ([I71, §3])

𝔣 = (𝔐 + 𝔚)/2, 𝔉 = (𝔐 - 𝔚)/2; G_r = 𝔣 for r even and 𝔉 for r odd. We prove (3.13), (3.14), the Corollary to Lemma 6, and positivity, continuity and monotonicity.

With our extension of 𝔐, 𝔚 to ℝ, 𝔉 = 1 on (-∞, 3] (as in [I71], where 𝔉 = 1 on [1, 3]), and 𝔣 = 2 on (-∞, 2].

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

Iwaniec's 𝔣 = (𝔐 + 𝔚)/2.

Equations

• IwaniecLinearSieve.majf s = (IwaniecLinearSieve.bigM s + IwaniecLinearSieve.bigW s) / 2

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

Iwaniec's 𝔉 = (𝔐 - 𝔚)/2.

Equations

• IwaniecLinearSieve.majF s = (IwaniecLinearSieve.bigM s - IwaniecLinearSieve.bigW s) / 2

noncomputable def IwaniecLinearSieve.majG (r : ℕ) (s : ℝ) : ℝ

Iwaniec's G_r: 𝔣 for r even, 𝔉 for r odd.

Equations

• IwaniecLinearSieve.majG r s = if Even r then IwaniecLinearSieve.majf s else IwaniecLinearSieve.majF s

theorem IwaniecLinearSieve.majG_of_even {r : ℕ} (hr : Even r) : majG r = majf

theorem IwaniecLinearSieve.majG_of_odd {r : ℕ} (hr : Odd r) : majG r = majF

theorem IwaniecLinearSieve.continuous_majf : Continuous majf

theorem IwaniecLinearSieve.continuous_majF : Continuous majF

theorem IwaniecLinearSieve.continuous_majG (r : ℕ) : Continuous (majG r)

theorem IwaniecLinearSieve.majF_of_le_three {s : ℝ} (hs : s ≤ 3) : majF s = 1

𝔉 = 1 for s ≤ 3.

theorem IwaniecLinearSieve.majf_eq {s : ℝ} (hs : 2 ≤ s) (hs' : s ≤ 3) : majf s = 1 + 1 / (s - 1) - Real.log (s - 1)

𝔣(s) = 1 + 1/(s-1) - log(s-1) for 2 ≤ s ≤ 3.

theorem IwaniecLinearSieve.majf_of_le_two {s : ℝ} (hs : s ≤ 2) : majf s = 2

theorem IwaniecLinearSieve.majf_mem (s : ℝ) : bigM s / 3 ≤ majf s ∧ majf s ≤ 2 * bigM s / 3

Corollary to [I71, Lemma 6]: 𝔐/3 ≤ 𝔣 ≤ 2𝔐/3.

theorem IwaniecLinearSieve.majF_mem (s : ℝ) : bigM s / 3 ≤ majF s ∧ majF s ≤ 2 * bigM s / 3

Corollary to [I71, Lemma 6]: 𝔐/3 ≤ 𝔉 ≤ 2𝔐/3.

theorem IwaniecLinearSieve.majG_mem (r : ℕ) (s : ℝ) : bigM s / 3 ≤ majG r s ∧ majG r s ≤ 2 * bigM s / 3

Corollary to [I71, Lemma 6] for G_r.

theorem IwaniecLinearSieve.majG_le_two (r : ℕ) (s : ℝ) : majG r s ≤ 2

theorem IwaniecLinearSieve.majG_pos (r : ℕ) (s : ℝ) : 0 < majG r s

theorem IwaniecLinearSieve.majf_pos (s : ℝ) : 0 < majf s

theorem IwaniecLinearSieve.majF_pos (s : ℝ) : 0 < majF s

Derivatives

theorem IwaniecLinearSieve.hasDerivAt_majF {s : ℝ} (hs : 3 < s) : HasDerivAt majF (-(s / (s - 1) ^ 2 * majf (s - 1))) s

theorem IwaniecLinearSieve.hasDerivWithinAt_majf_Ici {s : ℝ} (hs : 3 ≤ s) : HasDerivWithinAt majf (-(s / (s - 1) ^ 2 * majF (s - 1))) (Set.Ici s) s

theorem IwaniecLinearSieve.hasDerivAt_majf {s : ℝ} (hs : 2 < s) : HasDerivAt majf (-(s / (s - 1) ^ 2 * majF (s - 1))) s

𝔣' (s) = -s/(s-1)² 𝔉(s-1) for s > 2.

theorem IwaniecLinearSieve.hasDerivAt_majG_succ (r : ℕ) {t : ℝ} (ht : (5 + (-1) ^ r) / 2 < t) : HasDerivAt (majG (r + 1)) (-(majG r (t - 1) * t / (t - 1) ^ 2)) t

The derivative of G_{r+1} is -G_r(t-1) t/(t-1)², for t > 3, and for t > 2 if r is odd; i.e. for t > (5 + (-1)^r)/2 as in [I71, proof of Lemma 11].

Monotonicity

theorem IwaniecLinearSieve.majF_antitone : Antitone majF

theorem IwaniecLinearSieve.majf_antitone : Antitone majf

theorem IwaniecLinearSieve.majG_antitone (r : ℕ) : Antitone (majG r)

[I71, Remark after Lemma 6]: G_r is decreasing.

(3.13), (3.14)

theorem IwaniecLinearSieve.tendsto_majG_atTop (r : ℕ) : Filter.Tendsto (majG r) Filter.atTop (nhds 0)

theorem IwaniecLinearSieve.tendsto_majf_atTop : Filter.Tendsto majf Filter.atTop (nhds 0)

theorem IwaniecLinearSieve.tendsto_majF_atTop : Filter.Tendsto majF Filter.atTop (nhds 0)

theorem IwaniecLinearSieve.majF_eq_integral {s : ℝ} (hs : 3 ≤ s) : majF s = ∫ (t : ℝ) in Set.Ioi s, majf (t - 1) * t / (t - 1) ^ 2

[I71, (3.13)]: 𝔉(s) = ∫_s^∞ 𝔣(t-1) t/(t-1)² dt for s ≥ 3.

theorem IwaniecLinearSieve.majf_eq_integral {s : ℝ} (hs : 2 ≤ s) : majf s = ∫ (t : ℝ) in Set.Ioi s, majF (t - 1) * t / (t - 1) ^ 2

[I71, (3.14)]: 𝔣(s) = ∫_s^∞ 𝔉(t-1) t/(t-1)² dt for s ≥ 2.