Source indexedtheorem · leanprover/lean4:v4.32.0

BKLNW.lemma_11a

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:74 to 85

Mathematical statement

Exact Lean statement

@[blueprint
  "bklnw-lemma-11a"
  (title := "BKLNW Lemma 11a")
  (statement := /-- With the hypotheses as above, we have $\theta(x) \leq (1+\eps(\log x_1)) x)$ for all $x > 0$.-/)
  (proof := /-- Follows immediately from the given hypothesis $\theta(x) \leq \psi(x)$, splitting into the cases $x ≥ x_1$ and $x < x_1$. -/)
  (latexEnv := "lemma")
  (discussion := 788)]
theorem lemma_11a (I : Pre_inputs) {x : ℝ} (hx : x > 0) : θ x ≤ (1 + I.ε (log I.x₁)) * x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "bklnw-lemma-11a"  (title := "BKLNW Lemma 11a")  (statement := /-- With the hypotheses as above, we have $\theta(x) \leq (1+\eps(\log x_1)) x)$ for all $x > 0$.-/)  (proof := /-- Follows immediately from the given hypothesis $\theta(x) \leq \psi(x)$, splitting into the cases $x ≥ x_1$ and $x < x_1$. -/)  (latexEnv := "lemma")  (discussion := 788)]theorem lemma_11a (I : Pre_inputs) {x : ℝ} (hx : x > 0) : θ x ≤ (1 + I.ε (log I.x₁)) * x := by  have hx₁_pos : 1 ≤ I.x₁ := (one_le_exp (7).ofNat_nonneg).trans I.hx₁  by_cases h : x ≤ I.x₁  · grw [I.hx₁' x ⟨hx, h⟩, ← I.epsilon_nonneg (Real.log_nonneg hx₁_pos), add_zero, one_mul]  · grw [add_mul, theta_le_psi, ← I.hε _ (Real.log_nonneg hx₁_pos)] <;> grind [exp_log]