Real.sq_le_exp_const_mul_rpow

theorem sq_le_exp_const_mul_rpow {b r : ℝ} (hb : 0 < b) (hr : 1 ≤ r) :    r ^ 2 ≤ exp ((4 / b) * r ^ b) := by  have hrpos : 0 < r := zero_lt_one.trans_le hr  have hcoeff2 : 0 ≤ (2 / b : ℝ) := by positivity  have hcoeff4 : 0 ≤ (4 / b : ℝ) := by positivity  have hlog_le : log r ≤ (2 / b) * r ^ (b / 2) := by    have hle_exp : (b / 2) * log r ≤ exp ((b / 2) * log r) := le_exp_self _    calc      log r = (2 / b) * ((b / 2) * log r) := by        field_simp [ne_of_gt hb]      _ ≤ (2 / b) * exp ((b / 2) * log r) :=        mul_le_mul_of_nonneg_left hle_exp hcoeff2      _ = (2 / b) * r ^ (b / 2) := by        simp [rpow_def_of_pos hrpos, mul_comm]  have hpow_le : r ^ (b / 2) ≤ r ^ b :=    rpow_le_rpow_of_exponent_le hr (by linarith)  have hlog_sq : log (r ^ 2) ≤ (4 / b) * r ^ b := by    calc      log (r ^ 2) = 2 * log r := by        simp [log_pow]      _ ≤ 2 * ((2 / b) * r ^ (b / 2)) :=        mul_le_mul_of_nonneg_left hlog_le (by norm_num)      _ = (4 / b) * r ^ (b / 2) := by ring      _ ≤ (4 / b) * r ^ b :=        mul_le_mul_of_nonneg_left hpow_le hcoeff4  have hsq_pos : 0 < r ^ 2 := by positivity  rw [← exp_log hsq_pos]  exact exp_le_exp.2 hlog_sq