theorem Chapter16.lem_16_7_chebyshev_bound {x : ℝ} (hx : 0 ≤ x) : Chebyshev.theta x ≤ Real.log 4 * x

theorem Chapter16.lem_16_7_chebyshev_bound_book {x : ℝ} (hx : 0 ≤ x) : Chebyshev.theta x ≤ 4 * Real.log 2 * x

theorem Chapter16.div_log_sq_isLittleO_div_log : (fun (x : ℝ) => x / Real.log x ^ 2) =o[Filter.atTop] fun (x : ℝ) => x / Real.log x

theorem Chapter16.primeCounting_sub_theta_div_log_isLittleO : (fun (x : ℝ) => ↑⌊x⌋₊.primeCounting - Chebyshev.theta x / Real.log x) =o[Filter.atTop] fun (x : ℝ) => x / Real.log x

theorem Chapter16.thm_16_6_forward (htheta : Asymptotics.IsEquivalent Filter.atTop (fun (x : ℝ) => Chebyshev.theta x) fun (x : ℝ) => x) : Asymptotics.IsEquivalent Filter.atTop (fun (x : ℝ) => ↑⌊x⌋₊.primeCounting) fun (x : ℝ) => x / Real.log x

theorem Chapter16.thm_16_6_backward (hpi : Asymptotics.IsEquivalent Filter.atTop (fun (x : ℝ) => ↑⌊x⌋₊.primeCounting) fun (x : ℝ) => x / Real.log x) : Asymptotics.IsEquivalent Filter.atTop (fun (x : ℝ) => Chebyshev.theta x) fun (x : ℝ) => x

theorem Chapter16.thm_16_6_chebyshev_equiv : (Asymptotics.IsEquivalent Filter.atTop (fun (x : ℝ) => ↑⌊x⌋₊.primeCounting) fun (x : ℝ) => x / Real.log x) ↔ Asymptotics.IsEquivalent Filter.atTop (fun (x : ℝ) => Chebyshev.theta x) fun (x : ℝ) => x

theorem Chapter16.lem_16_8_integral_criterion (f : ℝ → ℝ) (hf_mono : Monotone f) (hf_conv : ∃ (L : ℝ), Filter.Tendsto (fun (x : ℝ) => ∫ (t : ℝ) in Set.Ioc 1 x, (f t - t) / t ^ 2) Filter.atTop (nhds L)) : Asymptotics.IsEquivalent Filter.atTop (fun (x : ℝ) => f x) fun (x : ℝ) => x

noncomputable def Chapter16.laplace_transform (h : ℝ → ℝ) (s : ℂ) : ℂ

noncomputable def Chapter16.Phi (s : ℂ) : ℂ

theorem Chapter16.theta_exp_eq_tsum (t : ℝ) : Chebyshev.theta (Real.exp t) = ∑' (p : Nat.Primes), if Real.log ↑↑p ≤ t then Real.log ↑↑p else 0

theorem Chapter16.exp_neg_mul_log_eq_cpow (p : ℕ) (hp : 0 < p) (s : ℂ) : Complex.exp (-s * ↑(Real.log ↑p)) = ↑p ^ (-s)

theorem Chapter16.integral_indicator_prime (p : ℕ) (hp : Nat.Prime p) (s : ℂ) (hs : 0 < s.re) : ∫ (t : ℝ) in Set.Ioi (Real.log ↑p), Complex.exp (-s * ↑t) = ↑p ^ (-s) / s

theorem Chapter16.prime_log_pos (p : Nat.Primes) : 0 < Real.log ↑↑p

theorem Chapter16.abel_norm_summand_eq (c : ℝ) (hc : 0 ≤ c) (s : ℂ) (t : ℝ) : ‖Complex.exp (-s * ↑t) * ↑(if c ≤ t then c else 0)‖ = if c ≤ t then c * Real.exp (-s.re * t) else 0

theorem Chapter16.abel_indicator_integral_real (c : ℝ) (hc : 0 < c) (σ : ℝ) (hσ : 0 < σ) : (∫ (t : ℝ) in Set.Ioi 0, if c ≤ t then c * Real.exp (-σ * t) else 0) = c * Real.exp (-σ * c) / σ

theorem Chapter16.abel_indicator_integral_complex (c : ℝ) (hc : 0 < c) (s : ℂ) : ∫ (t : ℝ) in Set.Ioi 0, Complex.exp (-s * ↑t) * ↑(if c ≤ t then c else 0) = ↑c * ∫ (t : ℝ) in Set.Ioi c, Complex.exp (-s * ↑t)

