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

muon_electron_ratio_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)

 237theorem muon_electron_ratio_error :
 238    |Constants.phi ^ (11 : ℕ) - ratio_mu_e_exp| / ratio_mu_e_exp < 0.04 := by

proof body

Tactic-mode proof.

 239  have hr := ratio_mu_e_exp_bounds
 240  have hexp_pos : (0 : ℝ) < ratio_mu_e_exp := by linarith [hr.1]
 241  rw [div_lt_iff₀ hexp_pos, abs_lt]
 242  constructor <;> nlinarith [phi11_gt, phi11_lt, hr.1, hr.2]
 243

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.