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.
Stronger theorems from the paper (convergence for fair schedules; cyclic convergence bounds) can be built on top of these monotonicity facts.
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)
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 : ℕ)
: