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

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

 108theorem mu_relative_error : |mu_pred - mu_codata| / mu_codata < 0.04 := by

proof body

Tactic-mode proof.

 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
 115/-! ## ScoreCard certificate -/
 116

used by (1)

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

depends on (3)

Lean names referenced from this declaration's body.