FKS2.Table4Ext.cell_eps_le_admissible_gen

theorem cell_eps_le_admissible_gen    (P : CellParams) (A B C R : ℝ)    (hk : (P.k : ℝ) = 2 * B) (hB : 0 ≤ B) (hRpos : 0 < R) (hAnn : 0 ≤ A)    (hAq : ((P.Aq : ℚ) : ℝ) = A)    (hCge : C / Real.sqrt R ≤ ((P.c64 * 64 : ℚ) : ℝ))    (hrB : R ^ B ≤ ((P.rB : ℚ) : ℝ))    (c : Cell) (hc : checkCellGen P c = true) :    ∀ x ∈ Set.Icc (exp (c.b : ℝ)) (exp (c.b' : ℝ)),      (c.eps : ℝ) ≤ admissible_bound A B C R x := by  unfold checkCellGen 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⟩, hrBpos⟩, hslo⟩, hshi⟩, hcheck⟩ := hc    have hslab := verify_expr_le_on_interval_dyadic (expSplitC P.c64)      (powRhs (P.Aq / (c.eps * P.rB)) P.k) ⟨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    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    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 and rewrite evals    have hineq := hslab s ⟨hs_lo, hs_hi⟩    rw [eval_expSplitC, eval_powRhs] at hineq    -- collapse (exp (c64·s))^64 = exp ((c64·64)·s)    have hexp64 : exp ((P.c64 : ℝ) * s) ^ (64 : ℕ) = exp (((P.c64 * 64 : ℚ) : ℝ) * s) := by      rw [← Real.exp_nat_mul]; congr 1; push_cast; ring    rw [hexp64] at hineq    have heps_pos : (0 : ℝ) < (c.eps : ℝ) := by exact_mod_cast heps    have hrBpos' : (0 : ℝ) < (P.rB : ℝ) := by exact_mod_cast hrBpos    have hs_nonneg : (0 : ℝ) ≤ s := Real.sqrt_nonneg _    -- LHS: bound true exp by the checked (over-estimated) exp    have hCs : C / Real.sqrt R * s ≤ ((P.c64 * 64 : ℚ) : ℝ) * s :=      mul_le_mul_of_nonneg_right hCge hs_nonneg    have hLHS : exp (C / Real.sqrt R * s) ≤ exp (((P.c64 * 64 : ℚ) : ℝ) * s) :=      Real.exp_le_exp.mpr hCs    -- RHS coefficient: q = Aq/(eps·rB) ≤ A/(eps·R^B)    have hRBpos : (0 : ℝ) < R ^ B := Real.rpow_pos_of_pos hRpos _    have hqle : ((P.Aq / (c.eps * P.rB) : ℚ) : ℝ) ≤ A / ((c.eps : ℝ) * R ^ B) := by      rw [show ((P.Aq / (c.eps * P.rB) : ℚ) : ℝ) = A / ((c.eps : ℝ) * (P.rB : ℝ)) by        push_cast [hAq]; ring]      exact div_le_div_of_nonneg_left hAnn (mul_pos heps_pos hRBpos)        (mul_le_mul_of_nonneg_left hrB heps_pos.le)    -- chain: exp(C/√R·s) ≤ exp(ĉ·s) ≤ q·s^k ≤ (A/(eps·R^B))·s^k    have hsk_nonneg : (0 : ℝ) ≤ s ^ P.k := pow_nonneg hs_nonneg _    have hchain : exp (C / Real.sqrt R * s) ≤ (A / ((c.eps : ℝ) * R ^ B)) * s ^ P.k := by      calc exp (C / Real.sqrt R * s)          ≤ exp (((P.c64 * 64 : ℚ) : ℝ) * s) := hLHS        _ ≤ ((P.Aq / (c.eps * P.rB) : ℚ) : ℝ) * s ^ P.k := hineq        _ ≤ (A / ((c.eps : ℝ) * R ^ B)) * s ^ P.k :=            mul_le_mul_of_nonneg_right hqle hsk_nonneg    -- multiply by eps, divide by exp, identify the curve    have hexp_pos : (0 : ℝ) < exp (C / Real.sqrt R * s) := exp_pos _    have h2 : (c.eps : ℝ) * exp (C / Real.sqrt R * s) ≤ (A / R ^ B) * s ^ P.k := by      have := mul_le_mul_of_nonneg_left hchain heps_pos.le      calc (c.eps : ℝ) * exp (C / Real.sqrt R * s)          ≤ (c.eps : ℝ) * ((A / ((c.eps : ℝ) * R ^ B)) * s ^ P.k) := this        _ = (A / R ^ B) * s ^ P.k := by field_simp    have key : (c.eps : ℝ) ≤ (A / R ^ B) * s ^ P.k * exp (-(C / Real.sqrt R * 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    -- curve identity: admissible_bound A B C R x = (A/R^B)·s^k·exp(−(C/√R)·s)    have hs_rpow : s = Real.log x ^ ((1 : ℝ) / 2) := by rw [hs_def, Real.sqrt_eq_rpow]    have hsqrtR : Real.sqrt R = R ^ ((1 : ℝ) / 2) := Real.sqrt_eq_rpow R    have hRnn : (0 : ℝ) ≤ R := hRpos.le    have hpowk : Real.log x ^ B = s ^ P.k := by      rw [hs_rpow, ← Real.rpow_natCast (Real.log x ^ ((1 : ℝ) / 2)) P.k,        ← Real.rpow_mul hlog_nonneg]      rw [show (1 : ℝ) / 2 * (P.k : ℝ) = B by rw [hk]; ring]    have hcurve : admissible_bound A B C R x        = (A / R ^ B) * s ^ P.k * exp (-(C / Real.sqrt R * s)) := by      unfold admissible_bound      have e1 : (Real.log x / R) ^ B = s ^ P.k / R ^ B := by        rw [Real.div_rpow hlog_nonneg hRnn, hpowk]      have e2 : (Real.log x / R) ^ ((1 : ℝ) / 2) = s / Real.sqrt R := by        rw [Real.div_rpow hlog_nonneg hRnn, ← hs_rpow, hsqrtR]      rw [e1, e2]      rw [show C / Real.sqrt R * s = C * (s / Real.sqrt R) by ring]      ring    rw [hcurve]    exact key