theorem Chapter16.abel_summable_primes_log_rpow (σ : ℝ) (hσ : 1 < σ) : Summable fun (p : Nat.Primes) => Real.log ↑↑p * ↑↑p ^ (-σ)

theorem Chapter16.abel_integrableOn_prime_summand (p : Nat.Primes) (s : ℂ) (hs : 0 < s.re) : MeasureTheory.IntegrableOn (fun (t : ℝ) => Complex.exp (-s * ↑t) * ↑(if Real.log ↑↑p ≤ t then Real.log ↑↑p else 0)) (Set.Ioi 0) MeasureTheory.volume

theorem Chapter16.abel_summation_laplace_theta (s : ℂ) (hs : 1 < s.re) : laplace_transform (fun (t : ℝ) => Chebyshev.theta (Real.exp t)) s = ∑' (p : Nat.Primes), ↑(Real.log ↑↑p) * ↑↑p ^ (-s) / s

theorem Chapter16.lem_16_10_laplace_theta (s : ℂ) (hs : 1 < s.re) : laplace_transform (fun (t : ℝ) => Chebyshev.theta (Real.exp t)) s = Phi s / s

theorem Chapter16.integrableOn_mul_exp_neg_Ioi' {r : ℝ} (hr : 0 < r) : MeasureTheory.IntegrableOn (fun (t : ℝ) => t * Real.exp (-r * t)) (Set.Ioi 0) MeasureTheory.volume

theorem Chapter16.laplace_holomorphic_of_exp_bound (h : ℝ → ℝ) (a C : ℝ) (hC : 0 < C) (hbound : ∀ (t : ℝ), 0 ≤ t → |h t| ≤ C * Real.exp (a * t)) : DifferentiableOn ℂ (fun (s : ℂ) => laplace_transform h s) {s : ℂ | a < s.re}

theorem Chapter16.lem_16_10_holomorphic : DifferentiableOn ℂ (fun (s : ℂ) => laplace_transform (fun (t : ℝ) => Chebyshev.theta (Real.exp t)) s) {s : ℂ | 1 < s.re}

noncomputable def Chapter16.PhiCorrection (s : ℂ) : ℂ

noncomputable def Chapter16.G₀ : ℂ → ℂ

theorem Chapter16.G₀_eq_of_ne {s : ℂ} (hs : s ≠ 1) : G₀ s = (s - 1) * riemannZeta s

theorem Chapter16.G₀_one : G₀ 1 = 1

theorem Chapter16.G₀_differentiableAt_of_ne {s : ℂ} (hs : s ≠ 1) : DifferentiableAt ℂ G₀ s

theorem Chapter16.G₀_analyticAt_one : AnalyticAt ℂ G₀ 1

theorem Chapter16.G₀_differentiable : Differentiable ℂ G₀

theorem Chapter16.G₀_ne_zero_of_one_le_re {s : ℂ} (hs : 1 ≤ s.re) : G₀ s ≠ 0

noncomputable def Chapter16.F₀ : ℂ → ℂ

theorem Chapter16.F₀_eq : F₀ = fun (z : ℂ) => (z - 1) ^ 2 • riemannZeta z

theorem Chapter16.meromorphicAt_riemannZeta_one : MeromorphicAt riemannZeta 1

theorem Chapter16.meromorphicAt_riemannZeta (s : ℂ) : MeromorphicAt riemannZeta s

theorem Chapter16.rpow_sub_one_bound {p σ : ℝ} (hp : 2 ≤ p) (hσ : 0 < σ) : (1 - 2 ^ (-σ)) * p ^ (2 * σ) ≤ p ^ σ * (p ^ σ - 1)

theorem Chapter16.summable_primes_rpow_neg {α : ℝ} (hα : 1 < α) : Summable fun (p : Nat.Primes) => ↑↑p ^ (-α)

theorem Chapter16.prime_rpow_sub_one_pos (p : Nat.Primes) (σ : ℝ) (hσ : 1 / 2 < σ) : 0 < ↑↑p ^ σ - 1

theorem Chapter16.phiCorrection_term_differentiableOn (p : Nat.Primes) (σ : ℝ) (hσ : 1 / 2 < σ) : DifferentiableOn ℂ (fun (w : ℂ) => ↑(Real.log ↑↑p) / (↑↑p ^ w * (↑↑p ^ w - 1))) {s : ℂ | σ < s.re}

