Source indexedtheorem · leanprover/lean4:v4.32.0

Mertens.sum_log_le

PrimeNumberTheoremAnd.IEANTN.Mertens · PrimeNumberTheoremAnd/IEANTN/Mertens.lean:342 to 363

Mathematical statement

Exact Lean statement

@[blueprint
  "Mertens-sum-log-le"
  (title := "Partial sum of logarithm upper bound")
  (statement := /-- For any $x \geq 1$, one has
$$ \sum_{n \leq x} \log n \leq x \log x.$$
 -/)
  (proof := /-- Trivial since $\log n \leq \log x$.
 -/)
  (latexEnv := "lemma")
  (discussion := 1304)]
theorem sum_log_le {x : ℝ} (hx : 1 ≤ x) :
    ∑ n ∈ Ioc 0 ⌊ x ⌋₊, log n ≤ x * log x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "Mertens-sum-log-le"  (title := "Partial sum of logarithm upper bound")  (statement := /-- For any $x \geq 1$, one has$$ \sum_{n \leq x} \log n \leq x \log x.$$ -/)  (proof := /-- Trivial since $\log n \leq \log x$. -/)  (latexEnv := "lemma")  (discussion := 1304)]theorem sum_log_le {x : ℝ} (hx : 1 ≤ x) :    ∑ n ∈ Ioc 0 ⌊ x ⌋₊, log n ≤ x * log x := by  calc  _ ≤ ∑ n ∈ Ioc 0 ⌊ x ⌋₊, log x := by    refine sum_le_sum fun n hn ↦ ?_    simp only [mem_Ioc] at hn    exact log_le_log (by exact_mod_cast hn.1) (Nat.le_floor_iff (by linarith)|>.mp hn.2)  _ = ⌊x⌋₊ * log x := by simp  _ ≤ _ := by    gcongr    · exact log_nonneg hx    · exact Nat.floor_le (by linarith)