Adapted from PrimeNumberTheoremAnd revision 127b50e33f6033e2147921167a117af96d9ba4ea, via Jason Davies's Iwaniec linear sieve snapshot c8d01549d2ae640b36ec198c1f0f6495f1b036cf (both Apache-2.0). Blueprint-only machinery is omitted.

Supporting lemmas for Iwaniec's sieve and its prime-number-theorem input.

theorem MeasureTheory.setIntegral_integral_swap {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SigmaFinite ν] [NormedSpace ℝ E] [SigmaFinite μ] (f : α → β → E) {s : Set α} {t : Set β} (hf : IntegrableOn (Function.uncurry f) (s ×ˢ t) (μ.prod ν)) : ∫ (x : α) in s, ∫ (y : β) in t, f x y ∂ν ∂μ = ∫ (y : β) in t, ∫ (x : α) in s, f x y ∂μ ∂ν

theorem MeasureTheory.integral_comp_mul_right_I0i_haar {𝕂 : Type u_1} [RCLike 𝕂] (f : ℝ → 𝕂) {a : ℝ} (ha : 0 < a) : ∫ (y : ℝ) in Set.Ioi 0, f (y * a) / ↑y = ∫ (y : ℝ) in Set.Ioi 0, f y / ↑y

theorem MeasureTheory.integral_comp_mul_right_I0i_haar_real (f : ℝ → ℝ) {a : ℝ} (ha : 0 < a) : ∫ (y : ℝ) in Set.Ioi 0, f (y * a) / y = ∫ (y : ℝ) in Set.Ioi 0, f y / y

theorem MeasureTheory.integral_comp_mul_left_I0i_haar {𝕂 : Type u_1} [RCLike 𝕂] (f : ℝ → 𝕂) {a : ℝ} (ha : 0 < a) : ∫ (y : ℝ) in Set.Ioi 0, f (a * y) / ↑y = ∫ (y : ℝ) in Set.Ioi 0, f y / ↑y

theorem MeasureTheory.integral_comp_rpow_I0i_haar_real (f : ℝ → ℝ) {p : ℝ} (hp : p ≠ 0) : ∫ (y : ℝ) in Set.Ioi 0, |p| * f (y ^ p) / y = ∫ (y : ℝ) in Set.Ioi 0, f y / y

theorem MeasureTheory.integral_comp_inv_I0i_haar {𝕂 : Type u_1} [RCLike 𝕂] (f : ℝ → 𝕂) : ∫ (y : ℝ) in Set.Ioi 0, f (1 / y) / ↑y = ∫ (y : ℝ) in Set.Ioi 0, f y / ↑y

theorem MeasureTheory.integral_comp_div_I0i_haar {𝕂 : Type u_1} [RCLike 𝕂] (f : ℝ → 𝕂) {a : ℝ} (ha : 0 < a) : ∫ (y : ℝ) in Set.Ioi 0, f (a / y) / ↑y = ∫ (y : ℝ) in Set.Ioi 0, f y / ↑y

theorem Complex.ofReal_rpow {x : ℝ} (h : x > 0) (y : ℝ) : ↑(x ^ y) = ↑x ^ ↑y

@[simp]

theorem Function.support_abs {𝕂 : Type u_1} [RCLike 𝕂] {α : Type u_2} (f : α → 𝕂) : (support fun (x : α) => ‖f x‖) = support f

@[simp]

theorem Function.support_ofReal {f : ℝ → ℝ} : (support fun (x : ℝ) => ↑(f x)) = support f

theorem Function.support_mul_subset_of_subset {𝕂 : Type u_1} [RCLike 𝕂] {s : Set ℝ} {f g : ℝ → 𝕂} (fSupp : support f ⊆ s) : support (f * g) ⊆ s

theorem Function.support_of_along_fiber_subset_subset {α : Type u_2} {β : Type u_3} {M : Type u_4} [Zero M] {f : α × β → M} {s : Set α} {t : Set β} (hx : ∀ (y : β), (support fun (x : α) => f (x, y)) ⊆ s) (hy : ∀ (x : α), (support fun (y : β) => f (x, y)) ⊆ t) : support f ⊆ s ×ˢ t

theorem Function.support_deriv_subset_Icc {𝕂 : Type u_1} [RCLike 𝕂] {a b : ℝ} {f : ℝ → 𝕂} (fSupp : support f ⊆ Set.Icc a b) : support (deriv f) ⊆ Set.Icc a b

