The functions g_n of [I71, §3]

Iwaniec's functions g_n (n ≥ 2) of [I71, (3.1)–(3.3)], defined on all of ℝ in IwaniecLinearSieve.Definitions, are:

• g 2 s = 3 log (3 / (s - 1)) + s - 4 for 2 ≤ s ≤ 4 and g 2 s = 0 for s ≥ 4;
• g (2n+1) s = ∫_s^∞ g (2n) (t-1) / (t-1) dt for s ≥ 3 and g (2n+1) s = g (2n+1) 3 for s ≤ 3;
• g (2n+2) s = ∫_s^∞ g (2n+1) (t-1) / (t-1) dt for s ≥ 2.

Outside the domains of [I71] the argument is clamped (g 2 and the even functions are constant on s ≤ 2, the odd functions on s ≤ 3), and g 0 = g 1 = 0. With these conventions every g i is continuous, nonnegative and antitone on all of ℝ, and g i s = 0 for s ≥ i + 2.

theorem IwaniecLinearSieve.g_zero (s : ℝ) : g 0 s = 0

theorem IwaniecLinearSieve.g_one (s : ℝ) : g 1 s = 0

theorem IwaniecLinearSieve.g_two_def (s : ℝ) : g 2 s = gTwoFormula (max 2 (min s 4))

theorem IwaniecLinearSieve.g_add_three (n : ℕ) (s : ℝ) : g (n + 3) s = ∫ (t : ℝ) in max s (gLower (n + 3))..↑n + 5, shiftKernel (g (n + 2)) t

theorem IwaniecLinearSieve.gLower_le_three (i : ℕ) : gLower i ≤ 3

theorem IwaniecLinearSieve.two_le_gLower (i : ℕ) : 2 ≤ gLower i

theorem IwaniecLinearSieve.gLower_even {i : ℕ} (hi : Even i) : gLower i = 2

theorem IwaniecLinearSieve.gLower_odd {i : ℕ} (hi : ¬Even i) : gLower i = 3

theorem IwaniecLinearSieve.shiftKernel_of_two_le (h : ℝ → ℝ) {t : ℝ} (ht : 2 ≤ t) : shiftKernel h t = h (t - 1) / (t - 1)

theorem IwaniecLinearSieve.continuous_shiftKernel {h : ℝ → ℝ} (hh : Continuous h) : Continuous (shiftKernel h)

theorem IwaniecLinearSieve.shiftKernel_nonneg {h : ℝ → ℝ} (hh : ∀ (s : ℝ), 0 ≤ h s) (t : ℝ) : 0 ≤ shiftKernel h t

theorem IwaniecLinearSieve.continuous_integral_left {k : ℝ → ℝ} (hk : Continuous k) (b : ℝ) : Continuous fun (u : ℝ) => ∫ (t : ℝ) in u..b, k t

g₂

theorem IwaniecLinearSieve.gTwoFormula_four : gTwoFormula 4 = 0

theorem IwaniecLinearSieve.gTwoFormula_continuousOn : ContinuousOn gTwoFormula (Set.Icc 2 4)

theorem IwaniecLinearSieve.gTwoFormula_sub_ge {u v : ℝ} (hu : 2 ≤ u) (huv : u ≤ v) (hv : v ≤ 4) : (v - u) * (4 - v) / (v - 1) ≤ gTwoFormula u - gTwoFormula v ∧ (u < v → 0 < gTwoFormula u - gTwoFormula v)

gTwoFormula u - gTwoFormula v ≥ 0 for 2 ≤ u ≤ v ≤ 4, with strictness when u < v.

theorem IwaniecLinearSieve.gTwoFormula_nonneg {u : ℝ} (hu : 2 ≤ u) (hu4 : u ≤ 4) : 0 ≤ gTwoFormula u

theorem IwaniecLinearSieve.gTwoFormula_pos {u : ℝ} (hu : 2 ≤ u) (hu4 : u < 4) : 0 < gTwoFormula u

Basic properties of g

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

[I71, (3.1)] on [2, 4].

theorem IwaniecLinearSieve.g_two_of_four_le {s : ℝ} (hs : 4 ≤ s) : g 2 s = 0

[I71, (3.1)] for s ≥ 4.

theorem IwaniecLinearSieve.g_eq_of_le_gLower (i : ℕ) {s : ℝ} (hs : s ≤ gLower i) : g i s = g i (gLower i)

theorem IwaniecLinearSieve.g_add_three_eq (n : ℕ) {s : ℝ} (hs : gLower (n + 3) ≤ s) : g (n + 3) s = ∫ (t : ℝ) in s..↑n + 5, g (n + 2) (t - 1) / (t - 1)

