electron_relative_error

formal source

 107    calc Constants.phi ^ 59 < (2139810000000 : ℝ) := phi59_lt
 108      _ < (0.5102 : ℝ) * 4194304000000 := by norm_num
 109
 110theorem electron_relative_error :
 111    |rs_mass_MeV .Lepton 2 - m_e_exp| / m_e_exp < 0.003 := by
 112  rw [electron_pred_eq]
 113  have hb := electron_mass_bounds
 114  have hexp_pos : (0 : ℝ) < m_e_exp := by unfold m_e_exp; norm_num
 115  rw [div_lt_iff₀ hexp_pos, abs_lt]
 116  unfold m_e_exp
 117  constructor <;> nlinarith [hb.1, hb.2]
 118
 119/-! ## Muon Mass Verification -/
 120
 121theorem muon_mass_bounds :
 122    (101.49 : ℝ) < muon_pred ∧ muon_pred < (101.57 : ℝ) := by
 123  unfold muon_pred
 124  constructor
 125  · rw [lt_div_iff₀ (by norm_num : (0 : ℝ) < 4194304000000)]
 126    calc (101.49 : ℝ) * 4194304000000 < (425698000000000 : ℝ) := by norm_num
 127      _ < Constants.phi ^ 70 := phi70_gt
 128  · rw [div_lt_iff₀ (by norm_num : (0 : ℝ) < 4194304000000)]
 129    calc Constants.phi ^ 70 < (426011000000000 : ℝ) := phi70_lt
 130      _ < (101.57 : ℝ) * 4194304000000 := by norm_num
 131
 132theorem muon_relative_error :
 133    |rs_mass_MeV .Lepton 13 - m_mu_exp| / m_mu_exp < 0.04 := by
 134  rw [muon_pred_eq]
 135  have hb := muon_mass_bounds
 136  have hexp_pos : (0 : ℝ) < m_mu_exp := by unfold m_mu_exp; norm_num
 137  rw [div_lt_iff₀ hexp_pos, abs_lt]
 138  unfold m_mu_exp
 139  constructor <;> nlinarith [hb.1, hb.2]
 140