theorem IwaniecLinearSievePNT.IntervalIntegral.integral_eq_integral_of_support_subset_Icc {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} (h : Function.support f ⊆ Set.Icc a b) : ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ

theorem IwaniecLinearSievePNT.SetIntegral.integral_eq_integral_inter_of_support_subset {μ : MeasureTheory.Measure ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {s t : Set ℝ} {f : ℝ → E} (h : Function.support f ⊆ t) (ht : MeasurableSet t) : ∫ (x : ℝ) in s, f x ∂μ = ∫ (x : ℝ) in s ∩ t, f x ∂μ

theorem IwaniecLinearSievePNT.SetIntegral.integral_eq_integral_inter_of_support_subset_Icc {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set ℝ} {f : ℝ → E} (h : Function.support f ⊆ Set.Icc a b) (hs : Set.Icc a b ⊆ s) : ∫ (x : ℝ) in s, f x ∂μ = ∫ (x : ℝ) in Set.Icc a b, f x ∂μ

theorem intervalIntegral.norm_integral_le_of_norm_le_const' {a b C : ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} (hab : a ≤ b) (h : ∀ x ∈ Set.Icc a b, ‖f x‖ ≤ C) : ‖∫ (x : ℝ) in a..b, f x‖ ≤ C * |b - a|

theorem Filter.TendstoAtZero_of_support_in_Icc {𝕂 : Type u_1} [RCLike 𝕂] {a b : ℝ} (f : ℝ → 𝕂) (ha : 0 < a) (fSupp : Function.support f ⊆ Set.Icc a b) : Tendsto f (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

theorem Filter.TendstoAtTop_of_support_in_Icc {𝕂 : Type u_1} [RCLike 𝕂] {a b : ℝ} (f : ℝ → 𝕂) (fSupp : Function.support f ⊆ Set.Icc a b) : Tendsto f atTop (nhds 0)

theorem Filter.BigO_zero_atZero_of_support_in_Icc {𝕂 : Type u_1} [RCLike 𝕂] {a b : ℝ} (f : ℝ → 𝕂) (ha : 0 < a) (fSupp : Function.support f ⊆ Set.Icc a b) : f =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => 0

theorem Filter.BigO_zero_atTop_of_support_in_Icc {𝕂 : Type u_1} [RCLike 𝕂] {a b : ℝ} (f : ℝ → 𝕂) (fSupp : Function.support f ⊆ Set.Icc a b) : f =O[atTop] fun (x : ℝ) => 0

theorem deriv.ofReal_comp' {f : ℝ → ℝ} : (deriv fun (x : ℝ) => ↑(f x)) = fun (x : ℝ) => ↑(deriv f x)

theorem deriv.comp_ofReal' {e : ℂ → ℂ} (hf : Differentiable ℂ e) : (deriv fun (x : ℝ) => e ↑x) = fun (x : ℝ) => deriv e ↑x

theorem IwaniecLinearSievePNT.PartialIntegration (f g : ℝ → ℂ) (fDiff : DifferentiableOn ℝ f (Set.Ioi 0)) (gDiff : DifferentiableOn ℝ g (Set.Ioi 0)) (fDerivgInt : MeasureTheory.IntegrableOn (f * deriv g) (Set.Ioi 0) MeasureTheory.volume) (gDerivfInt : MeasureTheory.IntegrableOn (deriv f * g) (Set.Ioi 0) MeasureTheory.volume) (lim_at_zero : Filter.Tendsto (f * g) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) (lim_at_inf : Filter.Tendsto (f * g) Filter.atTop (nhds 0)) : ∫ (x : ℝ) in Set.Ioi 0, f x * deriv g x = -∫ (x : ℝ) in Set.Ioi 0, deriv f x * g x

Need differentiability, and decay at 0 and ∞

theorem IwaniecLinearSievePNT.PartialIntegration_of_support_in_Icc {a b : ℝ} (f g : ℝ → ℂ) (ha : 0 < a) (h : a ≤ b) (fSupp : Function.support f ⊆ Set.Icc a b) (fDiff : DifferentiableOn ℝ f (Set.Ioi 0)) (gDiff : DifferentiableOn ℝ g (Set.Ioi 0)) (fderivCont : ContinuousOn (deriv f) (Set.Ioi 0)) (gderivCont : ContinuousOn (deriv g) (Set.Ioi 0)) : ∫ (x : ℝ) in Set.Ioi 0, f x * deriv g x = -∫ (x : ℝ) in Set.Ioi 0, deriv f x * g x

noncomputable def IwaniecLinearSievePNT.MellinConvolution {𝕂 : Type u_1} [RCLike 𝕂] (f g : ℝ → 𝕂) (x : ℝ) : 𝕂

Multiplicative convolution with respect to the measure dy / y on the positive reals.

Equations

• IwaniecLinearSievePNT.MellinConvolution f g x = ∫ (y : ℝ) in Set.Ioi 0, f y * g (x / y) / ↑y

theorem IwaniecLinearSievePNT.MellinConvolutionSymmetric {𝕂 : Type u_1} [RCLike 𝕂] (f g : ℝ → 𝕂) {x : ℝ} (xpos : 0 < x) : MellinConvolution f g x = MellinConvolution g f x

theorem IwaniecLinearSievePNT.support_MellinConvolution_subsets {𝕂 : Type u_1} [RCLike 𝕂] {f g : ℝ → 𝕂} {A B : Set ℝ} (hf : Function.support f ⊆ A) (hg : Function.support g ⊆ B) : Function.support (MellinConvolution f g) ⊆ A * B

theorem IwaniecLinearSievePNT.support_MellinConvolution {𝕂 : Type u_1} [RCLike 𝕂] (f g : ℝ → 𝕂) : Function.support (MellinConvolution f g) ⊆ Function.support f * Function.support g

theorem IwaniecLinearSievePNT.MellinConvolutionTransform (f g : ℝ → ℂ) (s : ℂ) (hf : MeasureTheory.IntegrableOn (Function.uncurry fun (x y : ℝ) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Set.Ioi 0 ×ˢ Set.Ioi 0) MeasureTheory.volume) : mellin (MellinConvolution f g) s = mellin f s * mellin g s

theorem IwaniecLinearSievePNT.mem_within_strip (σ₁ σ₂ : ℝ) : {s : ℂ | σ₁ ≤ s.re ∧ s.re ≤ σ₂} ∈ Filter.principal {s : ℂ | σ₁ ≤ s.re ∧ s.re ≤ σ₂}

theorem IwaniecLinearSievePNT.MellinOfPsi_aux {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) {s : ℂ} (hs : s ≠ 0) : ∫ (x : ℝ) in Set.Ioi 0, ↑(ν x) * ↑x ^ (s - 1) = -(1 / s) * ∫ (x : ℝ) in Set.Ioi 0, ↑(deriv ν x) * ↑x ^ s

theorem IwaniecLinearSievePNT.MellinOfPsi {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) : ∃ C > 0, ∀ (σ₁ : ℝ), 0 < σ₁ → ∀ (s : ℂ), σ₁ ≤ s.re → s.re ≤ 2 → ‖mellin (fun (x : ℝ) => ↑(ν x)) s‖ ≤ C * ‖s‖⁻¹

noncomputable def IwaniecLinearSievePNT.DeltaSpike (ν : ℝ → ℝ) (ε : ℝ) : ℝ → ℝ

A rescaled smoothing kernel concentrated near the multiplicative identity.

Equations

• IwaniecLinearSievePNT.DeltaSpike ν ε x = ν (x ^ (1 / ε)) / ε

theorem IwaniecLinearSievePNT.DeltaSpikeMass {ν : ℝ → ℝ} (mass_one : ∫ (x : ℝ) in Set.Ioi 0, ν x / x = 1) {ε : ℝ} (εpos : 0 < ε) : ∫ (x : ℝ) in Set.Ioi 0, DeltaSpike ν ε x / x = 1

theorem IwaniecLinearSievePNT.DeltaSpikeSupport_aux {ν : ℝ → ℝ} {ε : ℝ} (εpos : 0 < ε) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) : (Function.support fun (x : ℝ) => if x < 0 then 0 else DeltaSpike ν ε x) ⊆ Set.Icc (2 ^ (-ε)) (2 ^ ε)

theorem IwaniecLinearSievePNT.DeltaSpikeSupport' {ν : ℝ → ℝ} {ε x : ℝ} (εpos : 0 < ε) (xnonneg : 0 ≤ x) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) : DeltaSpike ν ε x ≠ 0 → x ∈ Set.Icc (2 ^ (-ε)) (2 ^ ε)

theorem IwaniecLinearSievePNT.DeltaSpikeSupport {ν : ℝ → ℝ} {ε x : ℝ} (εpos : 0 < ε) (xnonneg : 0 ≤ x) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) : x ∉ Set.Icc (2 ^ (-ε)) (2 ^ ε) → DeltaSpike ν ε x = 0

