def
definition
def or abbrev
mond_mean_chi2
show as:
view Lean formalization →
formal statement (Lean)
120def mond_mean_chi2 : ℝ := 4.65
proof body
Definition body.
121
122/-- ILG has higher median but LOWER mean than MOND — it handles
123 outliers better due to the global-only constraint. -/