Iwaniec's functions 𝔐, 𝔚 ([I71, §3, Definition])

• 𝔚(s) = 1/(s-1) - log(s-1) on [2, 3], 𝔚'(s) = s/(s-1)² 𝔚(s-1) for s > 3;
• 𝔐(s) = 2 + 1/(s-1) - log(s-1) on [2, 3], 𝔐'(s) = -s/(s-1)² 𝔐(s-1) for s > 3.

Both are defined on all of ℝ (𝔐 in IwaniecLinearSieve.Definitions) and are continuous; to the left of 2 they are constant (𝔚 = 1, 𝔐 = 3). We prove the integral equations (3.11) and (3.12) of [I71].

noncomputable def IwaniecLinearSieve.bigW : ℝ → ℝ

Iwaniec's 𝔚 [I71, §3, Definition].

Equations

• IwaniecLinearSieve.bigW = IwaniecLinearSieve.Delay.sol IwaniecLinearSieve.delayKer IwaniecLinearSieve.initW

theorem IwaniecLinearSieve.delayKer_of_ge {x : ℝ} (hx : 3 ≤ x) : delayKer x = x / (x - 1) ^ 2

theorem IwaniecLinearSieve.continuous_delayKer : Continuous delayKer

theorem IwaniecLinearSieve.continuous_initW : Continuous initW

theorem IwaniecLinearSieve.initW_of_le {s : ℝ} (hs : s ≤ 2) : initW s = 1

theorem IwaniecLinearSieve.initW_of_ge {s : ℝ} (hs : 2 ≤ s) : initW s = 1 / (s - 1) - Real.log (s - 1)

theorem IwaniecLinearSieve.continuous_bigW : Continuous bigW

theorem IwaniecLinearSieve.continuous_initM : Continuous fun (s : ℝ) => 2 + initW s

theorem IwaniecLinearSieve.continuous_bigM : Continuous bigM

theorem IwaniecLinearSieve.bigW_of_le_three {s : ℝ} (hs : s ≤ 3) : bigW s = initW s

theorem IwaniecLinearSieve.bigM_of_le_three {s : ℝ} (hs : s ≤ 3) : bigM s = 2 + initW s

theorem IwaniecLinearSieve.bigW_of_le_two {s : ℝ} (hs : s ≤ 2) : bigW s = 1

theorem IwaniecLinearSieve.bigM_of_le_two {s : ℝ} (hs : s ≤ 2) : bigM s = 3

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

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

theorem IwaniecLinearSieve.bigW_two : bigW 2 = 1

theorem IwaniecLinearSieve.bigM_two : bigM 2 = 3

theorem IwaniecLinearSieve.bigW_three : bigW 3 = 1 / 2 - Real.log 2

theorem IwaniecLinearSieve.bigM_three : bigM 3 = 5 / 2 - Real.log 2

theorem IwaniecLinearSieve.hasDerivAt_initForm {x : ℝ} (hx : 1 < x) : HasDerivAt (fun (x : ℝ) => 1 / (x - 1) - Real.log (x - 1)) (-(x / (x - 1) ^ 2)) x

The derivative of 1/(x-1) - log(x-1) is -x/(x-1)².

theorem IwaniecLinearSieve.bigW_eq_integral {s : ℝ} (hs : 3 ≤ s) : bigW s = bigW 3 + ∫ (x : ℝ) in 3..s, x / (x - 1) ^ 2 * bigW (x - 1)

theorem IwaniecLinearSieve.bigM_eq_integral {s : ℝ} (hs : 3 ≤ s) : bigM s = bigM 3 - ∫ (x : ℝ) in 3..s, x / (x - 1) ^ 2 * bigM (x - 1)

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

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

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

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

Auxiliary calculus

theorem IwaniecLinearSieve.hasDerivAt_integral_unit {F : ℝ → ℝ} (hF : Continuous F) (t : ℝ) : HasDerivAt (fun (t : ℝ) => ∫ (x : ℝ) in t - 1..t, F x) (F t - F (t - 1)) t

t ↦ ∫_{t-1}^t F has derivative F t - F (t - 1).

theorem IwaniecLinearSieve.eq_of_hasDerivAt_zero {g : ℝ → ℝ} {a : ℝ} (hg : ContinuousOn g (Set.Ici a)) (hd : ∀ (x : ℝ), a < x → HasDerivAt g 0 x) {s : ℝ} (hs : a ≤ s) : g s = g a

A function continuous on [a, ∞) with zero derivative on (a, ∞) is constant there.

(3.11)

noncomputable def IwaniecLinearSieve.wIntegrand (x : ℝ) : ℝ

The integrand of (3.11), made continuous on ℝ.

Equations

• IwaniecLinearSieve.wIntegrand x = IwaniecLinearSieve.bigW x / max x 1 ^ 2

theorem IwaniecLinearSieve.continuous_wIntegrand : Continuous wIntegrand

theorem IwaniecLinearSieve.wIntegrand_of_ge {x : ℝ} (hx : 1 ≤ x) : wIntegrand x = bigW x / x ^ 2

theorem IwaniecLinearSieve.integral_wIntegrand_two_three : ∫ (x : ℝ) in 2..3, wIntegrand x = (1 + Real.log 2) / 3 - 1 / 2

theorem IwaniecLinearSieve.bigW_eq_neg_mul_integral {s : ℝ} (hs : 3 ≤ s) : bigW s = -s * ∫ (x : ℝ) in s - 1..s, bigW x / x ^ 2

[I71, (3.11)]: 𝔚(s) = -s ∫_{s-1}^s 𝔚(x)/x² dx for s ≥ 3.

(3.12)

noncomputable def IwaniecLinearSieve.mIntegrand (x : ℝ) : ℝ

The integrand of (3.12), made continuous on ℝ.

Equations

• IwaniecLinearSieve.mIntegrand x = (1 - 1 / (2 * max x 1 ^ 2)) * IwaniecLinearSieve.bigM x

theorem IwaniecLinearSieve.continuous_mIntegrand : Continuous mIntegrand

theorem IwaniecLinearSieve.mIntegrand_of_ge {x : ℝ} (hx : 1 ≤ x) : mIntegrand x = (1 - 1 / (2 * x ^ 2)) * bigM x

theorem IwaniecLinearSieve.integral_mIntegrand_two_three : ∫ (x : ℝ) in 2..3, mIntegrand x = 7 / 2 * (5 / 2 - Real.log 2) / 3

theorem IwaniecLinearSieve.bigM_integral_identity {s : ℝ} (hs : 3 ≤ s) : ((s - 1) ^ 2 - 1 / 2) * bigM s / s = ∫ (x : ℝ) in s - 1..s, (1 - 1 / (2 * x ^ 2)) * bigM x

[I71, (3.12)]: ((s-1)² - 1/2) 𝔐(s) / s = ∫_{s-1}^s (1 - 1/(2x²)) 𝔐(x) dx for s ≥ 3.