def definition def or abbrev

`alpha_unmatch`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 106def alpha_unmatch (alpha_below : ℝ) : ℝ :=

Definition body.

 107  alpha_below * (1 - c_2_alpha * (alpha_below / Real.pi) ^ 2)
 108
 109/-! ## Master cert -/
 110

Lean names referenced from this declaration's body.