The functions f and F of [I71, §3]

f(s) = Σ_{i ≥ 1} g_{2i}(s) (fSieve) and F(s) = Σ_{i ≥ 1} g_{2i+1}(s) (FSieve), defined in IwaniecLinearSieve.Definitions. This module proves the Corollary to Lemma 4 of [I71]: convergence (with geometric majorants), continuity, positivity, f, F = O(s e^{-s}), and the integral equations (3.6), (3.7).

Since the g_i are clamped (see IwaniecLinearSieve.SieveFunctions.Defs), the series converge for all real s; f is constant on s ≤ 2 and F on s ≤ 3.

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

f_r = f for even r and F for odd r ([I71], before Lemma 7).

Equations

• IwaniecLinearSieve.fr r s = if Even r then IwaniecLinearSieve.fSieve s else IwaniecLinearSieve.FSieve s

Clamping and uniform bounds

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

theorem IwaniecLinearSieve.g_even_le_at_two (n : ℕ) (s : ℝ) : g (2 * n + 2) s ≤ g (2 * n + 2) 2

theorem IwaniecLinearSieve.g_odd_le_at_three (n : ℕ) (s : ℝ) : g (2 * n + 3) s ≤ g (2 * n + 3) 3

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

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

theorem IwaniecLinearSieve.summable_geom_gRatio (c : ℝ) : Summable fun (n : ℕ) => c * gRatio ^ n

theorem IwaniecLinearSieve.summable_g_even (s : ℝ) : Summable fun (n : ℕ) => g (2 * n + 2) s

theorem IwaniecLinearSieve.summable_g_odd (s : ℝ) : Summable fun (n : ℕ) => g (2 * n + 3) s

Basic properties of f and F

theorem IwaniecLinearSieve.continuous_fSieve : Continuous fSieve

theorem IwaniecLinearSieve.continuous_FSieve : Continuous FSieve

theorem IwaniecLinearSieve.fSieve_nonneg (s : ℝ) : 0 ≤ fSieve s

theorem IwaniecLinearSieve.FSieve_nonneg (s : ℝ) : 0 ≤ FSieve s

theorem IwaniecLinearSieve.fSieve_pos (s : ℝ) : 0 < fSieve s

theorem IwaniecLinearSieve.FSieve_pos (s : ℝ) : 0 < FSieve s

theorem IwaniecLinearSieve.fSieve_antitone : Antitone fSieve

theorem IwaniecLinearSieve.FSieve_antitone : Antitone FSieve

theorem IwaniecLinearSieve.fSieve_of_le_two {s : ℝ} (hs : s ≤ 2) : fSieve s = fSieve 2

theorem IwaniecLinearSieve.FSieve_of_le_three {s : ℝ} (hs : s ≤ 3) : FSieve s = FSieve 3

[I71, (3.7)], second line: F(s) = F(3) for s ≤ 3.

theorem IwaniecLinearSieve.fSieve_le {s : ℝ} (hs : 2 ≤ s) : fSieve s ≤ gLead * (1 - gRatio)⁻¹ * s * Real.exp (-s)

f(s) ≤ a (1 - A)⁻¹ s e^{-s} for s ≥ 2.

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

F(s) ≤ a (e/3) (1 - A)⁻¹ s e^{-s} for s ≥ 1.

theorem IwaniecLinearSieve.fSieve_isBigO : fSieve =O[Filter.atTop] fun (s : ℝ) => s * Real.exp (-s)

theorem IwaniecLinearSieve.FSieve_isBigO : FSieve =O[Filter.atTop] fun (s : ℝ) => s * Real.exp (-s)

theorem IwaniecLinearSieve.g_even_le_fSieve (n : ℕ) (s : ℝ) : g (2 * n + 2) s ≤ fSieve s

theorem IwaniecLinearSieve.g_odd_le_FSieve (n : ℕ) (s : ℝ) : g (2 * n + 3) s ≤ FSieve s

theorem IwaniecLinearSieve.sum_g_even_le_fSieve (N : ℕ) (s : ℝ) : ∑ n ∈ Finset.range N, g (2 * n + 2) s ≤ fSieve s

Partial sums of the series for f are at most f.

theorem IwaniecLinearSieve.sum_g_odd_le_FSieve (N : ℕ) (s : ℝ) : ∑ n ∈ Finset.range N, g (2 * n + 3) s ≤ FSieve s

