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

row_hartree_over_rest_upper

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)

  79theorem row_hartree_over_rest_upper :
  80    row_hartree_over_rest < (5.33e-5 : ℝ) := by

proof body

Tactic-mode proof.

  81  rw [row_hartree_over_rest_eq]
  82  have hpos : 0 < alphaInv ^ 2 := sq_pos_of_ne_zero (ne_of_gt alphaInv_pos)
  83  rw [div_lt_iff₀ hpos]
  84  have hsq : (137.030 : ℝ) ^ 2 < alphaInv ^ 2 := by
  85    nlinarith [alphaInv_gt, alphaInv_lt]
  86  have hnum : 1 < (5.33e-5 : ℝ) * (137.030 : ℝ) ^ 2 := by norm_num
  87  nlinarith
  88

used by (1)

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

depends on (7)

Lean names referenced from this declaration's body.