Source indexedtheorem · leanprover/lean4:v4.32.0

Mertens.E₃.bound''

PrimeNumberTheoremAnd.IEANTN.Mertens · PrimeNumberTheoremAnd/IEANTN/Mertens.lean:2418 to 2429

Mathematical statement

Exact Lean statement

@[blueprint
  "Mertens-third-theorem-error-le"]
theorem E₃.bound'' : (fun x ↦ ∏ p ∈ Ioc 0 ⌊ x ⌋₊ with p.Prime, (1 - (1:ℝ) / p)) ~[atTop] (fun x ↦ exp (-eulerMascheroniConstant) / log x)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "Mertens-third-theorem-error-le"]theorem E₃.bound'' : (fun x ↦ ∏ p ∈ Ioc 0 ⌊ x ⌋₊ with p.Prime, (1 - (1:ℝ) / p)) ~[atTop] (fun x ↦ exp (-eulerMascheroniConstant) / log x) := by   rw [isEquivalent_iff_tendsto_one]   · convert Tendsto.congr' ?_ (Tendsto.rexp ((isLittleO_one_iff ℝ).mp E₃.bound')) using 2 with x     · simp     simp only [EventuallyEq.iff_eventually, Pi.div_apply, eventually_atTop]; use 2; intro x hx     rw [prod_one_minus_div_prime_eq (by linarith)]     have : 0 < log x := by apply log_pos; linarith     field_simp   simp only [ne_eq, div_eq_zero_iff, exp_ne_zero, log_eq_zero, eventually_atTop]; use 2   grind