Mertens.sum_log_ge

@[blueprint  "Mertens-sum-log-ge"  (title := "Partial sum of logarithm lower bound")  (statement := /-- For any $x \geq 1$, one has$$ \sum_{n \leq x} \log n \geq x \log x - 2 x.$$ -/)  (proof := /-- We have \begin{align*} \sum_{n \leq x} \log n &= \sum_{2 \leq n \leq \lfloor x \rfloor} \log n \\ &\geq \sum_{2 \leq n \leq \lfloor x \rfloor} \int_{n-1}^n \log t \, dt \\ &= \int_1^{\lfloor x \rfloor} \log t \, dt \\ &\geq \int_1^x \log t\ dt - \log x \\ &= x \log x - x - \log x \\ &\geq x \log x - 2 x.\end{align*}Here we use the monotonicity of $\log n$ (and its vanishing at $n=1$) and the crude bound $\log x \leq x$. Note: the tools at Mathlib.Analysis.SumIntegralComparisons may be useful. -/)  (latexEnv := "corollary")  (discussion := 1305)]theorem sum_log_ge {x : ℝ} (hx : 1 ≤ x) :    ∑ n ∈ Ioc 0 ⌊ x ⌋₊, log n ≥ x * log x - 2 * x := by  have one_le_floor : 1 ≤ ⌊x⌋₊ := by simpa  calc  _ = ∑ n ∈ Icc 1 ⌊ x ⌋₊, log n := by rfl  _ = ∑ n ∈ Ico (1 + 1) (⌊ x ⌋₊ + 1), log n := by    rw [← add_sum_Ioc_eq_sum_Icc one_le_floor]    simp    rfl  _ = ∑ n ∈ Ico 1 ⌊ x ⌋₊, log ((n + 1 : ℕ)) := by    rw [← Finset.sum_Ico_add']  _ ≥ ∫ t in 1..⌊x⌋₊, log t := by    convert MonotoneOn.integral_le_sum_Ico one_le_floor ?_|>.ge    · norm_cast    · exact StrictMonoOn.monotoneOn (strictMonoOn_log.mono fun y hy ↦ (by simp_all; linarith))  _ = (∫ t in 1..x, log t) - ∫ t in ⌊x⌋₊..x, log t := by    nth_rw 3 [intervalIntegral.integral_symm]    rw [sub_neg_eq_add, intervalIntegral.integral_add_adjacent_intervals] <;> exact intervalIntegral.intervalIntegrable_log'  _ ≥ (∫ t in 1..x, log t) - log x := by    gcongr    grw [integral_log_le (by simpa) (Nat.floor_le (by linarith))]    nth_rw 2 [← mul_one (log x)]    gcongr    · exact log_nonneg hx    · linarith [Nat.lt_floor_add_one x]  _ ≥ x * log x - x - log x := by simp only [integral_log, log_one, mul_zero, sub_zero, ge_iff_le,    tsub_le_iff_right, sub_add_cancel, le_add_iff_nonneg_right, zero_le_one]  _ ≥ _ := by linarith [log_le_self (by linarith : 0 ≤ x)]