FKS2.Table4Ext.checkXpowCell_sound

theorem checkXpowCell_sound (n : ℕ) (hn : 0 < n) (c : Cell)    (hc : checkXpowCell n c = true) :    (c.eps : ℝ) ≤ Real.exp (-(c.b' : ℝ) / n) := by  have hnpos : (0 : ℝ) < (n : ℝ) := by exact_mod_cast hn  unfold checkXpowCell 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    -- semantic slab inequality: exp(s²/n) ≤ 1/eps on [slo, shi]    have hslab := verify_expr_le_on_interval_dyadic (expSplitXpow n)      (Expr.const (1 / c.eps)) ⟨c.slo, c.shi, hle⟩ (-50) 8      (expSplitXpow_supported _ _) (by norm_num) hcheck    -- instantiate at s = shi (the right endpoint, where exp(s²/n) is largest)    have hshi_mem : (c.shi : ℝ) ∈ Set.Icc ((c.slo : ℝ)) ((c.shi : ℝ)) :=      ⟨by exact_mod_cast hle, le_refl _⟩    have hineq := hslab (c.shi : ℝ) hshi_mem    rw [eval_expSplitXpow, Expr.eval_const] at hineq    -- (exp ((1/64n)·shi²))^64 = exp(shi²/n)    have hn' : (n : ℝ) ≠ 0 := ne_of_gt hnpos    have harg : ((64 : ℕ) : ℝ) * ((xpowCoef n : ℝ) * ((c.shi : ℝ) * (c.shi : ℝ)))        = ((c.shi : ℝ) * (c.shi : ℝ)) / n := by      simp only [xpowCoef]; push_cast; field_simp    have hexp64 :        exp ((xpowCoef n : ℝ) * ((c.shi : ℝ) * (c.shi : ℝ))) ^ (64 : ℕ)          = exp (((c.shi : ℝ) * (c.shi : ℝ)) / n) := by      rw [← Real.exp_nat_mul, harg]    rw [hexp64] at hineq    -- 1/eps on the RHS as a real reciprocal    have hrhs : ((1 / c.eps : ℚ) : ℝ) = 1 / (c.eps : ℝ) := by push_cast; ring    rw [hrhs] at hineq    -- positivity facts and the b' ≤ shi² side condition    have hepsR : (0 : ℝ) < (c.eps : ℝ) := by exact_mod_cast heps    have hbshi : (c.b' : ℝ) ≤ (c.shi : ℝ) * (c.shi : ℝ) := by exact_mod_cast hshi    have hexppos : (0 : ℝ) < exp ((c.b' : ℝ) / n) := Real.exp_pos _    -- exp(b'/n) ≤ exp(shi²/n) ≤ 1/eps    have hmono2 : exp ((c.b' : ℝ) / n) ≤ exp (((c.shi : ℝ) * (c.shi : ℝ)) / n) := by      apply Real.exp_le_exp.mpr      gcongr    have hchain : exp ((c.b' : ℝ) / n) ≤ 1 / (c.eps : ℝ) := le_trans hmono2 hineq    -- eps ≤ exp(-b'/n)    rw [neg_div, Real.exp_neg, ← one_div, le_div_iff₀ hexppos]    have hmul : exp ((c.b' : ℝ) / n) * (c.eps : ℝ) ≤ 1 :=      (le_div_iff₀ hepsR).mp hchain    linarith [hmul]