have hf : ∀ x, 0 < x → f x = log (x * (2 * x) ^ sqrt (2 * x) / 4 ^ (x / 3)) := by
  intro x h5
  have h6 := mul_pos (zero_lt_two' ℝ) h5
  have h7 := rpow_pos_of_pos h6 (sqrt (2 * x))
  rw [log_div (mul_pos h5 h7).ne' (rpow_pos_of_pos four_pos _).ne', log_mul h5.ne' h7.ne',
    log_rpow h6, log_rpow zero_lt_four, ← mul_div_right_comm, ← mul_div, mul_comm 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
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)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
⊢ x * (2 * x) ^ (2 * x).sqrt * 4 ^ (2 * x / 3) ≤ 4 ^ x