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 IwaniecLinearSievePNT.Rectangle.symm {z w : ℂ} : z.Rectangle w = w.Rectangle z

theorem IwaniecLinearSievePNT.Rectangle.symm_re {z w : ℂ} : (↑w.re + ↑z.im * Complex.I).Rectangle (↑z.re + ↑w.im * Complex.I) = z.Rectangle w

def IwaniecLinearSievePNT.RectangleBorder (z w : ℂ) : Set ℂ

A RectangleBorder has corners z and w.

Equations

• IwaniecLinearSievePNT.RectangleBorder z w = Set.uIcc z.re w.re ×ℂ {z.im} ∪ {z.re} ×ℂ Set.uIcc z.im w.im ∪ Set.uIcc z.re w.re ×ℂ {w.im} ∪ {w.re} ×ℂ Set.uIcc z.im w.im

def IwaniecLinearSievePNT.Square (p : ℂ) (c : ℝ) : Set ℂ

The axis-aligned square centered at p with half-side length c.

Equations

• IwaniecLinearSievePNT.Square p c = (-↑c - ↑c * Complex.I + p).Rectangle (↑c + ↑c * Complex.I + p)

theorem IwaniecLinearSievePNT.Square_apply {c : ℝ} (p : ℂ) (cpos : c > 0) : Square p c = Set.Icc (-c + p.re) (c + p.re) ×ℂ Set.Icc (-c + p.im) (c + p.im)

@[simp]

theorem IwaniecLinearSievePNT.preimage_equivRealProdCLM_reProdIm (s t : Set ℝ) : ⇑Complex.equivRealProdCLM.symm ⁻¹' (s ×ℂ t) = s ×ˢ t

@[simp]

theorem ContinuousLinearEquiv.coe_toLinearEquiv_symm {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (M : Type u_3) [TopologicalSpace M] [AddCommMonoid M] {M₂ : Type u_4} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M] [Module S M₂] (e : M ≃SL[σ] M₂) : ⇑(↑e).symm = ⇑e.symm

theorem IwaniecLinearSievePNT.segment_reProdIm_segment_eq_convexHull (z w : ℂ) : Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im = (convexHull ℝ) {z, ↑z.re + ↑w.im * Complex.I, ↑w.re + ↑z.im * Complex.I, w}

The axis-parallel complex rectangle with opposite corners z and w is complex product of two intervals, which is also the convex hull of the four corners. Golfed from mathlib4#9598.

theorem IwaniecLinearSievePNT.rectangle_in_convex {U : Set ℂ} (U_convex : Convex ℝ U) {z w : ℂ} (hz : z ∈ U) (hw : w ∈ U) (hzw : ↑z.re + ↑w.im * Complex.I ∈ U) (hwz : ↑w.re + ↑z.im * Complex.I ∈ U) : z.Rectangle w ⊆ U

If the four corners of a rectangle are contained in a convex set U, then the whole rectangle is. Golfed from mathlib4#9598.

theorem IwaniecLinearSievePNT.mem_Rect {z w : ℂ} (zRe_lt_wRe : z.re ≤ w.re) (zIm_lt_wIm : z.im ≤ w.im) (p : ℂ) : p ∈ z.Rectangle w ↔ z.re ≤ p.re ∧ p.re ≤ w.re ∧ z.im ≤ p.im ∧ p.im ≤ w.im

theorem IwaniecLinearSievePNT.square_neg (p : ℂ) (c : ℝ) : Square p (-c) = Square p c

theorem Set.left_not_mem_uIoo {a b : ℝ} : a ∉ uIoo a b

theorem Set.right_not_mem_uIoo {a b : ℝ} : b ∉ uIoo a b

theorem Set.ne_left_of_mem_uIoo {a b c : ℝ} (hc : c ∈ uIoo a b) : c ≠ a

theorem Set.ne_right_of_mem_uIoo {a b c : ℝ} (hc : c ∈ uIoo a b) : c ≠ b

theorem IwaniecLinearSievePNT.left_mem_rect (z w : ℂ) : z ∈ z.Rectangle w

theorem IwaniecLinearSievePNT.right_mem_rect (z w : ℂ) : w ∈ z.Rectangle w

theorem IwaniecLinearSievePNT.rect_subset_iff {z w z' w' : ℂ} : z'.Rectangle w' ⊆ z.Rectangle w ↔ z' ∈ z.Rectangle w ∧ w' ∈ z.Rectangle w

theorem IwaniecLinearSievePNT.RectSubRect {x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ} (x₀_le_x₁ : x₀ ≤ x₁) (x₁_le_x₂ : x₁ ≤ x₂) (x₂_le_x₃ : x₂ ≤ x₃) (y₀_le_y₁ : y₀ ≤ y₁) (y₁_le_y₂ : y₁ ≤ y₂) (y₂_le_y₃ : y₂ ≤ y₃) : (↑x₁ + ↑y₁ * Complex.I).Rectangle (↑x₂ + ↑y₂ * Complex.I) ⊆ (↑x₀ + ↑y₀ * Complex.I).Rectangle (↑x₃ + ↑y₃ * Complex.I)

theorem IwaniecLinearSievePNT.RectSubRect' {z₀ z₁ z₂ z₃ : ℂ} (x₀_le_x₁ : z₀.re ≤ z₁.re) (x₁_le_x₂ : z₁.re ≤ z₂.re) (x₂_le_x₃ : z₂.re ≤ z₃.re) (y₀_le_y₁ : z₀.im ≤ z₁.im) (y₁_le_y₂ : z₁.im ≤ z₂.im) (y₂_le_y₃ : z₂.im ≤ z₃.im) : z₁.Rectangle z₂ ⊆ z₀.Rectangle z₃

theorem IwaniecLinearSievePNT.rectangleBorder_subset_rectangle (z w : ℂ) : RectangleBorder z w ⊆ z.Rectangle w

theorem IwaniecLinearSievePNT.rectangle_disjoint_singleton {z w p : ℂ} (h : p.re < z.re ∧ p.re < w.re ∨ p.im < z.im ∧ p.im < w.im ∨ z.re < p.re ∧ w.re < p.re ∨ z.im < p.im ∧ w.im < p.im) : Disjoint (z.Rectangle w) {p}

Note: try using by simp for h.

theorem IwaniecLinearSievePNT.rectangleBorder_disjoint_singleton {z w p : ℂ} (h : p.re ≠ z.re ∧ p.re ≠ w.re ∧ p.im ≠ z.im ∧ p.im ≠ w.im) : Disjoint (RectangleBorder z w) {p}

theorem IwaniecLinearSievePNT.rectangle_subset_punctured_rect {z₀ z₁ z₂ z₃ p : ℂ} (hz : z₀.re ≤ z₁.re ∧ z₁.re ≤ z₂.re ∧ z₂.re ≤ z₃.re ∧ z₀.im ≤ z₁.im ∧ z₁.im ≤ z₂.im ∧ z₂.im ≤ z₃.im) (hp : p.re < z₁.re ∧ p.re < z₂.re ∨ p.im < z₁.im ∧ p.im < z₂.im ∨ z₁.re < p.re ∧ z₂.re < p.re ∨ z₁.im < p.im ∧ z₂.im < p.im) : z₁.Rectangle z₂ ⊆ z₀.Rectangle z₃ \ {p}

theorem IwaniecLinearSievePNT.rectangleBorder_subset_punctured_rect {z₀ z₁ z₂ z₃ p : ℂ} (hz : z₀.re ≤ z₁.re ∧ z₁.re ≤ z₂.re ∧ z₂.re ≤ z₃.re ∧ z₀.im ≤ z₁.im ∧ z₁.im ≤ z₂.im ∧ z₂.im ≤ z₃.im) (hp : p.re ≠ z₁.re ∧ p.re ≠ z₂.re ∧ p.im ≠ z₁.im ∧ p.im ≠ z₂.im) : RectangleBorder z₁ z₂ ⊆ z₀.Rectangle z₃ \ {p}

theorem IwaniecLinearSievePNT.rectangle_mem_nhds_iff {z w p : ℂ} : z.Rectangle w ∈ nhds p ↔ p ∈ Set.uIoo z.re w.re ×ℂ Set.uIoo z.im w.im

theorem IwaniecLinearSievePNT.mapsTo_rectangle_left_re (z w : ℂ) : Set.MapsTo (fun (y : ℝ) => ↑z.re + ↑y * Complex.I) (Set.uIcc z.im w.im) (z.Rectangle w)

theorem IwaniecLinearSievePNT.mapsTo_rectangle_right_re (z w : ℂ) : Set.MapsTo (fun (y : ℝ) => ↑w.re + ↑y * Complex.I) (Set.uIcc z.im w.im) (z.Rectangle w)

