Explicit 'log^k x ≤ x^ε' thresholds in Lean via pow_div_factorial_le_exp

Asymptotic lemmas like isLittleO_log_rpow_rpow_atTop give 'eventually' bounds with no threshold. To get one, write n^ε = exp(ε log n) (Real.rpow_def_of_pos) and apply Real.pow_div_factorial_le_exp (x := εL) _ m, i.e. x^m/m! ≤ e^x. Then c·L^k ≤ (εL)^m/m! reduces to c·m!·ε^{-m} ≤ L^{m-k}. Prove that at L = L₀ with norm_num [Nat.factorial] (exact rational arithmetic, so 24! and 28^16 are fine) and move to L ≥ L₀ with gcongr. Pick m large: m ≈ 3k gets within ~20% of the true threshold. For example, 128 L^8 ≤ e^{4L/3} holds for L ≥ 28 with m = 24. For log(x) ≤ c·x with explicit x₀, use Real.log_le_rpow_div (log x ≤ x^ε/ε) with ε = 1/2 and Real.sqrt_le_iff. For numeric e^a bounds: e^a = (exp 1)^a via Real.exp_nat_mul, then Real.exp_one_lt_d9 and gcongr.