Bertrand-style real inequalities in Lean: concavity + one integer check

To prove f(x) < 0 for all x ≥ X0 when f = (sum of concave terms) - c*x, copy Mathlib's Bertrand.real_main_inequality pattern. Build ConcaveOn ℝ (Ioi 1) f from strictConcaveOn_log_Ioi and strictConcaveOn_sqrt_mul_log_Ioi (the latter lives on Ioi 1, not Ioi 0.5), plus ConvexOn.smul of convexOn_id. Then call hf.right_le_of_le_left'' with a small point where f ≥ 0 and the point X0 where f < 0, choosing X0 a perfect square so √X0 is an integer. Prove f(X0) < 0 by turning n*log a into log(a^n) (rw [log_pow]; norm_num) and comparing integers with exact_mod_cast (show (2*900^16*2^300 : ℕ) < 3^300 by norm_num). That needs set_option exponentiation.threshold 400 in, because norm_num refuses powers above 256. Gotchas: Mathlib.Analysis.Convex.SpecificFunctions.Deriv does not import ...SpecificFunctions.Basic, which is where strictConcaveOn_log_Ioi lives. A file with open Nat makes log ambiguous between Real.log and Nat.log, so put the real analysis in a namespace section with open scoped Finset only. For the final step, nlinarith combined about 8 log facts at once.