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.

noncomputable def IwaniecLinearSievePNT.HIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (x₁ x₂ y : ℝ) : E

The contour integral along a horizontal line segment.

Equations

• IwaniecLinearSievePNT.HIntegral f x₁ x₂ y = ∫ (x : ℝ) in x₁..x₂, f (↑x + ↑y * Complex.I)

noncomputable def IwaniecLinearSievePNT.VIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (x y₁ y₂ : ℝ) : E

The contour integral along a vertical line segment, including its tangent factor I.

Equations

• IwaniecLinearSievePNT.VIntegral f x y₁ y₂ = Complex.I • ∫ (y : ℝ) in y₁..y₂, f (↑x + ↑y * Complex.I)

noncomputable def IwaniecLinearSievePNT.HIntegral' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (x₁ x₂ y : ℝ) : E

The horizontal contour integral normalized by 1 / (2 * π * I).

Equations

• IwaniecLinearSievePNT.HIntegral' f x₁ x₂ y = (1 / (2 * ↑Real.pi * Complex.I)) • IwaniecLinearSievePNT.HIntegral f x₁ x₂ y

noncomputable def IwaniecLinearSievePNT.VIntegral' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (x y₁ y₂ : ℝ) : E

The vertical contour integral normalized by 1 / (2 * π * I).

Equations

• IwaniecLinearSievePNT.VIntegral' f x y₁ y₂ = (1 / (2 * ↑Real.pi * Complex.I)) • IwaniecLinearSievePNT.VIntegral f x y₁ y₂

theorem IwaniecLinearSievePNT.HIntegral_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {x₁ x₂ y : ℝ} : HIntegral f x₁ x₂ y = -HIntegral f x₂ x₁ y

theorem IwaniecLinearSievePNT.VIntegral_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {x y₁ y₂ : ℝ} : VIntegral f x y₁ y₂ = -VIntegral f x y₂ y₁

noncomputable def IwaniecLinearSievePNT.RectangleIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w : ℂ) : E

A RectangleIntegral of a function f is one over a rectangle determined by z and w in ℂ.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev IwaniecLinearSievePNT.RectangleIntegral' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w : ℂ) : E

A RectangleIntegral' of a function f is one over a rectangle determined by z and w in ℂ, divided by 2 * π * I.

Equations

• IwaniecLinearSievePNT.RectangleIntegral' f z w = (1 / (2 * ↑Real.pi * Complex.I)) • IwaniecLinearSievePNT.RectangleIntegral f z w

noncomputable def IwaniecLinearSievePNT.UpperUIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (σ σ' T : ℝ) : E

The contour integral over the upper U-shaped contour, oriented from left to right.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def IwaniecLinearSievePNT.LowerUIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (σ σ' T : ℝ) : E

The contour integral over the lower U-shaped contour, oriented from left to right.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def IwaniecLinearSievePNT.VerticalIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (σ : ℝ) : E

The contour integral over the entire upward vertical line with real part σ.

Equations

• IwaniecLinearSievePNT.VerticalIntegral f σ = Complex.I • ∫ (t : ℝ), f (↑σ + ↑t * Complex.I)

@[reducible, inline]

noncomputable abbrev IwaniecLinearSievePNT.VerticalIntegral' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (σ : ℝ) : E

The full vertical contour integral normalized by 1 / (2 * π * I).

Equations

• IwaniecLinearSievePNT.VerticalIntegral' f σ = (1 / (2 * ↑Real.pi * Complex.I)) • IwaniecLinearSievePNT.VerticalIntegral f σ

theorem IwaniecLinearSievePNT.verticalIntegral_split_three {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {σ : ℝ} (a b : ℝ) (hf : MeasureTheory.Integrable (fun (t : ℝ) => f (↑σ + ↑t * Complex.I)) MeasureTheory.volume) : VerticalIntegral f σ = (Complex.I • ∫ (t : ℝ) in Set.Iic a, f (↑σ + ↑t * Complex.I)) + VIntegral f σ a b + Complex.I • ∫ (t : ℝ) in Set.Ici b, f (↑σ + ↑t * Complex.I)

theorem IwaniecLinearSievePNT.DiffVertRect_eq_UpperLowerUs {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {σ σ' T : ℝ} (f_int_σ : MeasureTheory.Integrable (fun (t : ℝ) => f (↑σ + ↑t * Complex.I)) MeasureTheory.volume) (f_int_σ' : MeasureTheory.Integrable (fun (t : ℝ) => f (↑σ' + ↑t * Complex.I)) MeasureTheory.volume) : VerticalIntegral f σ' - VerticalIntegral f σ - RectangleIntegral f (↑σ - Complex.I * ↑T) (↑σ' + Complex.I * ↑T) = UpperUIntegral f σ σ' T - LowerUIntegral f σ σ' T

@[reducible, inline]

abbrev IwaniecLinearSievePNT.HolomorphicOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (s : Set ℂ) : Prop

A function is HolomorphicOn a set if it is complex differentiable on that set.

Equations

• IwaniecLinearSievePNT.HolomorphicOn f s = DifferentiableOn ℂ f s

theorem IwaniecLinearSievePNT.existsDifferentiableOn_of_bddAbove {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} [CompleteSpace E] {s : Set ℂ} {c : ℂ} (hc : s ∈ nhds c) (hd : HolomorphicOn f (s \ {c})) (hb : BddAbove (norm ∘ f '' (s \ {c}))) : ∃ (g : ℂ → E), HolomorphicOn g s ∧ Set.EqOn f g (s \ {c})

theorem IwaniecLinearSievePNT.HolomorphicOn.vanishesOnRectangle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {z w : ℂ} {U : Set ℂ} (f_holo : HolomorphicOn f U) (hU : z.Rectangle w ⊆ U) : RectangleIntegral f z w = 0

theorem IwaniecLinearSievePNT.RectangleIntegral_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℂ → E} {z w : ℂ} (h : Set.EqOn f g (RectangleBorder z w)) : RectangleIntegral f z w = RectangleIntegral g z w

theorem IwaniecLinearSievePNT.RectangleIntegral'_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℂ → E} {z w : ℂ} (h : Set.EqOn f g (RectangleBorder z w)) : RectangleIntegral' f z w = RectangleIntegral' g z w

theorem IwaniecLinearSievePNT.rectangleIntegral_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w : ℂ) : RectangleIntegral f z w = RectangleIntegral f w z

theorem IwaniecLinearSievePNT.rectangleIntegral_symm_re {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w : ℂ) : RectangleIntegral f (↑w.re + ↑z.im * Complex.I) (↑z.re + ↑w.im * Complex.I) = -RectangleIntegral f z w

def IwaniecLinearSievePNT.RectangleBorderIntegrable {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) (z w : ℂ) : Prop

Integrability of the integrand on each of the four sides of a rectangle.

Equations

• One or more equations did not get rendered due to their size.

theorem IwaniecLinearSievePNT.RectangleBorderIntegrable.add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {z w : ℂ} {f g : ℂ → E} (hf : RectangleBorderIntegrable f z w) (hg : RectangleBorderIntegrable g z w) : RectangleIntegral (f + g) z w = RectangleIntegral f z w + RectangleIntegral g z w

theorem ContinuousOn.rectangleBorder_integrable {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} {z w : ℂ} (hf : ContinuousOn f (IwaniecLinearSievePNT.RectangleBorder z w)) : IwaniecLinearSievePNT.RectangleBorderIntegrable f z w

theorem ContinuousOn.rectangleBorderIntegrable {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} {z w : ℂ} (hf : ContinuousOn f (z.Rectangle w)) : IwaniecLinearSievePNT.RectangleBorderIntegrable f z w

theorem ContinuousOn.rectangleBorderNoPIntegrable {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} {z w p : ℂ} (hf : ContinuousOn f (z.Rectangle w \ {p})) (pNotOnBorder : p ∉ IwaniecLinearSievePNT.RectangleBorder z w) : IwaniecLinearSievePNT.RectangleBorderIntegrable f z w

theorem IwaniecLinearSievePNT.HolomorphicOn.rectangleBorderIntegrable' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {z w p : ℂ} (hf : HolomorphicOn f (z.Rectangle w \ {p})) (hp : z.Rectangle w ∈ nhds p) : RectangleBorderIntegrable f z w

theorem IwaniecLinearSievePNT.HolomorphicOn.rectangleBorderIntegrable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {z w : ℂ} (hf : HolomorphicOn f (z.Rectangle w)) : RectangleBorderIntegrable f z w

theorem IwaniecLinearSievePNT.RectangleIntegralHSplit {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {a x₀ x₁ y₀ y₁ : ℝ} (f_int_x₀_a_bot : IntervalIntegrable (fun (x : ℝ) => f (↑x + ↑y₀ * Complex.I)) MeasureTheory.volume x₀ a) (f_int_a_x₁_bot : IntervalIntegrable (fun (x : ℝ) => f (↑x + ↑y₀ * Complex.I)) MeasureTheory.volume a x₁) (f_int_x₀_a_top : IntervalIntegrable (fun (x : ℝ) => f (↑x + ↑y₁ * Complex.I)) MeasureTheory.volume x₀ a) (f_int_a_x₁_top : IntervalIntegrable (fun (x : ℝ) => f (↑x + ↑y₁ * Complex.I)) MeasureTheory.volume a x₁) : RectangleIntegral f (↑x₀ + ↑y₀ * Complex.I) (↑x₁ + ↑y₁ * Complex.I) = RectangleIntegral f (↑x₀ + ↑y₀ * Complex.I) (↑a + ↑y₁ * Complex.I) + RectangleIntegral f (↑a + ↑y₀ * Complex.I) (↑x₁ + ↑y₁ * Complex.I)

Given x₀ a x₁ : ℝ, and y₀ y₁ : ℝ and a function f : ℂ → ℂ so that both (t : ℝ) ↦ f(t + y₀ * I) and (t : ℝ) ↦ f(t + y₁ * I) are integrable over both t ∈ Icc x₀ a and t ∈ Icc a x₁, we have that RectangleIntegral f (x₀ + y₀ * I) (x₁ + y₁ * I) is the sum of RectangleIntegral f (x₀ + y₀ * I) (a + y₁ * I) and RectangleIntegral f (a + y₀ * I) (x₁ + y₁ * I).

theorem IwaniecLinearSievePNT.RectangleIntegralHSplit' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {a x₀ x₁ y₀ y₁ : ℝ} (ha : a ∈ Set.uIcc x₀ x₁) (hf : RectangleBorderIntegrable f (↑x₀ + ↑y₀ * Complex.I) (↑x₁ + ↑y₁ * Complex.I)) : RectangleIntegral f (↑x₀ + ↑y₀ * Complex.I) (↑x₁ + ↑y₁ * Complex.I) = RectangleIntegral f (↑x₀ + ↑y₀ * Complex.I) (↑a + ↑y₁ * Complex.I) + RectangleIntegral f (↑a + ↑y₀ * Complex.I) (↑x₁ + ↑y₁ * Complex.I)

theorem IwaniecLinearSievePNT.RectangleIntegralVSplit {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {b x₀ x₁ y₀ y₁ : ℝ} (f_int_y₀_b_left : IntervalIntegrable (fun (y : ℝ) => f (↑x₀ + ↑y * Complex.I)) MeasureTheory.volume y₀ b) (f_int_b_y₁_left : IntervalIntegrable (fun (y : ℝ) => f (↑x₀ + ↑y * Complex.I)) MeasureTheory.volume b y₁) (f_int_y₀_b_right : IntervalIntegrable (fun (y : ℝ) => f (↑x₁ + ↑y * Complex.I)) MeasureTheory.volume y₀ b) (f_int_b_y₁_right : IntervalIntegrable (fun (y : ℝ) => f (↑x₁ + ↑y * Complex.I)) MeasureTheory.volume b y₁) : RectangleIntegral f (↑x₀ + ↑y₀ * Complex.I) (↑x₁ + ↑y₁ * Complex.I) = RectangleIntegral f (↑x₀ + ↑y₀ * Complex.I) (↑x₁ + ↑b * Complex.I) + RectangleIntegral f (↑x₀ + ↑b * Complex.I) (↑x₁ + ↑y₁ * Complex.I)

theorem IwaniecLinearSievePNT.RectangleIntegralVSplit' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {b x₀ x₁ y₀ y₁ : ℝ} (hb : b ∈ Set.uIcc y₀ y₁) (hf : RectangleBorderIntegrable f (↑x₀ + ↑y₀ * Complex.I) (↑x₁ + ↑y₁ * Complex.I)) : RectangleIntegral f (↑x₀ + ↑y₀ * Complex.I) (↑x₁ + ↑y₁ * Complex.I) = RectangleIntegral f (↑x₀ + ↑y₀ * Complex.I) (↑x₁ + ↑b * Complex.I) + RectangleIntegral f (↑x₀ + ↑b * Complex.I) (↑x₁ + ↑y₁ * Complex.I)

theorem IwaniecLinearSievePNT.RectanglePullToNhdOfPole' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {z₀ z₁ z₂ z₃ p : ℂ} (h_orientation : z₀.re ≤ z₃.re ∧ z₀.im ≤ z₃.im ∧ z₁.re ≤ z₂.re ∧ z₁.im ≤ z₂.im) (hp : z₁.Rectangle z₂ ∈ nhds p) (hz : z₁.Rectangle z₂ ⊆ z₀.Rectangle z₃) (fHolo : HolomorphicOn f (z₀.Rectangle z₃ \ {p})) : RectangleIntegral f z₀ z₃ = RectangleIntegral f z₁ z₂

theorem IwaniecLinearSievePNT.RectanglePullToNhdOfPole {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {z w p : ℂ} (zRe_lt_wRe : z.re ≤ w.re) (zIm_lt_wIm : z.im ≤ w.im) (hp : z.Rectangle w ∈ nhds p) (fHolo : HolomorphicOn f (z.Rectangle w \ {p})) : ∀ᶠ (c : ℝ) in nhdsWithin 0 (Set.Ioi 0), RectangleIntegral f z w = RectangleIntegral f (-↑c - Complex.I * ↑c + p) (↑c + Complex.I * ↑c + p)

Given f holomorphic on a rectangle z and w except at a point p, the integral of f over the rectangle with corners z and w is the same as the integral of f over a small square centered at p.

theorem IwaniecLinearSievePNT.RectanglePullToNhdOfPole'' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {z w p : ℂ} (zRe_le_wRe : z.re ≤ w.re) (zIm_le_wIm : z.im ≤ w.im) (pInRectInterior : z.Rectangle w ∈ nhds p) (fHolo : HolomorphicOn f (z.Rectangle w \ {p})) : ∀ᶠ (c : ℝ) in nhdsWithin 0 (Set.Ioi 0), RectangleIntegral' f z w = RectangleIntegral' f (-↑c - Complex.I * ↑c + p) (↑c + Complex.I * ↑c + p)

theorem IwaniecLinearSievePNT.ResidueTheoremAtOrigin_aux1c (a b : ℝ) : have f := fun (y : ℝ) => (↑y + Complex.I)⁻¹; IntervalIntegrable f MeasureTheory.volume a b

theorem IwaniecLinearSievePNT.ResidueTheoremAtOrigin_aux1c' (a b : ℝ) : have f := fun (y : ℝ) => (↑y - Complex.I)⁻¹; IntervalIntegrable f MeasureTheory.volume a b

theorem IwaniecLinearSievePNT.ResidueTheoremAtOrigin_aux2c (a b : ℝ) : have f := fun (y : ℝ) => (1 + ↑y * Complex.I)⁻¹; IntervalIntegrable f MeasureTheory.volume a b

theorem IwaniecLinearSievePNT.ResidueTheoremAtOrigin_aux2c' (a b : ℝ) : have f := fun (y : ℝ) => (-1 + ↑y * Complex.I)⁻¹; IntervalIntegrable f MeasureTheory.volume a b

theorem IwaniecLinearSievePNT.RectangleIntegral.const_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w c : ℂ) : RectangleIntegral (fun (s : ℂ) => c • f s) z w = c • RectangleIntegral f z w

theorem IwaniecLinearSievePNT.RectangleIntegral.const_mul' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w c : ℂ) : RectangleIntegral' (fun (s : ℂ) => c • f s) z w = c • RectangleIntegral' f z w

theorem IwaniecLinearSievePNT.RectangleIntegral.translate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w p : ℂ) : RectangleIntegral (fun (s : ℂ) => f (s - p)) z w = RectangleIntegral f (z - p) (w - p)

theorem IwaniecLinearSievePNT.RectangleIntegral.translate' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w p : ℂ) : RectangleIntegral' (fun (s : ℂ) => f (s - p)) z w = RectangleIntegral' f (z - p) (w - p)

theorem Complex.inv_re_add_im {x y : ℝ} : (↑x + ↑y * I)⁻¹ = (↑x - I * ↑y) / (↑x ^ 2 + ↑y ^ 2)

theorem IwaniecLinearSievePNT.sq_add_sq_ne_zero {x y : ℝ} (hy : y ≠ 0) : x ^ 2 + y ^ 2 ≠ 0

theorem IwaniecLinearSievePNT.continuous_self_div_sq_add_sq {y : ℝ} (hy : y ≠ 0) : Continuous fun (x : ℝ) => x / (x ^ 2 + y ^ 2)

theorem IwaniecLinearSievePNT.integral_self_div_sq_add_sq {x₁ x₂ y : ℝ} (hy : y ≠ 0) : ∫ (x : ℝ) in x₁..x₂, x / (x ^ 2 + y ^ 2) = Real.log (x₂ ^ 2 + y ^ 2) / 2 - Real.log (x₁ ^ 2 + y ^ 2) / 2

theorem IwaniecLinearSievePNT.integral_const_div_sq_add_sq {x₁ x₂ y : ℝ} (hy : y ≠ 0) : ∫ (x : ℝ) in x₁..x₂, y / (x ^ 2 + y ^ 2) = Real.arctan (x₂ / y) - Real.arctan (x₁ / y)

theorem IwaniecLinearSievePNT.integral_const_div_self_add_im {A : ℂ} {x₁ x₂ y : ℝ} (hy : y ≠ 0) : ∫ (x : ℝ) in x₁..x₂, A / (↑x + ↑y * Complex.I) = A * (↑(Real.log (x₂ ^ 2 + y ^ 2)) / 2 - ↑(Real.log (x₁ ^ 2 + y ^ 2)) / 2) - A * Complex.I * (↑(Real.arctan (x₂ / y)) - ↑(Real.arctan (x₁ / y)))

theorem IwaniecLinearSievePNT.integral_const_div_re_add_self {A : ℂ} {x y₁ y₂ : ℝ} (hx : x ≠ 0) : ∫ (y : ℝ) in y₁..y₂, A / (↑x + ↑y * Complex.I) = A / Complex.I * (↑(Real.log (y₂ ^ 2 + (-x) ^ 2)) / 2 - ↑(Real.log (y₁ ^ 2 + (-x) ^ 2)) / 2) - A / Complex.I * Complex.I * (↑(Real.arctan (y₂ / -x)) - ↑(Real.arctan (y₁ / -x)))

theorem IwaniecLinearSievePNT.ResidueTheoremAtOrigin' {z w c : ℂ} (h1 : z.re < 0) (h2 : z.im < 0) (h3 : 0 < w.re) (h4 : 0 < w.im) : RectangleIntegral (fun (s : ℂ) => c / s) z w = 2 * Complex.I * ↑Real.pi * c

theorem IwaniecLinearSievePNT.ResidueTheoremInRectangle {z w p c : ℂ} (zRe_le_wRe : z.re ≤ w.re) (zIm_le_wIm : z.im ≤ w.im) (pInRectInterior : z.Rectangle w ∈ nhds p) : RectangleIntegral' (fun (s : ℂ) => c / (s - p)) z w = c

theorem IwaniecLinearSievePNT.ResidueTheoremAtOrigin : RectangleIntegral' (fun (s : ℂ) => 1 / s) (-1 - Complex.I) (1 + Complex.I) = 1

theorem IwaniecLinearSievePNT.ResidueTheoremOnRectangleWithSimplePole {f g : ℂ → ℂ} {z w p A : ℂ} (zRe_le_wRe : z.re ≤ w.re) (zIm_le_wIm : z.im ≤ w.im) (pInRectInterior : z.Rectangle w ∈ nhds p) (gHolo : HolomorphicOn g (z.Rectangle w)) (principalPart : Set.EqOn (f - fun (s : ℂ) => A / (s - p)) g (z.Rectangle w \ {p})) : RectangleIntegral' f z w = A

theorem IwaniecLinearSievePNT.IsBigO_to_BddAbove {f : ℂ → ℂ} {p : ℂ} (f_near_p : f =O[nhdsWithin p {p}ᶜ] 1) : ∃ U ∈ nhds p, BddAbove (norm ∘ f '' (U \ {p}))

theorem IwaniecLinearSievePNT.BddAbove_on_rectangle_of_bdd_near {z w p : ℂ} {f : ℂ → ℂ} (f_cont : ContinuousOn f (z.Rectangle w \ {p})) (f_near_p : f =O[nhdsWithin p {p}ᶜ] 1) : BddAbove (norm ∘ f '' (z.Rectangle w \ {p}))

theorem IwaniecLinearSievePNT.ResidueTheoremOnRectangleWithSimplePole' {f : ℂ → ℂ} {z w p A : ℂ} (zRe_le_wRe : z.re ≤ w.re) (zIm_le_wIm : z.im ≤ w.im) (pInRectInterior : z.Rectangle w ∈ nhds p) (fHolo : HolomorphicOn f (z.Rectangle w \ {p})) (near_p : (f - fun (s : ℂ) => A / (s - p)) =O[nhdsWithin p {p}ᶜ] 1) : RectangleIntegral' f z w = A