Theorem: primorial_bounds_finprod (PrimeNumberTheoremAnd/Consequences.lean)

State before:
⊢ ∃ E, (E =o[atTop] fun x => x) ∧ ∀ (x : ℝ), ↑(∏ᶠ (p : ℕ) (_ : ↑p ≤ x) (_ : p.Prime), p) = rexp (x + E x)
Tactic:
sorry
State after:
no goals