have hf' : ∀ x, 0 < x → 0 < x * (2 * x) ^ sqrt (2 * x) / 4 ^ (x / 3) := fun x h =>
  div_pos (mul_pos h (rpow_pos_of_pos (mul_pos two_pos h) _)) (rpow_pos_of_pos four_pos _)
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
⊢ x * (2 * x) ^ (2 * x).sqrt * 4 ^ (2 * x / 3) ≤ 4 ^ x
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
⊢ x * (2 * x) ^ (2 * x).sqrt * 4 ^ (2 * x / 3) ≤ 4 ^ x