theorem IwaniecLinearSieve.continuous_g (i : ℕ) : Continuous (g i)

theorem IwaniecLinearSieve.g_eq_zero_of_le (i : ℕ) {s : ℝ} : ↑i + 2 ≤ s → g i s = 0

g i s = 0 for s ≥ i + 2 ([I71], remark after (3.3)).

theorem IwaniecLinearSieve.g_nonneg (i : ℕ) (s : ℝ) : 0 ≤ g i s

theorem IwaniecLinearSieve.g_pos (i : ℕ) : 2 ≤ i → ∀ {s : ℝ}, s < ↑i + 2 → 0 < g i s

g i s > 0 for i ≥ 2 and s < i + 2.

theorem IwaniecLinearSieve.g_antitone (i : ℕ) : Antitone (g i)

theorem IwaniecLinearSieve.g_add_three_sub (n : ℕ) {u v : ℝ} (hu : gLower (n + 3) ≤ u) (hv : gLower (n + 3) ≤ v) : g (n + 3) u - g (n + 3) v = ∫ (t : ℝ) in u..v, shiftKernel (g (n + 2)) t

Differences of g (n + 3) are integrals of the kernel.

Improper integrals

theorem IwaniecLinearSieve.integral_Ioi_eq_of_eq_zero {h : ℝ → ℝ} {s b : ℝ} (hsb : s ≤ b) (hint : MeasureTheory.IntegrableOn h (Set.Ioc s b) MeasureTheory.volume) (hz : ∀ (t : ℝ), b ≤ t → h t = 0) : MeasureTheory.IntegrableOn h (Set.Ioi s) MeasureTheory.volume ∧ ∫ (t : ℝ) in Set.Ioi s, h t = ∫ (t : ℝ) in s..b, h t

If h is integrable on (s, b] and vanishes on [b, ∞), then it is integrable on (s, ∞) and its integral there is ∫_s^b h.

theorem IwaniecLinearSieve.g_add_three_eq_Ioi (n : ℕ) {s : ℝ} (hs : gLower (n + 3) ≤ s) : MeasureTheory.IntegrableOn (fun (t : ℝ) => g (n + 2) (t - 1) / (t - 1)) (Set.Ioi s) MeasureTheory.volume ∧ g (n + 3) s = ∫ (t : ℝ) in Set.Ioi s, g (n + 2) (t - 1) / (t - 1)

The identities (3.2), (3.3) in the form of [I71]

theorem IwaniecLinearSieve.not_even_two_mul_add_three (m : ℕ) : ¬Even (2 * m + 3)

theorem IwaniecLinearSieve.even_two_mul_add_four (m : ℕ) : Even (2 * m + 4)

theorem IwaniecLinearSieve.g_odd_eq_integral {n : ℕ} (hn : 1 ≤ n) {s : ℝ} (hs : 3 ≤ s) : MeasureTheory.IntegrableOn (fun (t : ℝ) => g (2 * n) (t - 1) / (t - 1)) (Set.Ioi s) MeasureTheory.volume ∧ g (2 * n + 1) s = ∫ (t : ℝ) in Set.Ioi s, g (2 * n) (t - 1) / (t - 1)

[I71, (3.2)], first line: g_{2n+1}(s) = ∫_s^∞ g_{2n}(t-1)/(t-1) dt for s ≥ 3.

theorem IwaniecLinearSieve.g_odd_of_le_three (n : ℕ) {s : ℝ} (hs : s ≤ 3) : g (2 * n + 1) s = g (2 * n + 1) 3

[I71, (3.2)], second line: g_{2n+1}(s) = g_{2n+1}(3) for s ≤ 3.

theorem IwaniecLinearSieve.g_even_eq_integral {n : ℕ} (hn : 1 ≤ n) {s : ℝ} (hs : 2 ≤ s) : MeasureTheory.IntegrableOn (fun (t : ℝ) => g (2 * n + 1) (t - 1) / (t - 1)) (Set.Ioi s) MeasureTheory.volume ∧ g (2 * n + 2) s = ∫ (t : ℝ) in Set.Ioi s, g (2 * n + 1) (t - 1) / (t - 1)

[I71, (3.3)]: g_{2n+2}(s) = ∫_s^∞ g_{2n+1}(t-1)/(t-1) dt for s ≥ 2.

theorem IwaniecLinearSieve.g_even_of_le_two (n : ℕ) {s : ℝ} (hs : s ≤ 2) : g (2 * n + 2) s = g (2 * n + 2) 2

Even g are constant on s ≤ 2.