theorem Chapter16.phiCorrection_term_norm_bound (p : Nat.Primes) (σ : ℝ) (hσ : 1 / 2 < σ) (w : ℂ) (hw : σ < w.re) : ‖↑(Real.log ↑↑p) / (↑↑p ^ w * (↑↑p ^ w - 1))‖ ≤ Real.log ↑↑p / (↑↑p ^ σ * (↑↑p ^ σ - 1))

theorem Chapter16.phiCorrection_summable_bound (σ : ℝ) (hσ : 1 / 2 < σ) : Summable fun (p : Nat.Primes) => Real.log ↑↑p / (↑↑p ^ σ * (↑↑p ^ σ - 1))

theorem Chapter16.phiCorrection_holomorphic : DifferentiableOn ℂ PhiCorrection {s : ℂ | 1 / 2 < s.re}

theorem Chapter16.tsum_eq_tsum_primes_of_support_subset_prime_powers {f : ℕ → ℂ} (hf : Summable f) (hsupp : Function.support f ⊆ {n : ℕ | IsPrimePow n}) : ∑' (n : ℕ), f n = ∑' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 1))

theorem Chapter16.vonMangoldt_LSeries_eq_double_sum (s : ℂ) (hs : 1 < s.re) : LSeries (fun (n : ℕ) => ↑(ArithmeticFunction.vonMangoldt n)) s = ∑' (p : Nat.Primes) (k : ℕ), ↑(Real.log ↑↑p) / ↑↑p ^ ((k + 1) • s)

theorem Chapter16.vonMangoldt_LSeries_eq_Phi_add_PhiCorrection (s : ℂ) (hs : 1 < s.re) : LSeries (fun (n : ℕ) => ↑(ArithmeticFunction.vonMangoldt n)) s = Phi s + PhiCorrection s

theorem Chapter16.euler_product_log_deriv (s : ℂ) (hs : 1 < s.re) : -deriv riemannZeta s / riemannZeta s = Phi s + PhiCorrection s

theorem Chapter16.log_deriv_zeta_meromorphic_on_pos_re : MeromorphicOn (fun (s : ℂ) => -deriv riemannZeta s / riemannZeta s) {s : ℂ | 0 < s.re}

theorem Chapter16.log_deriv_zeta_minus_pole_holomorphic : ∃ (h : ℂ → ℂ), DifferentiableOn ℂ h {s : ℂ | 1 ≤ s.re} ∧ ∀ (s : ℂ), 1 < s.re → h s = -deriv riemannZeta s / riemannZeta s - 1 / (s - 1)

theorem Chapter16.lem_16_11_Phi_holomorphic : ∃ (g : ℂ → ℂ), DifferentiableOn ℂ g {s : ℂ | 1 ≤ s.re} ∧ ∀ (s : ℂ), 1 < s.re → g s = Phi s - 1 / (s - 1)

theorem Chapter16.lem_16_11_Phi_meromorphic : ∃ (g : ℂ → ℂ), MeromorphicOn g {s : ℂ | 1 / 2 < s.re} ∧ ∀ (s : ℂ), 1 < s.re → g s = Phi s - 1 / (s - 1)

noncomputable def Chapter16.boundedProj (z : ℂ) (C : ℝ) : ℂ

theorem Chapter16.norm_boundedProj_le (z : ℂ) (C : ℝ) (hC : 0 ≤ C) : ‖boundedProj z C‖ ≤ C

noncomputable def Chapter16.right_semicircle_integrand (g : ℂ → ℂ) (f : ℝ → ℝ) (r τ u : ℝ) : ℂ

noncomputable def Chapter16.newman_cif_I_right (f : ℝ → ℝ) (M : ℝ) (hM : ∀ (t : ℝ), 0 ≤ t → |f t| ≤ M) (g : ℂ → ℂ) (hg_holo : DifferentiableOn ℂ g {s : ℂ | 0 ≤ s.re}) (hg_laplace : ∀ (s : ℂ), 0 < s.re → g s = laplace_transform f s) (r : ℝ) (hr : 0 < r) : ℝ → ℂ

noncomputable def Chapter16.left_semicircle_integrand (g : ℂ → ℂ) (f : ℝ → ℝ) (r τ u : ℝ) : ℂ

noncomputable def Chapter16.newman_cif_I_left (f : ℝ → ℝ) (M : ℝ) (hM : ∀ (t : ℝ), 0 ≤ t → |f t| ≤ M) (g : ℂ → ℂ) (hg_holo : DifferentiableOn ℂ g {s : ℂ | 0 ≤ s.re}) (hg_laplace : ∀ (s : ℂ), 0 < s.re → g s = laplace_transform f s) (r : ℝ) (hr : 0 < r) : ℝ → ℂ

