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

alphaInv_lt

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)

 335theorem alphaInv_lt : alphaInv < (137.039 : ℝ) := by

proof body

Tactic-mode proof.

 336  simp only [alphaInv]
 337  have hseed_pos : (0 : ℝ) < alpha_seed := lt_trans (by norm_num) alpha_seed_gt
 338  have hy_lo : (0.00866 : ℝ) < f_gap / alpha_seed := by
 339    have hmul : (0.00866 : ℝ) * alpha_seed < f_gap := by
 340      have h1 : (0.00866 : ℝ) * alpha_seed < (0.00866 : ℝ) * (138.230092 : ℝ) := by
 341        exact mul_lt_mul_of_pos_left alpha_seed_lt (by norm_num)
 342      have h2 : (0.00866 : ℝ) * (138.230092 : ℝ) < (1.1979 : ℝ) := by norm_num
 343      exact lt_trans h1 (lt_trans h2 f_gap_gt_strong)
 344    exact (lt_div_iff₀ hseed_pos).2 (by simpa [mul_comm, mul_left_comm, mul_assoc] using hmul)
 345  have hexp_hi : Real.exp (-(f_gap / alpha_seed)) < ((495689 / 500000 : ℚ) : ℝ) := by
 346    have hmono : Real.exp (-(f_gap / alpha_seed)) < Real.exp (-(0.00866 : ℝ)) := by
 347      exact Real.exp_lt_exp.mpr (by linarith [hy_lo])
 348    exact lt_trans hmono exp_neg_00866_lt
 349  have hmul :
 350      alpha_seed * Real.exp (-(f_gap / alpha_seed)) <
 351        alpha_seed * (((495689 / 500000 : ℚ) : ℝ)) := by
 352    exact mul_lt_mul_of_pos_left hexp_hi hseed_pos
 353  have hseed_hi :
 354      alpha_seed * (((495689 / 500000 : ℚ) : ℝ)) <
 355        (138.230092 : ℝ) * (((495689 / 500000 : ℚ) : ℝ)) := by
 356    exact mul_lt_mul_of_pos_right alpha_seed_lt (by norm_num)
 357  calc
 358    alpha_seed * Real.exp (-(f_gap / alpha_seed))
 359        < alpha_seed * (((495689 / 500000 : ℚ) : ℝ) : ℝ) := hmul
 360    _ < (138.230092 : ℝ) * (((495689 / 500000 : ℚ) : ℝ) : ℝ) := hseed_hi
 361    _ < (137.039 : ℝ) := by norm_num
 362
 363/-- Upper bound alias retained for backwards compatibility after the canonical
 364exponential α update. -/

used by (10)

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

depends on (16)

Lean names referenced from this declaration's body.