Basic properties of 𝔐, 𝔚 ([I71, §3])

0 < 𝔐, 𝔐 antitone, 𝔐 = O(e^{-s}), and [I71, Lemma 6] |𝔚| ≤ 𝔐/3.

theorem IwaniecLinearSieve.initW_mem {s : ℝ} (hs : s ≤ 3) : -(1 / 2) ≤ initW s ∧ initW s ≤ 1

On (-∞, 3], -1/2 ≤ 𝔚 ≤ 1.

theorem IwaniecLinearSieve.bigM_pos_of_le_three {s : ℝ} (hs : s ≤ 3) : 0 < bigM s

theorem IwaniecLinearSieve.abs_bigW_le_of_le_three {s : ℝ} (hs : s ≤ 3) : |bigW s| ≤ bigM s / 3

theorem IwaniecLinearSieve.weight_mem {x : ℝ} (hx : 1 ≤ x) : 0 < 1 - 1 / (2 * x ^ 2) ∧ 1 - 1 / (2 * x ^ 2) ≤ 1

The weight 1 - 1/(2x²) of (3.12) is in (0, 1] for x ≥ 1.

theorem IwaniecLinearSieve.continuousOn_weight_mul {g : ℝ → ℝ} (hg : Continuous g) {a b : ℝ} (ha : 0 < a) : ContinuousOn (fun (x : ℝ) => (1 - 1 / (2 * x ^ 2)) * g x) (Set.Icc a b)

theorem IwaniecLinearSieve.bigM_pos (s : ℝ) : 0 < bigM s

0 < 𝔐 [I71, after (3.12)].

theorem IwaniecLinearSieve.antitone_of_antitoneOn_Iic_Ici {f : ℝ → ℝ} {a : ℝ} (h₁ : AntitoneOn f (Set.Iic a)) (h₂ : AntitoneOn f (Set.Ici a)) : Antitone f

An antitone function on (-∞, a] and on [a, ∞) is antitone.

theorem IwaniecLinearSieve.antitoneOn_initW : AntitoneOn initW (Set.Iic 3)

theorem IwaniecLinearSieve.continuousOn_kernel_mul {g : ℝ → ℝ} (hg : Continuous g) : ContinuousOn (fun (x : ℝ) => x / (x - 1) ^ 2 * g (x - 1)) (Set.Ici 2)

theorem IwaniecLinearSieve.intervalIntegrable_kernel_mul {g : ℝ → ℝ} (hg : Continuous g) {a b : ℝ} (ha : 2 ≤ a) (hb : 2 ≤ b) : IntervalIntegrable (fun (x : ℝ) => x / (x - 1) ^ 2 * g (x - 1)) MeasureTheory.volume a b

theorem IwaniecLinearSieve.kernel_pos {x : ℝ} (hx : 1 < x) : 0 < x / (x - 1) ^ 2

theorem IwaniecLinearSieve.bigM_antitone : Antitone bigM

𝔐 is antitone (on all of ℝ).

theorem IwaniecLinearSieve.bigM_le_three (s : ℝ) : bigM s ≤ 3

theorem IwaniecLinearSieve.bigM_le_ratio {s : ℝ} (hs : 3 ≤ s) : bigM s ≤ s / ((s - 1) ^ 2 - 1 / 2) * bigM (s - 1)

From (3.12) and monotonicity: 𝔐(s) ≤ s/((s-1)² - 1/2) 𝔐(s-1) for s ≥ 3.

theorem IwaniecLinearSieve.bigM_le_exp (s : ℝ) : bigM s ≤ 3 * Real.exp 5 * Real.exp (-s)

𝔐(s) = O(e^{-s}).

theorem IwaniecLinearSieve.tendsto_bigM_atTop : Filter.Tendsto bigM Filter.atTop (nhds 0)

theorem IwaniecLinearSieve.lemma6_aux {r x M : ℝ} (hr : r ≠ 0) (hx : x ≠ 0) : 1 / (3 * r) * ((1 - 1 / (2 * x ^ 2)) * M) - M / 3 / x ^ 2 = M * (x ^ 2 - 1 / 2 - r) / (3 * r * x ^ 2)

theorem IwaniecLinearSieve.abs_bigW_lt {s : ℝ} (hs : 3 ≤ s) : |bigW s| < bigM s / 3

[I71, Lemma 6], strict form for s ≥ 3: |𝔚(s)| < 𝔐(s)/3.

theorem IwaniecLinearSieve.abs_bigW_le (s : ℝ) : |bigW s| ≤ bigM s / 3

[I71, Lemma 6]: |𝔚(s)| ≤ 𝔐(s)/3 (for all s; [I71] states it for s ≥ 2).

theorem IwaniecLinearSieve.abs_bigW_le_exp (s : ℝ) : |bigW s| ≤ Real.exp 5 * Real.exp (-s)

𝔚(s) = O(e^{-s}).