mu_pred_upper

formal source

  81  have step2 : (1898 : ℝ) * (0.5102 : ℝ) < (969 : ℝ) := by norm_num
  82  linarith
  83
  84theorem mu_pred_upper : mu_pred < (1904 : ℝ) := by
  85  unfold mu_pred
  86  have he_pos : 0 < electron_pred := electron_pred_pos
  87  rw [div_lt_iff₀ he_pos]
  88  -- want: proton_binding_pred < 1904 * electron_pred
  89  have he_lo : (0.5098 : ℝ) < electron_pred := electron_mass_bounds.1
  90  have hp_hi : proton_binding_pred < (970.4 : ℝ) := proton_mass_bounds.2
  91  -- proton_binding_pred < 970.4 < 1904 * 0.5098 = 970.6592 < 1904 * electron_pred
  92  have step1 : (970.4 : ℝ) < (1904 : ℝ) * (0.5098 : ℝ) := by norm_num
  93  have step2 : (1904 : ℝ) * (0.5098 : ℝ) < (1904 : ℝ) * electron_pred := by
  94    have h1904 : (0 : ℝ) < 1904 := by norm_num
  95    exact mul_lt_mul_of_pos_left he_lo h1904
  96  linarith
  97
  98theorem mu_pred_bracket : (1898 : ℝ) < mu_pred ∧ mu_pred < (1904 : ℝ) :=
  99  ⟨mu_pred_lower, mu_pred_upper⟩
 100
 101/-! ## CODATA comparison
 102
 103The predicted ratio is approximately 1901, while CODATA reads 1836.15.
 104The relative residual `(μ_pred - μ_codata) / μ_codata` is bounded
 105above by 4 percent.
 106-/
 107
 108theorem mu_relative_error : |mu_pred - mu_codata| / mu_codata < 0.04 := by
 109  have hb := mu_pred_bracket
 110  have hcodata_pos : (0 : ℝ) < mu_codata := by unfold mu_codata; norm_num
 111  rw [div_lt_iff₀ hcodata_pos, abs_lt]
 112  unfold mu_codata
 113  constructor <;> nlinarith [hb.1, hb.2]
 114