muon_relative_error

formal source

 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
 141/-! ## Tau Mass Verification -/
 142
 143theorem tau_mass_bounds :
 144    (1821 : ℝ) < tau_pred ∧ tau_pred < (1823 : ℝ) := by
 145  unfold tau_pred
 146  constructor
 147  · rw [lt_div_iff₀ (by norm_num : (0 : ℝ) < 4194304000000)]
 148    calc (1821 : ℝ) * 4194304000000 < (7638724000000000 : ℝ) := by norm_num
 149      _ < Constants.phi ^ 76 := phi76_gt
 150  · rw [div_lt_iff₀ (by norm_num : (0 : ℝ) < 4194304000000)]
 151    calc Constants.phi ^ 76 < (7646046000000000 : ℝ) := phi76_lt
 152      _ < (1823 : ℝ) * 4194304000000 := by norm_num
 153
 154theorem tau_relative_error :
 155    |rs_mass_MeV .Lepton 19 - m_tau_exp| / m_tau_exp < 0.03 := by
 156  rw [tau_pred_eq]
 157  have hb := tau_mass_bounds
 158  have hexp_pos : (0 : ℝ) < m_tau_exp := by unfold m_tau_exp; norm_num
 159  rw [div_lt_iff₀ hexp_pos, abs_lt]
 160  unfold m_tau_exp
 161  constructor <;> nlinarith [hb.1, hb.2]
 162