Ramanujan.Calculations.a_exp_upper_of

theorem a_exp_upper_of    {a : ℝ → ℝ}    (ha_eq_admissible_ge_3000 :      ∀ {z : ℝ}, z ≥ exp 3000 →        a z = admissible_bound (379.7 * 5.573412 ^ 5) 6.52 1.89 5.573412 z)    {L C : ℝ}    (hL : 3000 ≤ L)    (hpow5 : (5.573412 : ℝ) ^ (5 : ℕ) * ((L / 5.573412) ^ (5 : ℕ)) = L ^ (5 : ℕ))    (haux : ∀ y ∈ Set.Icc L L, styleVal y ≤ C) :    a (exp L) ≤ C := by  have hLpos : 0 < L := by linarith  rw [ha_eq_admissible_ge_3000 (z := exp L) (exp_le_exp.mpr hL)]  unfold admissible_bound  rw [log_exp, rpow_652_split (by positivity : 0 < L / 5.573412),    sqrt_ratio_5573412 (y := L) hLpos.le]  let A : ℝ := (L / 5.573412) ^ (1.52 : ℝ)  let E : ℝ := exp (-(1.89 : ℝ) * (sqrt L / sqrt (5.573412 : ℝ)))  have hrewrite :      (379.7 * 5.573412 ^ 5) * ((L / 5.573412) ^ 5 * A) * E      = L ^ 5 * ((379.7 : ℝ) * A * E) := by    calc      (379.7 * 5.573412 ^ 5) * ((L / 5.573412) ^ 5 * A) * E          = (5.573412 ^ 5 * (L / 5.573412) ^ 5) * ((379.7 : ℝ) * A * E) := by              ring      _ = L ^ 5 * ((379.7 : ℝ) * A * E) := by rw [hpow5]  rw [hrewrite, style_eq L hLpos]  exact haux L ⟨le_rfl, le_rfl⟩