 506
 507/-! ## Learning and Consolidation -/
 508
 509structure LearningEvent where
 510  experience : LedgerMemoryTrace
 511  attention : ℝ
 512  attention_bounded : 0 ≤ attention ∧ attention ≤ 1
 513  repetitions : ℕ
 514  spacing : ℕ
 515
 516noncomputable def spaced_bonus (event : LearningEvent) : ℝ :=
 517  log (1 + event.spacing / working_memory_window) / log φ
 518
 519theorem spaced_bonus_nonneg (event : LearningEvent) : 0 ≤ spaced_bonus event := by
 520  unfold spaced_bonus
 521  apply div_nonneg
 522  · apply log_nonneg
 523    have hs : 0 ≤ (event.spacing : ℝ) := by norm_cast; omega
 524    have hw : 0 < (working_memory_window : ℝ) := by norm_num [working_memory_window]
 525    linarith [div_nonneg hs hw.le]
 526  · exact log_nonneg Constants.phi_ge_one
 527
 528noncomputable def learning_rate (event : LearningEvent) : ℝ :=
 529  φ ^ (-(event.repetitions : ℝ)) * event.attention * (1 + spaced_bonus event)
 530
 531theorem learning_rate_nonneg (event : LearningEvent) : 0 ≤ learning_rate event := by
 532  unfold learning_rate
 533  apply mul_nonneg
 534  · apply mul_nonneg (rpow_pos_of_pos phi_pos _).le event.attention_bounded.1
 535  · linarith [spaced_bonus_nonneg event]
 536
 537theorem learning_compounds (e1 e2 : LearningEvent)
 538    (h_same : e1.experience = e2.experience)
 539    (h_more : e1.repetitions > e2.repetitions)

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.