pith. machine review for the scientific record. sign in
theorem proved tactic proof

alphaInv_gt

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 307theorem alphaInv_gt : (137.030 : ℝ) < alphaInv := by

proof body

Tactic-mode proof.

 308  simp only [alphaInv]
 309  have hseed_pos : (0 : ℝ) < alpha_seed := lt_trans (by norm_num) alpha_seed_gt
 310  have hy_hi : f_gap / alpha_seed < (0.00871 : ℝ) := by
 311    have hmul : f_gap < (0.00871 : ℝ) * alpha_seed := by
 312      have h1 : f_gap < (1.203 : ℝ) := f_gap_lt
 313      have h2 : (1.203 : ℝ) < (0.00871 : ℝ) * (138.230048 : ℝ) := by norm_num
 314      have h3 : (0.00871 : ℝ) * (138.230048 : ℝ) < (0.00871 : ℝ) * alpha_seed := by
 315        exact mul_lt_mul_of_pos_left alpha_seed_gt (by norm_num)
 316      exact lt_trans h1 (lt_trans h2 h3)
 317    exact (div_lt_iff₀ hseed_pos).2 (by simpa [mul_comm, mul_left_comm, mul_assoc] using hmul)
 318  have hexp_lo : ((991327 / 1000000 : ℚ) : ℝ) < Real.exp (-(f_gap / alpha_seed)) := by
 319    have hmono : Real.exp (-(0.00871 : ℝ)) < Real.exp (-(f_gap / alpha_seed)) := by
 320      exact Real.exp_lt_exp.mpr (by linarith [hy_hi])
 321    exact lt_trans exp_neg_00871_gt hmono
 322  have hseed_mul :
 323      (138.230048 : ℝ) * (((991327 / 1000000 : ℚ) : ℝ)) <
 324        alpha_seed * (((991327 / 1000000 : ℚ) : ℝ)) := by
 325    exact mul_lt_mul_of_pos_right alpha_seed_gt (by norm_num)
 326  have hmul :
 327      alpha_seed * (((991327 / 1000000 : ℚ) : ℝ)) <
 328        alpha_seed * Real.exp (-(f_gap / alpha_seed)) := by
 329    exact mul_lt_mul_of_pos_left hexp_lo hseed_pos
 330  calc
 331    (137.030 : ℝ) < (138.230048 : ℝ) * (((991327 / 1000000 : ℚ) : ℝ) : ℝ) := by norm_num
 332    _ < alpha_seed * (((991327 / 1000000 : ℚ) : ℝ) : ℝ) := hseed_mul
 333    _ < alpha_seed * Real.exp (-(f_gap / alpha_seed)) := hmul
 334

used by (12)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (11)

Lean names referenced from this declaration's body.