Hopfield: basic lemmas #
This file contains small, reusable lemmas about the spec-level Hopfield definitions.
The “paper theorems” (energy monotonicity, convergence, Hebbian stability) should live in separate files once proved.
@[simp]
theorem
NN.MLTheory.Proofs.Hopfield.updateAt_apply_eq_update
{α : Type}
[AddCommMonoid α]
[Mul α]
[One α]
[Neg α]
[LE α]
[DecidableRel fun (x1 x2 : α) => x1 ≤ x2]
{n : ℕ}
(p : Spec.Hopfield.Params α n)
(s : Spec.Hopfield.State n)
(u : Fin n)
:
@[simp]
theorem
NN.MLTheory.Proofs.Hopfield.updateAt_apply_self
{α : Type}
[AddCommMonoid α]
[Mul α]
[One α]
[Neg α]
[LE α]
[DecidableRel fun (x1 x2 : α) => x1 ≤ x2]
{n : ℕ}
(p : Spec.Hopfield.Params α n)
(s : Spec.Hopfield.State n)
(u : Fin n)
:
@[simp]
theorem
NN.MLTheory.Proofs.Hopfield.updateAt_apply_ne
{α : Type}
[AddCommMonoid α]
[Mul α]
[One α]
[Neg α]
[LE α]
[DecidableRel fun (x1 x2 : α) => x1 ≤ x2]
{n : ℕ}
(p : Spec.Hopfield.Params α n)
(s : Spec.Hopfield.State n)
{u v : Fin n}
(h : v ≠ u)
:
theorem
NN.MLTheory.Proofs.Hopfield.pluses_updateAt_eq_succ_of_set_true
{α : Type}
[AddCommMonoid α]
[Mul α]
[One α]
[Neg α]
[LE α]
[DecidableRel fun (x1 x2 : α) => x1 ≤ x2]
{n : ℕ}
(p : Spec.Hopfield.Params α n)
(s : Spec.Hopfield.State n)
(u : Fin n)
(hsu : s u = false)
(hdec : decide (p.θ u ≤ Spec.Hopfield.net p s u) = true)
:
theorem
NN.MLTheory.Proofs.Hopfield.pluses_updateAt_eq_pred_of_set_false
{α : Type}
[AddCommMonoid α]
[Mul α]
[One α]
[Neg α]
[LE α]
[DecidableRel fun (x1 x2 : α) => x1 ≤ x2]
{n : ℕ}
(p : Spec.Hopfield.Params α n)
(s : Spec.Hopfield.State n)
(u : Fin n)
(hsu : s u = true)
(hdec : decide (p.θ u ≤ Spec.Hopfield.net p s u) = false)
: