learning_rate

formal source

 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)
 540    (h_attn : e1.attention = e2.attention)
 541    (h_space : e1.spacing = e2.spacing)
 542    (hs1 : e1.experience.strength > 0) (_hs2 : e2.experience.strength > 0) :
 543    let dr1 := -learning_rate e1 * memory_cost e1.experience e1.experience.encoding_tick
 544    let dr2 := -learning_rate e2 * memory_cost e2.experience e2.experience.encoding_tick
 545    dr1 ≥ dr2 := by
 546  intro dr1 dr2
 547  have h_pow_le : φ ^ (-(e1.repetitions : ℝ)) ≤ φ ^ (-(e2.repetitions : ℝ)) := by
 548    apply rpow_le_rpow_of_exponent_le (le_of_lt phi_gt_one)
 549    simp only [neg_le_neg_iff, Nat.cast_le]; exact Nat.le_of_lt h_more
 550  have h_bonus : spaced_bonus e1 = spaced_bonus e2 := by unfold spaced_bonus; rw [h_space]
 551  have h_lr_le : learning_rate e1 ≤ learning_rate e2 := by
 552    unfold learning_rate; rw [h_attn, h_bonus]
 553    apply mul_le_mul_of_nonneg_right _ (by linarith [spaced_bonus_nonneg e2])
 554    apply mul_le_mul_of_nonneg_right h_pow_le e2.attention_bounded.1
 555  have h_cost_same : memory_cost e1.experience e1.experience.encoding_tick =
 556                     memory_cost e2.experience e2.experience.encoding_tick := by rw [h_same]
 557  have h_cost_nonneg : 0 ≤ memory_cost e1.experience e1.experience.encoding_tick :=
 558    memory_cost_nonneg _ _ hs1 (le_refl _)