Source indexedtheorem · leanprover/lean4:v4.32.0

primorial_bounds

PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:278 to 299

Mathematical statement

Exact Lean statement

@[blueprint
  (title := "primorial-bounds")
  (statement := /--
  We have
    $$ \prod_{p \leq x} p = \exp( x + o(x) )$$
  -/)
  (proof := /-- Exponentiate Theorem \ref{chebyshev_asymptotic}. -/)
  (latexEnv := "corollary")]
theorem primorial_bounds :
    ∃ E : ℝ → ℝ, E =o[atTop] (fun x ↦ x) ∧
      ∀ x : ℝ, ∏ p ∈ (Iic ⌊x⌋₊).filter Nat.Prime, p = exp (x + E x)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  (title := "primorial-bounds")  (statement := /--  We have    $$ \prod_{p \leq x} p = \exp( x + o(x) )$$  -/)  (proof := /-- Exponentiate Theorem \ref{chebyshev_asymptotic}. -/)  (latexEnv := "corollary")]theorem primorial_bounds :    ∃ E : ℝ → ℝ, E =o[atTop] (fun x ↦ x) ∧      ∀ x : ℝ, ∏ p ∈ (Iic ⌊x⌋₊).filter Nat.Prime, p = exp (x + E x) := by  use (fun x ↦ ∑ p ∈ (filter Nat.Prime (Iic ⌊x⌋₊)), log p - x)  constructor  · exact Asymptotics.IsEquivalent.isLittleO chebyshev_asymptotic  intro x  simp only [cast_prod, add_sub_cancel, exp_sum]  apply Finset.prod_congr rfl  intros x hx  rw[Real.exp_log]  rw[Finset.mem_filter] at hx  norm_cast  exact Nat.Prime.pos hx.right