Partial sums of the series for F are at most F.

theorem IwaniecLinearSieve.hasSum_g_fSieve (s : ℝ) : HasSum (fun (n : ℕ) => g (2 * n + 2) s) (fSieve s)

theorem IwaniecLinearSieve.hasSum_g_FSieve (s : ℝ) : HasSum (fun (n : ℕ) => g (2 * n + 3) s) (FSieve s)

theorem IwaniecLinearSieve.hasSum_g (s : ℝ) : HasSum (fun (k : ℕ) => g (k + 2) s) (fSieve s + FSieve s)

Σ_{k ≥ 2} g_k(s) = f(s) + F(s).

theorem IwaniecLinearSieve.fr_of_even {r : ℕ} (hr : Even r) : fr r = fSieve

theorem IwaniecLinearSieve.fr_of_odd {r : ℕ} (hr : ¬Even r) : fr r = FSieve

The integral equations (3.6), (3.7)

theorem IwaniecLinearSieve.shift_div_le {h : ℝ → ℝ} {C t : ℝ} (ht : 1 < t) (hb : h (t - 1) ≤ C * (t - 1) * Real.exp (-(t - 1))) : h (t - 1) / (t - 1) ≤ C * Real.exp 1 * Real.exp (-t)

theorem IwaniecLinearSieve.integrableOn_shift {h : ℝ → ℝ} (hh : Continuous h) {C s : ℝ} (hs : 2 ≤ s) (hnn : ∀ (u : ℝ), 0 ≤ h u) (hb : ∀ (u : ℝ), s - 1 ≤ u → h u ≤ C * u * Real.exp (-u)) : MeasureTheory.IntegrableOn (fun (t : ℝ) => h (t - 1) / (t - 1)) (Set.Ioi s) MeasureTheory.volume

An exponentially decaying h gives an integrable kernel h(t-1)/(t-1) on (s, ∞).

theorem IwaniecLinearSieve.tsum_integral_Ioi_shift {φ : ℕ → ℝ → ℝ} {s : ℝ} (hs : 2 ≤ s) (hnn : ∀ (n : ℕ) (x : ℝ), 0 ≤ φ n x) (hint : ∀ (n : ℕ), MeasureTheory.IntegrableOn (fun (t : ℝ) => φ n (t - 1) / (t - 1)) (Set.Ioi s) MeasureTheory.volume) (hsum : Summable fun (n : ℕ) => ∫ (t : ℝ) in Set.Ioi s, φ n (t - 1) / (t - 1)) : ∑' (n : ℕ), ∫ (t : ℝ) in Set.Ioi s, φ n (t - 1) / (t - 1) = ∫ (t : ℝ) in Set.Ioi s, (∑' (n : ℕ), φ n (t - 1)) / (t - 1)

Interchange of Σ and ∫_s^∞ for nonnegative kernels.

theorem IwaniecLinearSieve.integrableOn_FSieve_shift {s : ℝ} (hs : 2 ≤ s) : MeasureTheory.IntegrableOn (fun (t : ℝ) => FSieve (t - 1) / (t - 1)) (Set.Ioi s) MeasureTheory.volume

theorem IwaniecLinearSieve.integrableOn_fSieve_shift {s : ℝ} (hs : 3 ≤ s) : MeasureTheory.IntegrableOn (fun (t : ℝ) => fSieve (t - 1) / (t - 1)) (Set.Ioi s) MeasureTheory.volume

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

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

theorem IwaniecLinearSieve.fSieve_eq_integral {s : ℝ} (hs : 2 ≤ s) : fSieve s = (∫ (t : ℝ) in Set.Ioi s, FSieve (t - 1) / (t - 1)) + g 2 s

[I71, (3.6)]: f(s) = ∫_s^∞ F(t-1)/(t-1) dt + g₂(s) for s ≥ 2.

theorem IwaniecLinearSieve.FSieve_eq_integral {s : ℝ} (hs : 3 ≤ s) : FSieve s = ∫ (t : ℝ) in Set.Ioi s, fSieve (t - 1) / (t - 1)

[I71, (3.7)], first line: F(s) = ∫_s^∞ f(t-1)/(t-1) dt for s ≥ 3.