def
definition
def or abbrev
learning_rate
show as:
view Lean formalization →
formal statement (Lean)
528noncomputable def learning_rate (event : LearningEvent) : ℝ :=
proof body
Definition body.
529 φ ^ (-(event.repetitions : ℝ)) * event.attention * (1 + spaced_bonus event)
530