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.deriv_conj_conj' (f : ℂ → ℂ) (p : ℂ) : deriv (fun (z : ℂ) => (starRingEnd ℂ) (f ((starRingEnd ℂ) z))) ((starRingEnd ℂ) p) = (starRingEnd ℂ) (deriv f p)

theorem IwaniecLinearSievePNT.deriv_riemannZeta_conj (s : ℂ) : deriv riemannZeta ((starRingEnd ℂ) s) = (starRingEnd ℂ) (deriv riemannZeta s)

theorem IwaniecLinearSievePNT.logDerivZeta_conj (s : ℂ) : (deriv riemannZeta / riemannZeta) ((starRingEnd ℂ) s) = (starRingEnd ℂ) ((deriv riemannZeta / riemannZeta) s)

theorem IwaniecLinearSievePNT.logDerivZeta_conj' (s : ℂ) : logDeriv riemannZeta ((starRingEnd ℂ) s) = (starRingEnd ℂ) (logDeriv riemannZeta s)

theorem IwaniecLinearSievePNT.intervalIntegral_conj {f : ℝ → ℂ} {a b : ℝ} : ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (f x) = (starRingEnd ℂ) (∫ (x : ℝ) in a..b, f x)