pith. machine review for the scientific record. sign in
theorem proved tactic proof

learning_compounds

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 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

proof body

Tactic-mode proof.

 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 _)
 559  simp only [dr1, dr2]; rw [h_cost_same]; nlinarith
 560

used by (1)

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

depends on (7)

Lean names referenced from this declaration's body.