Hopfield: basic lemmas

An asynchronous update changes one Boolean coordinate. The lemmas here describe that change and its effect on the active-unit count, used to break energy ties in the convergence argument.

@[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) : Spec.Hopfield.updateAt p s u = Function.update s u (decide (p.θ u ≤ Spec.Hopfield.net p s u))

One asynchronous update is a Function.update at the chosen unit, with the threshold test as the new value. Stating it this way lets the Mathlib Function.update lemmas do the bookkeeping.

@[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) : Spec.Hopfield.updateAt p s u u = decide (p.θ u ≤ Spec.Hopfield.net p s u)

At the updated unit, the new state is the threshold test.

@[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) : Spec.Hopfield.updateAt p s u v = s v

Every other unit is untouched, which is what makes the update asynchronous.

theorem NN.MLTheory.Proofs.Hopfield.apply_eq_not_decide_of_updateAt_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 : Fin n) (h : Spec.Hopfield.updateAt p s u ≠ s) : s u = !decide (p.θ u ≤ Spec.Hopfield.net p s u)

When an update changes the state, the old value of the updated unit is the negation of the threshold test: every other unit is untouched, so the change must happen at u itself.

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) : Spec.Hopfield.pluses (Spec.Hopfield.updateAt p s u) = Spec.Hopfield.pluses s + 1

Flipping a unit from false to true raises the count of active units by one.

The active count is the tie-breaking measure in the convergence proof: when the energy stays flat, a real state change still has to move this counter, and it cannot rise forever.

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) : Spec.Hopfield.pluses (Spec.Hopfield.updateAt p s u) + 1 = Spec.Hopfield.pluses s

Flipping a unit from true to false lowers the active count by one.