Source indexedtheorem · leanprover/lean4:v4.32.0

BKLNW.thm_1a_crit

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:160 to 174

Mathematical statement

Exact Lean statement

@[blueprint
  "bklnw-thm-1a-checked"
  (statement := /-- One has $x(1-m) \leq \theta(x) \leq x(1+M)$ whenever $x \geq e^b$ and $b,M,m$ obey the condition that $b \geq 20$, $\eps(b) \leq M$, and $\eps(b) + c_0 (e^{-b/2} + e^{-2b/3} + e^{-4b/5}) \leq m$. -/)
  (latexEnv := "theorem")
  (discussion := 801)]
theorem thm_1a_crit {b M m : ℝ} (h_check : check_row_prop (b, M, m)) {x : ℝ} (hx : x ≥ exp b) :
    x * (1 - m) ≤ θ x ∧ θ x ≤ x * (1 + M)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "bklnw-thm-1a-checked"  (statement := /-- One has $x(1-m) \leq \theta(x) \leq x(1+M)$ whenever $x \geq e^b$ and $b,M,m$ obey the condition that $b \geq 20$, $\eps(b) \leq M$, and $\eps(b) + c_0 (e^{-b/2} + e^{-2b/3} + e^{-4b/5}) \leq m$. -/)  (latexEnv := "theorem")  (discussion := 801)]theorem thm_1a_crit {b M m : ℝ} (h_check : check_row_prop (b, M, m)) {x : ℝ} (hx : x ≥ exp b) :    x * (1 - m) ≤ θ x ∧ θ x ≤ x * (1 + M) := by  obtain ⟨hb, hM, hm⟩ := h_check  have := thm_1a (exp_le_exp.mpr hb) (exp_le_exp.mpr hb) hx hx  simp only at hm hM this  simp only [log_exp b, rpow_def_of_pos (exp_pos b)] at this  have h : 0 ≤ x := (exp_pos b).le.trans hx  grw [← hm, ← hM]  rw [show Pre_inputs.default.ε = BKLNW_app.table_8_ε by rfl] at this  grind