Hopfield global dynamics: energy along trajectories #
This file lifts the single-step energy lemma to whole trajectories:
for any (possibly adversarial) asynchronous update schedule useq, the energy sequence is
non-increasing.
Monotonicity alone does not guarantee convergence: a schedule might never update an unstable unit.
Convergence.lean proves finite-state convergence and a sweep bound for the cyclic schedule.
theorem
NN.MLTheory.Proofs.Hopfield.energy_seqStates_succ_le
{n : ℕ}
(p : Spec.Hopfield.Params ℝ n)
(hsym : SymmetricW p)
(hdiag : DiagonalZero p)
(useq : ℕ → Fin n)
(s0 : Spec.Hopfield.State n)
(k : ℕ)
:
Spec.Hopfield.energy p (Spec.Hopfield.seqStates p useq s0 (k + 1)) ≤ Spec.Hopfield.energy p (Spec.Hopfield.seqStates p useq s0 k)
Energy is nonincreasing along any update sequence, one step at a time.
theorem
NN.MLTheory.Proofs.Hopfield.energy_seqStates_le_start
{n : ℕ}
(p : Spec.Hopfield.Params ℝ n)
(hsym : SymmetricW p)
(hdiag : DiagonalZero p)
(useq : ℕ → Fin n)
(s0 : Spec.Hopfield.State n)
(k : ℕ)
:
Hence energy never exceeds its starting value, for any schedule of units.
The schedule is an arbitrary Nat → Fin n, so this covers random and cyclic orders alike.