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

tau_relative_error

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)

 154theorem tau_relative_error :
 155    |rs_mass_MeV .Lepton 19 - m_tau_exp| / m_tau_exp < 0.03 := by

proof body

Tactic-mode proof.

 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
 163/-! ## Mass Ratio Verification -/
 164

used by (3)

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.