theorem Chapter16.newman_cif_circle_integral (f : ℝ → ℝ) (M : ℝ) (hM : ∀ (t : ℝ), 0 ≤ t → |f t| ≤ M) (g : ℂ → ℂ) (hg_holo : DifferentiableOn ℂ g {s : ℂ | 0 ≤ s.re}) (hg_laplace : ∀ (s : ℂ), 0 < s.re → g s = laplace_transform f s) (r : ℝ) (hr : 0 < r) (τ : ℝ) : g 0 - ↑(∫ (t : ℝ) in Set.Ioc 0 τ, f t) = (1 / (2 * ↑Real.pi * Complex.I) * ∫ (u : ℝ) in -(Real.pi / 2)..Real.pi / 2, right_semicircle_integrand g f r τ u) + 1 / (2 * ↑Real.pi * Complex.I) * ∫ (u : ℝ) in Real.pi / 2..3 * Real.pi / 2, left_semicircle_integrand g f r τ u

theorem Chapter16.newman_cif_identity (f : ℝ → ℝ) (M : ℝ) (hM : ∀ (t : ℝ), 0 ≤ t → |f t| ≤ M) (g : ℂ → ℂ) (hg_holo : DifferentiableOn ℂ g {s : ℂ | 0 ≤ s.re}) (hg_laplace : ∀ (s : ℂ), 0 < s.re → g s = laplace_transform f s) (r : ℝ) (hr : 0 < r) (τ : ℝ) : g 0 - ↑(∫ (t : ℝ) in Set.Ioc 0 τ, f t) = newman_cif_I_right f M hM g hg_holo hg_laplace r hr τ + newman_cif_I_left f M hM g hg_holo hg_laplace r hr τ

theorem Chapter16.newman_right_semicircle_bound (f : ℝ → ℝ) (M : ℝ) (hM : ∀ (t : ℝ), 0 ≤ t → |f t| ≤ M) (g : ℂ → ℂ) (hg_holo : DifferentiableOn ℂ g {s : ℂ | 0 ≤ s.re}) (hg_laplace : ∀ (s : ℂ), 0 < s.re → g s = laplace_transform f s) (r : ℝ) (hr : 0 < r) (τ : ℝ) : ‖newman_cif_I_right f M hM g hg_holo hg_laplace r hr τ‖ ≤ 1 / r

theorem Chapter16.newman_left_semicircle_bound (f : ℝ → ℝ) (M : ℝ) (hM : ∀ (t : ℝ), 0 ≤ t → |f t| ≤ M) (g : ℂ → ℂ) (hg_holo : DifferentiableOn ℂ g {s : ℂ | 0 ≤ s.re}) (hg_laplace : ∀ (s : ℂ), 0 < s.re → g s = laplace_transform f s) (r : ℝ) (hr : 0 < r) : ∀ᶠ (τ : ℝ) in Filter.atTop, ‖newman_cif_I_left f M hM g hg_holo hg_laplace r hr τ‖ ≤ 1 / r

theorem Chapter16.newman_contour_decomposition (f : ℝ → ℝ) (M : ℝ) (hM : ∀ (t : ℝ), 0 ≤ t → |f t| ≤ M) (g : ℂ → ℂ) (hg_holo : DifferentiableOn ℂ g {s : ℂ | 0 ≤ s.re}) (hg_laplace : ∀ (s : ℂ), 0 < s.re → g s = laplace_transform f s) (r : ℝ) (hr : 0 < r) : ∃ (I_right : ℝ → ℂ) (I_left : ℝ → ℂ), (∀ (τ : ℝ), g 0 - ↑(∫ (t : ℝ) in Set.Ioc 0 τ, f t) = I_right τ + I_left τ) ∧ (∀ (τ : ℝ), ‖I_right τ‖ ≤ 1 / r) ∧ ∀ᶠ (τ : ℝ) in Filter.atTop, ‖I_left τ‖ ≤ 1 / r

