FKS2.Table4Ext.cell_eps_le_admissible

theorem cell_eps_le_admissible (c : Cell) (hc : checkCell c = true) :    ∀ x ∈ Set.Icc (exp (c.b : ℝ)) (exp (c.b' : ℝ)),      (c.eps : ℝ) ≤ admissible_bound (Aq : ℝ) (3 / 2) (Cq : ℝ) 1 x := by  -- unpack the boolean  unfold checkCell at hc  split at hc  case isFalse => simp at hc  case isTrue hle =>    simp only [Bool.and_eq_true, decide_eq_true_eq] at hc    obtain ⟨⟨⟨⟨heps, hslo0⟩, hslo⟩, hshi⟩, hcheck⟩ := hc    -- the slab inequality, semantically    have hslab := verify_expr_le_on_interval_dyadic expSplit      (cubeRhs (Aq / c.eps)) ⟨c.slo, c.shi, hle⟩ (-50) 8      (by norm_num) hcheck    intro x hx    obtain ⟨hx_lo, hx_hi⟩ := hx    have hxpos : (0 : ℝ) < x := lt_of_lt_of_le (exp_pos _) hx_lo    -- log x ∈ [b, b']    have hb_le : (c.b : ℝ) ≤ Real.log x :=      (Real.le_log_iff_exp_le hxpos).mpr hx_lo    have hb'_ge : Real.log x ≤ (c.b' : ℝ) :=      (Real.log_le_iff_le_exp hxpos).mpr hx_hi    have hlog_nonneg : (0 : ℝ) ≤ Real.log x :=      le_trans (Nat.cast_nonneg _) hb_le    -- s = √(log x) ∈ [slo, shi]    set s : ℝ := Real.sqrt (Real.log x) with hs_def    have h0lo : (0 : ℝ) ≤ (c.slo : ℝ) := by exact_mod_cast hslo0    have h0hi : (0 : ℝ) ≤ (c.shi : ℝ) := by      have : ((c.slo : ℚ) : ℝ) ≤ ((c.shi : ℚ) : ℝ) := by exact_mod_cast hle      linarith    have hs_lo : (c.slo : ℝ) ≤ s := by      have h1 : ((c.slo : ℝ)) ^ 2 ≤ Real.log x := by        have hq : ((c.slo : ℝ)) * ((c.slo : ℝ)) ≤ ((c.b : ℕ) : ℝ) := by          exact_mod_cast hslo        calc ((c.slo : ℝ)) ^ 2 = ((c.slo : ℝ)) * ((c.slo : ℝ)) := pow_two _          _ ≤ ((c.b : ℕ) : ℝ) := hq          _ ≤ Real.log x := hb_le      calc (c.slo : ℝ) = Real.sqrt (((c.slo : ℝ)) ^ 2) :=            (Real.sqrt_sq h0lo).symm        _ ≤ s := Real.sqrt_le_sqrt h1    have hs_hi : s ≤ (c.shi : ℝ) := by      have h1 : Real.log x ≤ ((c.shi : ℝ)) ^ 2 := by        have hq : ((c.b' : ℕ) : ℝ) ≤ ((c.shi : ℝ)) * ((c.shi : ℝ)) := by          exact_mod_cast hshi        calc Real.log x ≤ ((c.b' : ℕ) : ℝ) := hb'_ge          _ ≤ ((c.shi : ℝ)) * ((c.shi : ℝ)) := hq          _ = ((c.shi : ℝ)) ^ 2 := (pow_two _).symm      calc s ≤ Real.sqrt (((c.shi : ℝ)) ^ 2) := Real.sqrt_le_sqrt h1        _ = (c.shi : ℝ) := Real.sqrt_sq h0hi    -- instantiate the slab inequality at s    have hineq := hslab s ⟨hs_lo, hs_hi⟩    rw [eval_expSplit, eval_cubeRhs] at hineq    -- (exp (C/64·s))^64 = exp (C·s)    have hCC : ((Cq64 : ℚ) : ℝ) * 64 = ((Cq : ℚ) : ℝ) := by      simp only [Cq64, Cq]      push_cast      norm_num    have hexp64 : exp ((Cq64 : ℝ) * s) ^ (64 : ℕ) = exp ((Cq : ℝ) * s) := by      rw [← Real.exp_nat_mul]      congr 1      rw [← hCC]      ring    rw [hexp64] at hineq    -- divide back: exp(C·s) ≤ (A/ε)·s³  →  ε·exp(C·s) ≤ A·s³    have heps_pos : (0 : ℝ) < (c.eps : ℝ) := by exact_mod_cast heps    have hexp_pos : (0 : ℝ) < exp ((Cq : ℝ) * s) := exp_pos _    have hdiv : ((Aq / c.eps : ℚ) : ℝ) = (Aq : ℝ) / (c.eps : ℝ) := by      push_cast      ring    rw [hdiv] at hineq    have h2 : (c.eps : ℝ) * exp ((Cq : ℝ) * s) ≤ (Aq : ℝ) * s ^ (3 : ℕ) := by      have h3 := mul_le_mul_of_nonneg_left hineq (le_of_lt heps_pos)      calc (c.eps : ℝ) * exp ((Cq : ℝ) * s)          ≤ (c.eps : ℝ) * ((Aq : ℝ) / (c.eps : ℝ) * s ^ (3 : ℕ)) := h3        _ = (Aq : ℝ) * s ^ (3 : ℕ) := by field_simp    -- ε ≤ A·s³·exp(−C·s)    have key : (c.eps : ℝ) ≤ (Aq : ℝ) * s ^ (3 : ℕ) * exp (-((Cq : ℝ) * s)) := by      have h4 := mul_le_mul_of_nonneg_right h2        (le_of_lt (inv_pos.mpr hexp_pos))      rw [mul_assoc, mul_inv_cancel₀ (ne_of_gt hexp_pos), mul_one] at h4      rw [Real.exp_neg]      exact h4    -- identify the curve: admissible_bound A (3/2) C 1 x = A·s³·exp(−C·s)    have hs_rpow : s = Real.log x ^ ((1 : ℝ) / 2) := by      rw [hs_def, Real.sqrt_eq_rpow]    have h32 : Real.log x ^ ((3 : ℝ) / 2) = s ^ (3 : ℕ) := by      rw [hs_rpow, ← Real.rpow_natCast (Real.log x ^ ((1 : ℝ) / 2)) 3,        ← Real.rpow_mul hlog_nonneg]      norm_num    have hcurve : admissible_bound (Aq : ℝ) (3 / 2) (Cq : ℝ) 1 x        = (Aq : ℝ) * s ^ (3 : ℕ) * exp (-((Cq : ℝ) * s)) := by      unfold admissible_bound      rw [div_one, show ((3 : ℝ) / 2) = (3 : ℝ) / 2 from rfl, h32,        ← hs_rpow, neg_mul]    rw [hcurve]    exact key