theorem IwaniecLinearSievePNT.DeltaSpikeContinuous {ν : ℝ → ℝ} {ε : ℝ} (εpos : 0 < ε) (diffν : ContDiff ℝ 1 ν) : Continuous fun (x : ℝ) => DeltaSpike ν ε x

theorem IwaniecLinearSievePNT.DeltaSpikeOfRealContinuous {ν : ℝ → ℝ} {ε : ℝ} (εpos : 0 < ε) (diffν : ContDiff ℝ 1 ν) : Continuous fun (x : ℝ) => ↑(DeltaSpike ν ε x)

theorem IwaniecLinearSievePNT.MellinOfDeltaSpike (ν : ℝ → ℝ) {ε : ℝ} (εpos : ε > 0) (s : ℂ) : mellin (fun (x : ℝ) => ↑(DeltaSpike ν ε x)) s = mellin (fun (x : ℝ) => ↑(ν x)) (↑ε * s)

theorem IwaniecLinearSievePNT.MellinOfDeltaSpikeAt1 (ν : ℝ → ℝ) {ε : ℝ} (εpos : ε > 0) : mellin (fun (x : ℝ) => ↑(DeltaSpike ν ε x)) 1 = mellin (fun (x : ℝ) => ↑(ν x)) ↑ε

theorem IwaniecLinearSievePNT.MellinOfDeltaSpikeAt1_asymp {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, ν x / x = 1) : (fun (ε : ℝ) => mellin (fun (x : ℝ) => ↑(ν x)) ↑ε - 1) =O[nhdsWithin 0 (Set.Ioi 0)] id

