f_gap_lt

formal source

 213    _ < w8_from_eight_tick * log IndisputableMonolith.Constants.phi := by
 214      exact mul_lt_mul_of_pos_left h_log_lo h_w8_pos
 215
 216theorem f_gap_lt : f_gap < (1.203 : ℝ) := by
 217  simp only [f_gap]
 218  have h_w8_hi := W8Bounds.w8_computed_lt
 219  have h_log_hi := log_phi_lt_0483
 220  have h_w8_pos : 0 < w8_from_eight_tick := IndisputableMonolith.Constants.w8_pos
 221  have h0483 : 0 < (0.483 : ℝ) := by norm_num
 222  -- f_gap = w8 * log(phi) < 2.490572090 * 0.483 = 1.202946...
 223  calc w8_from_eight_tick * log IndisputableMonolith.Constants.phi
 224      < w8_from_eight_tick * (0.483 : ℝ) := by
 225        exact mul_lt_mul_of_pos_left h_log_hi h_w8_pos
 226    _ < (2.490572090 : ℝ) * (0.483 : ℝ) := by
 227        exact mul_lt_mul_of_pos_right h_w8_hi h0483
 228    _ < (1.203 : ℝ) := by norm_num
 229
 230/-! ## Local exp bounds used by the exponential α formula -/
 231
 232private def exp_taylor_10_at_neg_00871 : ℚ :=
 233  let x : ℚ := -(871 : ℚ) / 100000
 234  1 + x + x^2/2 + x^3/6 + x^4/24 + x^5/120 + x^6/720 + x^7/5040 + x^8/40320 + x^9/362880
 235
 236private def exp_error_10_at_neg_00871 : ℚ :=
 237  let x : ℚ := (871 : ℚ) / 100000
 238  x^10 * 11 / (Nat.factorial 10 * 10)
 239
 240private lemma exp_neg_00871_taylor_floor :
 241    (991327 / 1000000 : ℚ) < exp_taylor_10_at_neg_00871 - exp_error_10_at_neg_00871 := by
 242  native_decide
 243
 244private lemma exp_neg_00871_gt : ((991327 / 1000000 : ℚ) : ℝ) < Real.exp (-0.00871 : ℝ) := by
 245  have hx_abs : |(-0.00871 : ℝ)| ≤ 1 := by norm_num
 246  have h_bound := Real.exp_bound hx_abs (n := 10) (by norm_num : 0 < 10)