Bounding ∑ (log Y)²/(Y(Y+1)) in Lean: telescope against an antiderivative

To bound ∑_{Y≤M} (log Y)²/(Y(Y+1)) without integrals, take f(y) = ((log y)² + 3 log y + 3)/y. This is a slightly loosened version of the antiderivative ((log y)² + 2 log y + 2)/y of (log t)²/t². Prove term ≤ f(Y) − f(Y+1) for natural Y ≥ 1, then use induction with sum_Icc_succ_top, which gives ≤ 3 − f(M+1) ≤ 3. With d = log(Y+1) − log Y, the inequality reduces to Y·d·(2L + d + 3) ≤ 3L + 3. Y·d ≤ 1 follows from Real.log_le_sub_one_of_pos at (Y+1)/Y. For Y ≥ 2 you need d ≤ 1/2 ≤ log 2 ≤ L. Y = 1 is checked by hand with Real.log_two_lt_d9. The exact antiderivative (coefficient 2) needs log(1+x) ≤ x − x²/2 + x³/3, which is more work; coefficient 3 avoids that. Applied to Romanov's theorem this replaced (log Y)² ≤ 16√Y and cut the constant by 5×. Also useful: (log M)² ≤ M, from log y ≤ y/e at y = √M (Real.log_le_sub_one_of_pos at y/e) and e ≥ 2.