theorem Chapter16.newman_contour_split (f : ℝ → ℝ) (M : ℝ) (hM : ∀ (t : ℝ), 0 ≤ t → |f t| ≤ M) (g : ℂ → ℂ) (hg_holo : DifferentiableOn ℂ g {s : ℂ | 0 ≤ s.re}) (hg_laplace : ∀ (s : ℂ), 0 < s.re → g s = laplace_transform f s) (r : ℝ) (hr : 0 < r) : ∃ (I_right : ℝ → ℂ) (I_left : ℝ → ℂ), (∀ (τ : ℝ), g 0 - ↑(∫ (t : ℝ) in Set.Ioc 0 τ, f t) = I_right τ + I_left τ) ∧ (∀ (τ : ℝ), ‖I_right τ‖ ≤ 1 / r) ∧ ∀ᶠ (τ : ℝ) in Filter.atTop, ‖I_left τ‖ ≤ 2 / r

theorem Chapter16.newman_contour_bound (f : ℝ → ℝ) (M : ℝ) (hM : ∀ (t : ℝ), 0 ≤ t → |f t| ≤ M) (g : ℂ → ℂ) (hg_holo : DifferentiableOn ℂ g {s : ℂ | 0 ≤ s.re}) (hg_laplace : ∀ (s : ℂ), 0 < s.re → g s = laplace_transform f s) (r : ℝ) (hr : 0 < r) : ∀ᶠ (τ : ℝ) in Filter.atTop, ‖g 0 - ↑(∫ (t : ℝ) in Set.Ioc 0 τ, f t)‖ ≤ 3 / r

theorem Chapter16.newman_key_convergence (f : ℝ → ℝ) (M : ℝ) (hM : ∀ (t : ℝ), 0 ≤ t → |f t| ≤ M) (g : ℂ → ℂ) (hg_holo : DifferentiableOn ℂ g {s : ℂ | 0 ≤ s.re}) (hg_laplace : ∀ (s : ℂ), 0 < s.re → g s = laplace_transform f s) : Filter.Tendsto (fun (τ : ℝ) => ↑(∫ (t : ℝ) in Set.Ioc 0 τ, f t)) Filter.atTop (nhds (g 0))

theorem Chapter16.thm_16_13_newman_tauberian (f : ℝ → ℝ) (hf_bound : ∃ (M : ℝ), ∀ (t : ℝ), 0 ≤ t → |f t| ≤ M) (g : ℂ → ℂ) (hg_holo : DifferentiableOn ℂ g {s : ℂ | 0 ≤ s.re}) (hg_laplace : ∀ (s : ℂ), 0 < s.re → g s = laplace_transform f s) : ∃ (L : ℝ), Filter.Tendsto (fun (x : ℝ) => ∫ (t : ℝ) in Set.Ioc 0 x, f t) Filter.atTop (nhds L) ∧ ↑L = g 0

noncomputable def Chapter16.H (t : ℝ) : ℝ

theorem Chapter16.H_bounded : ∃ (M : ℝ), ∀ (t : ℝ), 0 ≤ t → |H t| ≤ M

theorem Chapter16.laplace_H_identity (s : ℂ) (hs : 0 < s.re) : laplace_transform H s = Phi (s + 1) / (s + 1) - 1 / s

theorem Chapter16.cor_16_12_Phi_shift_meromorphic : ∃ (g : ℂ → ℂ), MeromorphicOn g {s : ℂ | -1 / 2 < s.re} ∧ ∀ (s : ℂ), 0 < s.re → g s = Phi (s + 1) - 1 / s

theorem Chapter16.cor_16_12_laplace_H_holomorphic : ∃ (g : ℂ → ℂ), DifferentiableOn ℂ g {s : ℂ | 0 ≤ s.re} ∧ ∀ (s : ℂ), 0 < s.re → g s = Phi (s + 1) / (s + 1) - 1 / s

theorem Chapter16.H_integral_change_of_variables (T : ℝ) (hT : 0 ≤ T) : ∫ (t : ℝ) in Set.Ioc 0 T, H t = ∫ (x : ℝ) in Set.Ioc 1 (Real.exp T), (Chebyshev.theta x - x) / x ^ 2

theorem Chapter16.integral_theta_minus_id_convergent : ∃ (L : ℝ), Filter.Tendsto (fun (x : ℝ) => ∫ (t : ℝ) in Set.Ioc 1 x, (Chebyshev.theta t - t) / t ^ 2) Filter.atTop (nhds L)

theorem Chapter16.theta_asymptotic : Asymptotics.IsEquivalent Filter.atTop (fun (x : ℝ) => Chebyshev.theta x) fun (x : ℝ) => x

theorem Chapter16.thm_16_15_PNT : Asymptotics.IsEquivalent Filter.atTop (fun (x : ℝ) => ↑⌊x⌋₊.primeCounting) fun (x : ℝ) => x / Real.log x