def
definition
def or abbrev
gradient_coefficient
show as:
view Lean formalization →
formal statement (Lean)
28noncomputable def gradient_coefficient (scale : ScaleFactor) (α C_lag : ℝ) (t : ℝ) : ℝ :=
proof body
Definition body.
29 let a := scale.a t
30 a * (1 + 0.01 * α * C_lag)
31