feat(NumberTheory.Chebyshev): prove connection between prime counting and theta (leanprover-community#32281)

Uses Abel summation to express the prime counting function in terms of the Chebyshev theta function. This upstreams some results from PrimeNumberTheoremAnd.

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

Author: 3 people

Mathlib.lean

@@ -2135,6 +2135,7 @@ public import Mathlib.Analysis.SpecialFunctions.Log.Deriv
 public import Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
 public import Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
 public import Mathlib.Analysis.SpecialFunctions.Log.ERealExp
+public import Mathlib.Analysis.SpecialFunctions.Log.InvLog
 public import Mathlib.Analysis.SpecialFunctions.Log.Monotone
 public import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
 public import Mathlib.Analysis.SpecialFunctions.Log.PosLog

Mathlib/Analysis/SpecialFunctions/Log/InvLog.lean

@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2025 Alastair Irving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alastair Irving, Michael Stoll
+-/
+
+module
+
+public import Mathlib.Analysis.SpecialFunctions.Log.Deriv
+public import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
+
+/-!
+# Multiplicative inverse of real logarithm
+
+We prove properties of the function `x ↦ (log x)⁻¹`.
+
+## Main results
+
+- `deriv_inv_log` gives a formula for the derivative which holds for all values.
+-/
+
+@[expose] public section
+
+namespace Real
+
+open Filter
+
+lemma not_differentiableAt_inv_log_zero : ¬ DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) 0 := by
+  simp only [← hasDerivAt_deriv_iff, hasDerivAt_iff_tendsto_slope_zero, zero_add, log_zero,
+    inv_zero, sub_zero, smul_eq_mul, ← mul_inv, mul_comm _ (log _)]
+  have H' : Tendsto (fun x ↦ log x * x) (nhdsWithin 0 (Set.Iio 0)) (nhdsWithin 0 (Set.Ioi 0)) := by
+    refine tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
+      tendsto_log_mul_self_nhdsLT_zero ?_
+    simp only [← nhdsWithin_Ioo_eq_nhdsLT neg_one_lt_zero, Set.mem_Ioi]
+    refine eventually_nhdsWithin_of_forall fun x ⟨hx₁, hx₂⟩ ↦ mul_pos_of_neg_of_neg ?_ hx₂
+    refine log_neg_eq_log x ▸ log_neg ?_ ?_ <;> grind
+  exact fun H ↦ (tendsto_nhdsWithin_mono_left (show Set.Iio (0 : ℝ) ⊆ _ by grind) H).not_tendsto
+    (by simp) (tendsto_inv_nhdsGT_zero.comp H')
+
+lemma not_continuousAt_inv_log_one : ¬ ContinuousAt (fun x ↦ (log x)⁻¹) 1 := by
+  suffices Tendsto (fun x ↦ (log x)⁻¹) (nhdsWithin 1 {1}ᶜ) (Bornology.cobounded ℝ) from
+    not_continuousAt_of_tendsto this nhdsWithin_le_nhds (Metric.disjoint_nhds_cobounded _)
+  have H := HasDerivAt.tendsto_nhdsNE (by simpa using hasDerivAt_log one_ne_zero) one_ne_zero
+  exact tendsto_inv₀_nhdsNE_zero.comp <| log_one ▸ H
+
+lemma not_continuousAt_inv_log_neg_one : ¬ ContinuousAt (fun x ↦ (log x)⁻¹) (-1) := by
+  refine fun H ↦ not_continuousAt_inv_log_one ?_
+  simpa only [log_neg_eq_log] using ContinuousAt.comp' H continuousAt_neg
+
+theorem deriv_inv_log {x : ℝ} :
+    deriv (fun x ↦ (log x)⁻¹) x = -x⁻¹ / (log x ^ 2) := by
+  rcases eq_or_ne x 0 with rfl | h0
+  · simpa using deriv_zero_of_not_differentiableAt not_differentiableAt_inv_log_zero
+  rcases eq_or_ne x 1 with rfl | h1
+  · simpa using deriv_zero_of_not_differentiableAt <|
+      mt DifferentiableAt.continuousAt not_continuousAt_inv_log_one
+  rcases eq_or_ne x (-1) with rfl | h2
+  · simpa using deriv_zero_of_not_differentiableAt <|
+      mt DifferentiableAt.continuousAt not_continuousAt_inv_log_neg_one
+  simp_all
+
+end Real

Mathlib/Computability/AkraBazzi/SumTransform.lean

@@ -10,6 +10,8 @@ public import Mathlib.Analysis.Calculus.Deriv.Inv
 public import Mathlib.Analysis.SpecialFunctions.Pow.Continuity
 public import Mathlib.Analysis.SpecialFunctions.Log.Deriv
 
+import Mathlib.Analysis.SpecialFunctions.Log.InvLog
+
 /-!
 # Akra-Bazzi theorem: the sum transform
 
@@ -353,16 +355,16 @@ lemma differentiableAt_one_add_smoothingFn {x : ℝ} (hx : 1 < x) :
 lemma differentiableOn_one_add_smoothingFn : DifferentiableOn ℝ (fun z => 1 + ε z) (Set.Ioi 1) :=
   fun _ hx => (differentiableAt_one_add_smoothingFn hx).differentiableWithinAt
 
-lemma deriv_smoothingFn {x : ℝ} (hx : 1 < x) : deriv ε x = -x⁻¹ / (log x ^ 2) := by
-  have : log x ≠ 0 := Real.log_ne_zero_of_pos_of_ne_one (by positivity) (ne_of_gt hx)
-  change deriv (fun z => 1 / log z) x = -x⁻¹ / (log x ^ 2)
-  rw [deriv_fun_div] <;> aesop
+lemma deriv_smoothingFn {x : ℝ} : deriv ε x = -x⁻¹ / (log x ^ 2) := by
+  unfold smoothingFn
+  simp_rw [one_div]
+  apply deriv_inv_log
 
 lemma isLittleO_deriv_smoothingFn : deriv ε =o[atTop] fun x => x⁻¹ :=
   calc deriv ε
     _ =ᶠ[atTop] fun x => -x⁻¹ / (log x ^ 2) := by
-      filter_upwards [eventually_gt_atTop 1] with x hx
-      rw [deriv_smoothingFn hx]
+      filter_upwards with x
+      rw [deriv_smoothingFn]
     _ = fun x => (-x * log x ^ 2)⁻¹ := by
       simp_rw [neg_div, div_eq_mul_inv, ← mul_inv, neg_inv, neg_mul]
     _ =o[atTop] fun x => (x * 1)⁻¹ := by
@@ -381,17 +383,17 @@ lemma eventually_deriv_one_sub_smoothingFn :
     _ =ᶠ[atTop] -(deriv ε) := by
       filter_upwards [eventually_gt_atTop 1] with x hx; rw [deriv_fun_sub] <;> aesop
     _ =ᶠ[atTop] fun x => x⁻¹ / (log x ^ 2) := by
-      filter_upwards [eventually_gt_atTop 1] with x hx
-      simp [deriv_smoothingFn hx, neg_div]
+      filter_upwards with x
+      simp [deriv_smoothingFn, neg_div]
 
 lemma eventually_deriv_one_add_smoothingFn :
     deriv (fun x => 1 + ε x) =ᶠ[atTop] fun x => -x⁻¹ / (log x ^ 2) :=
   calc deriv (fun x => 1 + ε x)
     _ =ᶠ[atTop] deriv ε := by
       filter_upwards [eventually_gt_atTop 1] with x hx; rw [deriv_fun_add] <;> aesop
     _ =ᶠ[atTop] fun x => -x⁻¹ / (log x ^ 2) := by
-      filter_upwards [eventually_gt_atTop 1] with x hx
-      simp [deriv_smoothingFn hx]
+      filter_upwards with x
+      simp [deriv_smoothingFn]
 
 lemma isLittleO_deriv_one_sub_smoothingFn :
     deriv (fun x => 1 - ε x) =o[atTop] fun (x : ℝ) => x⁻¹ :=

Mathlib/NumberTheory/AbelSummation.lean

@@ -235,6 +235,30 @@ theorem sum_mul_eq_sub_integral_mul₀' (hc : c 0 = 0) (m : ℕ)
   convert sum_mul_eq_sub_integral_mul₀ c hc m hf_diff hf_int
   all_goals rw [Nat.floor_natCast]
 
+/-- Specialized version of `sum_mul_eq_sub_integral_mul` when `c 0 = c 1 = 0`. -/
+theorem sum_mul_eq_sub_integral_mul₁ (hc : c 0 = 0) (hc1 : c 1 = 0) (b : ℝ)
+    (hf_diff : ∀ t ∈ Set.Icc 2 b, DifferentiableAt ℝ f t)
+    (hf_int : IntegrableOn (deriv f) (Set.Icc 2 b)) :
+    ∑ k ∈ Icc 0 ⌊b⌋₊, f k * c k =
+      f b * (∑ k ∈ Icc 0 ⌊b⌋₊, c k) - ∫ t in Set.Ioc 2 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k := by
+  by_cases! hb : b < 2
+  · -- Easy case, everything is 0
+    have H₁ : ∀ n ∈ Icc 0 ⌊b⌋₊, c n = 0 := by grind [(Nat.floor_lt' two_ne_zero).mpr hb]
+    have H₂ : ∀ n ∈ Icc 0 ⌊b⌋₊, f n * c n = 0 := by grind
+    simp [sum_eq_zero H₁, sum_eq_zero H₂, Set.Ioc_eq_empty_of_le hb.le]
+  -- Split off the first two terms of the sum
+  have : 2 ≤ ⌊b⌋₊ := Nat.le_floor hb
+  have H : ∑ k ∈ Icc 0 ⌊b⌋₊, f ↑k * c k = f (2 :) * c 2 + ∑ k ∈ Ioc 2 ⌊b⌋₊, f ↑k * c k := by
+    rw [add_sum_Ioc_eq_sum_Icc (f := fun (k : ℕ) ↦ f k * c k) this,
+      show Icc 0 ⌊b⌋₊ = {0, 1} ∪ Icc 2 ⌊b⌋₊ by grind]
+    exact sum_union_eq_right fun k hk hk' ↦ by grind
+  rw [H]
+  -- Apply Abel summation to the remainder
+  nth_rewrite 3 [show 2 = ⌊(2 : ℝ)⌋₊ by simp]
+  rw [sum_mul_eq_sub_sub_integral_mul c zero_le_two hb hf_diff hf_int]
+  simp [show Icc 0 2 = {0, 1, 2} by rfl, hc, hc1]
+  grind
+
 end specialversions
 
 section limit

Mathlib/NumberTheory/Chebyshev.lean

@@ -5,10 +5,15 @@ Authors: Alastair Irving, Terry Tao, Ruben Van de Velde
 -/
 module
 
+public import Mathlib.Algebra.Order.Floor.Semifield
 public import Mathlib.Analysis.SpecialFunctions.Pow.Real
+public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
+public import Mathlib.NumberTheory.AbelSummation
+public import Mathlib.NumberTheory.PrimeCounting
 public import Mathlib.NumberTheory.Primorial
 public import Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
 
+import Mathlib.Analysis.SpecialFunctions.Log.InvLog
 import Mathlib.Data.Nat.Prime.Int
 
 /-!
@@ -28,6 +33,8 @@ These give logarithmically weighted sums of primes and prime powers.
 - `Chebyshev.theta_le_log4_mul_x` gives Chebyshev's upper bound on `θ`
 - `Chebyshev.psi_eq_sum_theta` and `Chebyshev.psi_eq_theta_add_sum_theta` relate `psi` to `theta`.
 - `Chebyshev.psi_le_const_mul_self` gives Chebyshev's upper bound on `ψ`.
+- `Chebyshev.primeCounting_eq_theta_div_log_add_integral` relates the prime counting function to `θ`
+- `Chebyshev.eventually_primeCounting_le` gives an upper bound on the prime counting function.
 
 ## Notation
 
@@ -40,14 +47,14 @@ Parts of this file were upstreamed from the PrimeNumberTheoremAnd project by Kon
 
 ## TODOS
 
-- Upstream the results relating `theta` and `psi` to the prime counting function.
 - Prove Chebyshev's lower bound.
 -/
 @[expose] public section
 
 open Nat hiding log
 open Finset Real
 open ArithmeticFunction hiding log
+open scoped Nat.Prime
 
 namespace Chebyshev
 
@@ -269,4 +276,172 @@ theorem psi_sub_theta_eq_sum_not_prime (x : ℝ) :
   · simp [h, vonMangoldt_apply_prime]
   · simp
 
+section PrimeCounting
+
+/-! ## Relation to prime counting
+
+We relate `θ` to the prime counting function `π`.-/
+
+open Asymptotics Filter MeasureTheory
+
+/-- Integrability for the integral in `Chebyshev.primeCounting_eq_theta_div_log_add_integral`. -/
+theorem integrableOn_theta_div_id_mul_log_sq (x : ℝ) :
+    IntegrableOn (fun t ↦ θ t / (t * log t ^ 2)) (Set.Icc 2 x) volume := by
+  conv => arg 1; ext; rw [theta, div_eq_mul_one_div, mul_comm, sum_filter]
+  refine integrableOn_mul_sum_Icc _ (by norm_num) <| ContinuousOn.integrableOn_Icc fun x hx ↦
+    ContinuousAt.continuousWithinAt ?_
+  have : x ≠ 0 := by linarith [hx.1]
+  have : x * log x ^ 2 ≠ 0 := mul_ne_zero this <| by simp; grind
+  fun_prop (disch := assumption)
+
+/-- Expresses the prime counting function `π` in terms of `θ` by using Abel summation. -/
+theorem primeCounting_eq_theta_div_log_add_integral {x : ℝ} (hx : 2 ≤ x) :
+    π ⌊x⌋₊ = θ x / log x + ∫ t in 2..x, θ t / (t * log t ^ 2) := by
+  -- Rewrite in a form to which Abel summation can be applied
+  simp only [primeCounting, primeCounting', count_eq_card_filter_range]
+  rw [card_eq_sum_ones, range_succ_eq_Icc_zero, sum_filter]
+  push_cast
+  let a : ℕ → ℝ := Set.indicator (setOf Nat.Prime) (fun n ↦ log n)
+  trans ∑ n ∈ Icc 0 ⌊x⌋₊, (log n)⁻¹ * a n
+  · refine sum_congr rfl fun n hn ↦ ?_
+    split_ifs with h
+    · have : log n ≠ 0 := log_ne_zero_of_pos_of_ne_one (mod_cast h.pos) (mod_cast h.ne_one)
+      simp [a, h, field]
+    · simp [a, h]
+  rw [sum_mul_eq_sub_integral_mul₁ a (f := fun n ↦ (log n)⁻¹) (by simp [a]) (by simp [a]),
+    ← intervalIntegral.integral_of_le hx]
+  · -- Rewrite the derivative inside the intigral
+    have int_deriv (f : ℝ → ℝ) :
+        ∫ u in 2..x, deriv (fun x ↦ (log x)⁻¹) u * f u =
+        ∫ u in 2..x, f u * -(u * log u ^ 2)⁻¹ :=
+      intervalIntegral.integral_congr fun u _ ↦ by simp [deriv_inv_log, field]
+    simp [int_deriv, a, Set.indicator_apply, sum_filter, theta_eq_sum_Icc]
+    grind
+  · -- Differentiability
+    intro z ⟨hz, _⟩
+    have : z ≠ 0 := by linarith
+    have : log z ≠ 0 := by apply log_ne_zero_of_pos_of_ne_one <;> linarith
+    fun_prop (disch := assumption)
+  · -- Integrability of the derivative
+    refine ContinuousOn.integrableOn_Icc fun z ⟨hz, _⟩ ↦ ContinuousWithinAt.congr ?_
+      (fun _ _ ↦ deriv_inv_log) deriv_inv_log
+    have hz₀ : z ≠ 0 := by linarith
+    have : log z ^ 2 ≠ 0 := by
+      refine pow_ne_zero 2 <| log_ne_zero_of_pos_of_ne_one ?_ ?_ <;> linarith
+    exact ContinuousAt.continuousWithinAt <| by fun_prop (disch := assumption)
+
+theorem intervalIntegrable_one_div_log_sq {a b : ℝ} (one_lt_a : 1 < a) (one_lt_b : 1 < b) :
+    IntervalIntegrable (fun x ↦ 1 / log x ^ 2) MeasureTheory.volume a b := by
+  refine ContinuousOn.intervalIntegrable fun x hx ↦ ContinuousAt.continuousWithinAt ?_
+  rw [Set.mem_uIcc] at hx
+  have : x ≠ 0 := by grind
+  have : log x ^ 2 ≠ 0 := pow_ne_zero _ (log_ne_zero.mpr (by grind))
+  fun_prop (disch := assumption)
+
+/- Simple bound on the integral from monotonicity.
+We will bound the integral on 2..x by splitting into two intervals and using this result on both. -/
+private theorem integral_1_div_log_sq_le {a b : ℝ} (hab : a ≤ b) (one_lt : 1 < a) :
+    ∫ x in a..b, 1 / log x ^ 2 ≤ (b - a) / log a ^ 2 := by
+  calc
+  _ ≤ ∫ x in a..b, 1 / log a ^ 2 := by
+      refine intervalIntegral.integral_mono_on hab ?_ (by simp) fun x ⟨hx, _⟩ ↦ by gcongr <;> bound
+      apply intervalIntegrable_one_div_log_sq <;> linarith
+  _ ≤ _ := by simp [field]
+
+/- Explicit integral bound, we expose a BigO version below since the constants and lower order term
+aren't very convenient. -/
+private theorem integral_one_div_log_sq_le_explicit {x : ℝ} (hx : 4 ≤ x) :
+    ∫ t in 2..x, 1 / log t ^ 2 ≤ 4 * x / (log x) ^ 2 + x.sqrt / log 2 ^ 2 := by
+  have two_le_sqrt : 2 ≤ x.sqrt := Real.le_sqrt_of_sq_le <| by norm_num [hx]
+  have sqrt_le_x : x.sqrt ≤ x := sqrt_le_left (by linarith) |>.mpr (by bound)
+  rw [← intervalIntegral.integral_add_adjacent_intervals (b := x.sqrt)]
+  · grw [integral_1_div_log_sq_le two_le_sqrt (by linarith),
+      integral_1_div_log_sq_le sqrt_le_x (by linarith)]
+    rw [log_sqrt (by linarith), add_comm, div_pow, ← div_mul, mul_comm, mul_div_assoc]
+    norm_num
+    gcongr <;> linarith
+  all_goals apply intervalIntegrable_one_div_log_sq <;> linarith
+
+-- Somewhat arbitrary bound which we use to estimate the second term.
+private theorem sqrt_isLittleO :
+    Real.sqrt =o[atTop] (fun x ↦ x / log x ^ 2) := by
+  apply isLittleO_mul_iff_isLittleO_div _|>.mp
+  · conv => arg 2; ext; rw [mul_comm]
+    apply isLittleO_mul_iff_isLittleO_div _|>.mpr
+    · simp_rw [div_sqrt, sqrt_eq_rpow, ← rpow_two]
+      apply isLittleO_log_rpow_rpow_atTop _ (by norm_num)
+    filter_upwards [eventually_gt_atTop 0] with x hx using sqrt_ne_zero'.mpr hx
+  filter_upwards [eventually_gt_atTop 1] with x hx
+  apply pow_ne_zero _ <| log_ne_zero.mpr ⟨_, _, _⟩ <;> linarith
+
+theorem integral_one_div_log_sq_isBigO :
+    (fun x ↦ ∫ t in 2..x, 1 / log t ^ 2) =O[atTop] (fun x ↦ x / log x ^ 2) := by
+  trans (fun x ↦  4 * x / log x ^ 2 + √x / log 2 ^ 2)
+  · apply IsBigO.of_bound'
+    filter_upwards [eventually_ge_atTop 4] with x hx
+    apply le_trans <| intervalIntegral.abs_integral_le_integral_abs (by linarith)
+    rw [intervalIntegral.integral_congr (g := (fun t ↦ 1 / log t ^ 2))]
+    · grw [integral_one_div_log_sq_le_explicit hx, norm_of_nonneg]
+      positivity
+    intro t ht
+    simp
+  refine IsBigO.add ?_ ?_
+  · simp_rw [mul_div_assoc]
+    apply isBigO_const_mul_self
+  conv => arg 2; ext; rw [← mul_one_div, mul_comm]
+  apply IsBigO.const_mul_left sqrt_isLittleO.isBigO
+
+/-- Bound on the integral in `Chebyshev.primeCounting_eq_theta_div_log_add_integral`. -/
+theorem integral_theta_div_log_sq_isBigO :
+    (fun x ↦ ∫ t in 2..x, θ t / (t * log t ^ 2)) =O[atTop] (fun x ↦ x / log x ^ 2) := by
+  refine (IsBigO.of_bound (log 4) ?_).trans integral_one_div_log_sq_isBigO
+  filter_upwards [eventually_ge_atTop 4] with x hx
+  simp_rw [norm_eq_abs]
+  calc |∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)|
+    _ ≤ ∫ (x : ℝ) in 2..x, |θ x / (x * log x ^ 2)| :=
+        intervalIntegral.abs_integral_le_integral_abs (by linarith)
+    _ ≤ ∫ (x : ℝ) in 2..x, log 4 * (1 / log x ^ 2) :=
+        intervalIntegral.integral_mono_on (by linarith) ?hf ?hg fun t ⟨ht, _⟩ ↦ ?hh
+    _ = log 4 * |∫ (t : ℝ) in 2..x, 1 / log t ^ 2| := by
+        rw [intervalIntegral.integral_const_mul, abs_of_nonneg]
+        exact intervalIntegral.integral_nonneg (by linarith) fun u _ ↦ by positivity
+  case hf =>
+    refine (intervalIntegrable_iff.mpr ?_).abs
+    rw [Set.uIoc_of_le (by linarith), ← integrableOn_Icc_iff_integrableOn_Ioc]
+    exact integrableOn_theta_div_id_mul_log_sq x
+  case hg =>
+    refine (intervalIntegrable_one_div_log_sq ?_ ?_).const_mul _ <;> linarith
+  case hh =>
+    calc |θ t / (t * log t ^ 2)|
+    _ = θ t / (t * log t ^ 2) := abs_of_nonneg (by positivity [theta_nonneg t])
+    _ ≤ log 4 * t / (t * log t ^ 2) := by grw [theta_le_log4_mul_x (by linarith)]
+    _ = log 4 * (1 / log t ^ 2) := by field
+
+theorem integral_theta_div_log_sq_isLittleO :
+    (fun x ↦ ∫ t in 2..x, θ t / (t * log t ^ 2)) =o[atTop] (fun x ↦ x / log x) := by
+  refine integral_theta_div_log_sq_isBigO.trans_isLittleO ?_
+  refine isLittleO_iff_tendsto' (by simp) |>.mpr ?_
+  refine Tendsto.congr' (f₁ := fun x ↦ (log x)⁻¹) ?_ tendsto_log_atTop.inv_tendsto_atTop
+  filter_upwards [eventually_gt_atTop 0] with x hx
+  field
+
+theorem primeCounting_sub_theta_div_log_isBigO :
+    (fun x ↦ π ⌊x⌋₊ - θ x / log x) =O[atTop] (fun x ↦ x / log x ^ 2) := by
+  apply integral_theta_div_log_sq_isBigO.congr' _ (by rfl)
+  filter_upwards [eventually_ge_atTop 2] with x hx
+  rw [primeCounting_eq_theta_div_log_add_integral hx]
+  simp
+
+/-- Chebyshev's upper bound on the prime counting function -/
+theorem eventually_primeCounting_le {ε : ℝ} (εpos : 0 < ε) :
+    ∀ᶠ x in atTop, π ⌊x⌋₊ ≤ (log 4 + ε) * x / log x := by
+  have := integral_theta_div_log_sq_isLittleO.bound εpos
+  filter_upwards [eventually_ge_atTop 2, this] with x hx hx2
+  rw [primeCounting_eq_theta_div_log_add_integral hx, add_mul, add_div]
+  have hl : 0 ≤ log x := by bound
+  rw [norm_of_nonneg (show 0 ≤ x / log x by bound), ← mul_div_assoc] at hx2
+  grw [theta_le_log4_mul_x (by linarith), ← hx2]
+  grind [le_norm_self]
+
+end PrimeCounting
 end Chebyshev