Mertens.sum_log_eq

@[blueprint  "Mertens-sum-log"  (title := "Partial sum of logarithm identity")  (statement := /-- For any $x \geq 1$, one has$$ \sum_{n \leq x} \log n = x \log x - (\{ x \}-1/2) \log x - x + 1 + \int_1^x (\{ t \}-1/2) \frac{dt}{t} $$(NOTE: this identity is not actually needed in the proof of Mertens' theorems, but may be worth recording nevertheless.) -/)  (proof := /-- Apply the Euler-Maclaurin formula. -/)  (latexEnv := "lemma")  (discussion := 1303)]theorem sum_log_eq {x : ℝ} (hx : 1 ≤ x) :    ∑ n ∈ Ioc 0 ⌊ x ⌋₊, log n =      x * log x - (x - ⌊x⌋₊ - 1 / 2) * log x - x + 1 + ∫ t in 1..x, (t - ⌊t⌋₊ - 1 / 2) / t := by  rw [← sum_Ioc_one_eq_sum_Ioc_zero (Nat.le_floor (by grind)) (by simp)]  have : 1 = ⌊(1 : ℝ)⌋₊ := by simp  nth_rw 1 [this]  rw [sum_eq_integral_add_integral_deriv (by norm_num) hx (fun _ _ ↦ (by fun_prop (disch := grind)))]  · simp only [log_one, B1, Nat.floor_one, Nat.cast_one, sub_self, zero_sub,    RCLike.ofReal_real_eq_id, id_eq, mul_neg, zero_mul, neg_zero, integral_log, mul_zero, sub_zero,    deriv_log']    ring_nf    congr    ext    ring  · simp only [deriv_log', Set.uIcc_of_le hx]    fun_prop (disch := grind)