alphaInv_pos

formal source

  52/-- P1-C03 dimensionless Bohr/reduced-Compton radius ratio. -/
  53noncomputable def row_bohr_over_reduced_compton : ℝ := alphaInv
  54
  55private theorem alphaInv_pos : 0 < alphaInv := by
  56  linarith [alphaInv_gt]
  57
  58theorem row_hartree_over_rest_eq : row_hartree_over_rest = 1 / alphaInv ^ 2 := by
  59  unfold row_hartree_over_rest alpha
  60  field_simp [ne_of_gt alphaInv_pos]
  61
  62theorem row_rydberg_over_rest_eq :
  63    row_rydberg_over_rest = 1 / (2 * alphaInv ^ 2) := by
  64  unfold row_rydberg_over_rest alpha
  65  field_simp [ne_of_gt alphaInv_pos]
  66
  67/-! ## Certified interval bounds -/
  68
  69theorem row_hartree_over_rest_lower :
  70    (5.32e-5 : ℝ) < row_hartree_over_rest := by
  71  rw [row_hartree_over_rest_eq]
  72  have hpos : 0 < alphaInv ^ 2 := sq_pos_of_ne_zero (ne_of_gt alphaInv_pos)
  73  rw [lt_div_iff₀ hpos]
  74  have hsq : alphaInv ^ 2 < (137.039 : ℝ) ^ 2 := by
  75    nlinarith [alphaInv_lt, alphaInv_gt]
  76  have hnum : (5.32e-5 : ℝ) * (137.039 : ℝ) ^ 2 < 1 := by norm_num
  77  nlinarith
  78
  79theorem row_hartree_over_rest_upper :
  80    row_hartree_over_rest < (5.33e-5 : ℝ) := by
  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]