theorem IwaniecLinearSievePNT.MellinOf1 (s : ℂ) (h : s.re > 0) : mellin (fun (x : ℝ) => if 0 < x ∧ x ≤ 1 then 1 else 0) s = 1 / s

noncomputable def IwaniecLinearSievePNT.Smooth1 (ν : ℝ → ℝ) (ε : ℝ) : ℝ → ℝ

The indicator of (0, 1] smoothed by multiplicative convolution with DeltaSpike.

Equations

• IwaniecLinearSievePNT.Smooth1 ν ε = IwaniecLinearSievePNT.MellinConvolution (fun (x : ℝ) => if 0 < x ∧ x ≤ 1 then 1 else 0) (IwaniecLinearSievePNT.DeltaSpike ν ε)

theorem IwaniecLinearSievePNT.Smooth1_def_ite {ν : ℝ → ℝ} {ε x : ℝ} (xpos : 0 < x) : Smooth1 ν ε x = MellinConvolution (fun (x : ℝ) => if 0 < x ∧ x ≤ 1 then 1 else 0) (fun (x : ℝ) => if x < 0 then 0 else DeltaSpike ν ε x) x

theorem IwaniecLinearSievePNT.Smooth1Properties_estimate {ε : ℝ} (εpos : 0 < ε) : (1 - 2 ^ (-ε)) / ε < Real.log 2

theorem IwaniecLinearSievePNT.Smooth1Properties_below_aux {x ε : ℝ} (hx : x ≤ 1 - Real.log 2 * ε) (εpos : 0 < ε) : x < 2 ^ (-ε)

theorem IwaniecLinearSievePNT.Smooth1Properties_below {ν : ℝ → ℝ} (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, ν x / x = 1) : ∃ (c : ℝ), 0 < c ∧ c = Real.log 2 ∧ ∀ (ε x : ℝ), 0 < ε → 0 < x → x ≤ 1 - c * ε → Smooth1 ν ε x = 1

theorem IwaniecLinearSievePNT.Smooth1Properties_above_aux {x ε : ℝ} (hx : 1 + 2 * Real.log 2 * ε ≤ x) (hε : ε ∈ Set.Ioo 0 1) : 2 ^ ε < x

theorem IwaniecLinearSievePNT.Smooth1Properties_above_aux2 {x y ε : ℝ} (hε : ε ∈ Set.Ioo 0 1) (hy : y ∈ Set.Ioc 0 1) (hx2 : 2 ^ ε < x) : 2 < (x / y) ^ (1 / ε)

theorem IwaniecLinearSievePNT.Smooth1Properties_above {ν : ℝ → ℝ} (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) : ∃ (c : ℝ), 0 < c ∧ c = 2 * Real.log 2 ∧ ∀ (ε x : ℝ), ε ∈ Set.Ioo 0 1 → 1 + c * ε ≤ x → Smooth1 ν ε x = 0

