FKS2.corollary_14_small_adm

lemma corollary_14_small_adm :    ∀ {x : ℝ}, 2 ≤ x → x ≤ Real.exp 30 →    (1:ℝ) ≤ admissible_bound 121.0961 (3/2) 2 5.5666305 x := by  intro x hx hx30  let u : ℝ := Real.log x / 5.5666305  have hu_pos : 0 < u := by    have hlogx : 0 < Real.log x := Real.log_pos (lt_of_lt_of_le (by norm_num) hx)    exact div_pos hlogx (by norm_num)  have hu_ge : (31/250:ℝ) ≤ u := by    have hlog2x : Real.log 2 ≤ Real.log x := Real.log_le_log (by norm_num) hx    have h : (31/250:ℝ) * 5.5666305 ≤ Real.log x := by      nlinarith [hlog2x, LogTables.log_2_gt]    exact (le_div_iff₀ (by norm_num : (0:ℝ) < 5.5666305)).2 h  have hu_le : u ≤ 30 / 5.5666305 := by    have hlog : Real.log x ≤ 30 := by      have := Real.log_le_log (by positivity : 0 < x) hx30      simpa [Real.log_exp] using this    have hdiv : Real.log x / 5.5666305 ≤ 30 / 5.5666305 :=      div_le_div_of_nonneg_right hlog (by norm_num)    simpa [u] using hdiv  change (1:ℝ) ≤ 121.0961 * u ^ (3 / 2 : ℝ) * Real.exp (-2 * u ^ (1 / 2 : ℝ))  have hu_pow : u ^ (3 / 2 : ℝ) = u * Real.sqrt u := by    rw [show (3 / 2 : ℝ) = (1:ℝ) + (1 / 2 : ℝ) by norm_num]    rw [Real.rpow_add hu_pos]    simp [Real.sqrt_eq_rpow]  have hu_sqrtpow : u ^ (1 / 2 : ℝ) = Real.sqrt u := by    simp [Real.sqrt_eq_rpow]  rw [hu_pow, hu_sqrtpow]  by_cases hu64 : u ≤ (16/25:ℝ)  · exact corollary_14_small_adm_case1 u hu_pos hu_ge hu64  · have hu64' : (16/25:ℝ) < u := lt_of_not_ge hu64    by_cases hu94 : u ≤ (9/4:ℝ)    · exact corollary_14_small_adm_case2 u hu_pos hu64' hu94    · have hu94' : (9/4:ℝ) < u := lt_of_not_ge hu94      exact corollary_14_small_adm_case3 u hu_pos hu94' hu_le