theorem IwaniecLinearSievePNT.mapsTo_rectangle_left_im (z w : ℂ) : Set.MapsTo (fun (x : ℝ) => ↑x + ↑z.im * Complex.I) (Set.uIcc z.re w.re) (z.Rectangle w)

theorem IwaniecLinearSievePNT.mapsTo_rectangle_right_im (z w : ℂ) : Set.MapsTo (fun (x : ℝ) => ↑x + ↑w.im * Complex.I) (Set.uIcc z.re w.re) (z.Rectangle w)

theorem IwaniecLinearSievePNT.mapsTo_rectangleBorder_left_re (z w : ℂ) : Set.MapsTo (fun (y : ℝ) => ↑z.re + ↑y * Complex.I) (Set.uIcc z.im w.im) (RectangleBorder z w)

theorem IwaniecLinearSievePNT.mapsTo_rectangleBorder_right_re (z w : ℂ) : Set.MapsTo (fun (y : ℝ) => ↑w.re + ↑y * Complex.I) (Set.uIcc z.im w.im) (RectangleBorder z w)

theorem IwaniecLinearSievePNT.mapsTo_rectangleBorder_left_im (z w : ℂ) : Set.MapsTo (fun (x : ℝ) => ↑x + ↑z.im * Complex.I) (Set.uIcc z.re w.re) (RectangleBorder z w)

theorem IwaniecLinearSievePNT.mapsTo_rectangleBorder_right_im (z w : ℂ) : Set.MapsTo (fun (x : ℝ) => ↑x + ↑w.im * Complex.I) (Set.uIcc z.re w.re) (RectangleBorder z w)

theorem IwaniecLinearSievePNT.mapsTo_rectangle_left_re_NoP (z w : ℂ) {p : ℂ} (pNotOnBorder : p ∉ RectangleBorder z w) : Set.MapsTo (fun (y : ℝ) => ↑z.re + ↑y * Complex.I) (Set.uIcc z.im w.im) (z.Rectangle w \ {p})

theorem IwaniecLinearSievePNT.mapsTo_rectangle_right_re_NoP (z w : ℂ) {p : ℂ} (pNotOnBorder : p ∉ RectangleBorder z w) : Set.MapsTo (fun (y : ℝ) => ↑w.re + ↑y * Complex.I) (Set.uIcc z.im w.im) (z.Rectangle w \ {p})

theorem IwaniecLinearSievePNT.mapsTo_rectangle_left_im_NoP (z w : ℂ) {p : ℂ} (pNotOnBorder : p ∉ RectangleBorder z w) : Set.MapsTo (fun (x : ℝ) => ↑x + ↑z.im * Complex.I) (Set.uIcc z.re w.re) (z.Rectangle w \ {p})

theorem IwaniecLinearSievePNT.mapsTo_rectangle_right_im_NoP (z w : ℂ) {p : ℂ} (pNotOnBorder : p ∉ RectangleBorder z w) : Set.MapsTo (fun (x : ℝ) => ↑x + ↑w.im * Complex.I) (Set.uIcc z.re w.re) (z.Rectangle w \ {p})

theorem IwaniecLinearSievePNT.not_mem_rectangleBorder_of_rectangle_mem_nhds {z w p : ℂ} (hp : z.Rectangle w ∈ nhds p) : p ∉ RectangleBorder z w

theorem Complex.nhds_hasBasis_square (p : ℂ) : (nhds p).HasBasis (fun (x : ℝ) => 0 < x) fun (x : ℝ) => IwaniecLinearSievePNT.Square p x

theorem IwaniecLinearSievePNT.square_mem_nhds (p : ℂ) {c : ℝ} (hc : c ≠ 0) : Square p c ∈ nhds p

theorem IwaniecLinearSievePNT.square_subset_square {p : ℂ} {c₁ c₂ : ℝ} (hc₁ : 0 < c₁) (hc : c₁ ≤ c₂) : Square p c₁ ⊆ Square p c₂

theorem IwaniecLinearSievePNT.SmallSquareInRectangle {z w p : ℂ} (pInRectInterior : z.Rectangle w ∈ nhds p) : ∀ᶠ (c : ℝ) in nhdsWithin 0 (Set.Ioi 0), Square p c ⊆ z.Rectangle w