structure definition def or abbrev

`LearningEvent`

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

formal statement (Lean)

 509structure LearningEvent where
 510  experience : LedgerMemoryTrace
 511  attention : ℝ
 512  attention_bounded : 0 ≤ attention ∧ attention ≤ 1
 513  repetitions : ℕ
 514  spacing : ℕ
 515

used by (5)

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

learning_compounds in IndisputableMonolith.Thermodynamics.MemoryLedger decl_use
learning_rate in IndisputableMonolith.Thermodynamics.MemoryLedger decl_use
learning_rate_nonneg in IndisputableMonolith.Thermodynamics.MemoryLedger decl_use
spaced_bonus in IndisputableMonolith.Thermodynamics.MemoryLedger decl_use
spaced_bonus_nonneg in IndisputableMonolith.Thermodynamics.MemoryLedger decl_use

depends on (1)

Lean names referenced from this declaration's body.

LedgerMemoryTrace in IndisputableMonolith.Thermodynamics.MemoryLedger decl_use