theorem IwaniecLinearSievePNT.DeltaSpikeNonNeg_of_NonNeg {ν : ℝ → ℝ} (νnonneg : ∀ x > 0, 0 ≤ ν x) {x ε : ℝ} (xpos : 0 < x) (εpos : 0 < ε) : 0 ≤ DeltaSpike ν ε x

theorem IwaniecLinearSievePNT.MellinConvNonNeg_of_NonNeg {f g : ℝ → ℝ} (f_nonneg : ∀ x > 0, 0 ≤ f x) (g_nonneg : ∀ x > 0, 0 ≤ g x) {x : ℝ} (xpos : 0 < x) : 0 ≤ MellinConvolution f g x

theorem IwaniecLinearSievePNT.Smooth1Nonneg {ν : ℝ → ℝ} (νnonneg : ∀ x > 0, 0 ≤ ν x) {ε x : ℝ} (xpos : 0 < x) (εpos : 0 < ε) : 0 ≤ Smooth1 ν ε x

theorem IwaniecLinearSievePNT.Smooth1LeOne_aux {x ε : ℝ} {ν : ℝ → ℝ} (xpos : 0 < x) (εpos : 0 < ε) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, ν x / x = 1) : ∫ (y : ℝ) in Set.Ioi 0, ν ((x / y) ^ (1 / ε)) / ε / y = 1

theorem IwaniecLinearSievePNT.Smooth1LeOne {ν : ℝ → ℝ} (νnonneg : ∀ x > 0, 0 ≤ ν x) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, ν x / x = 1) {ε : ℝ} (εpos : 0 < ε) {x : ℝ} (xpos : 0 < x) : Smooth1 ν ε x ≤ 1

theorem IwaniecLinearSievePNT.MellinOfSmooth1a {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) {ε : ℝ} (εpos : 0 < ε) {s : ℂ} (hs : 0 < s.re) : mellin (fun (x : ℝ) => ↑(Smooth1 ν ε x)) s = s⁻¹ * mellin (fun (x : ℝ) => ↑(ν x)) (↑ε * s)

theorem IwaniecLinearSievePNT.MellinOfSmooth1b {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) : ∃ (C : ℝ) (_ : 0 < C), ∀ (σ₁ : ℝ), 0 < σ₁ → ∀ (s : ℂ), σ₁ ≤ s.re → s.re ≤ 2 → ∀ (ε : ℝ), 0 < ε → ε < 1 → ‖mellin (fun (x : ℝ) => ↑(Smooth1 ν ε x)) s‖ ≤ C * (ε * ‖s‖ ^ 2)⁻¹

theorem IwaniecLinearSievePNT.MellinOfSmooth1c {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, ν x / x = 1) : (fun (ε : ℝ) => mellin (fun (x : ℝ) => ↑(Smooth1 ν ε x)) 1 - 1) =O[nhdsWithin 0 (Set.Ioi 0)] id

theorem IwaniecLinearSievePNT.Smooth1ContinuousAt {SmoothingF : ℝ → ℝ} (diffSmoothingF : ContDiff ℝ 1 SmoothingF) (SmoothingFpos : ∀ x > 0, 0 ≤ SmoothingF x) (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2) {ε : ℝ} (εpos : 0 < ε) {y : ℝ} (ypos : 0 < y) : ContinuousAt (fun (x : ℝ) => Smooth1 SmoothingF ε x) y

theorem IwaniecLinearSievePNT.Smooth1MellinConvergent {Ψ : ℝ → ℝ} {ε : ℝ} (diffΨ : ContDiff ℝ 1 Ψ) (suppΨ : Function.support Ψ ⊆ Set.Icc (1 / 2) 2) (hε : ε ∈ Set.Ioo 0 1) (Ψnonneg : ∀ x > 0, 0 ≤ Ψ x) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, Ψ x / x = 1) {s : ℂ} (hs : 0 < s.re) : MellinConvergent (fun (x : ℝ) => ↑(Smooth1 Ψ ε x)) s

theorem IwaniecLinearSievePNT.Smooth1MellinDifferentiable {Ψ : ℝ → ℝ} {ε : ℝ} (diffΨ : ContDiff ℝ 1 Ψ) (suppΨ : Function.support Ψ ⊆ Set.Icc (1 / 2) 2) (hε : ε ∈ Set.Ioo 0 1) (Ψnonneg : ∀ x > 0, 0 ≤ Ψ x) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, Ψ x / x = 1) {s : ℂ} (hs : 0 < s.re) : DifferentiableAt ℂ (mellin fun (x : ℝ) => ↑(Smooth1 Ψ ε x)) s