Exact logarithm of the selected-count lower bound

import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Tactic.Ring
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Theorems.Thm_mme_recursive_profiled_CW_exact_step
import Definitions.Def_mme_recursive_profiled_CW_data
import Mathlib.Algebra.Order.Field.Basic
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Linarith
open MME MME.ProfiledCW
set_option autoImplicit false
universe u

theorem mme_hash_selected_bound_log (A Q : ℝ) (hA : 0 < A) (hQ : 0 < Q) :
    Real.log (A * Real.exp (-4 * Real.sqrt (Real.log Q)) / (32 * Q)) =
      Real.log A - Real.log Q - 4 * Real.sqrt (Real.log Q) - Real.log 32 := by sorry