Hebbian phase/weight dynamics

A joint phase/weight Lyapunov function hebbianL with a Frobenius weight penalty, the Hebbian weight flow hebbianWeightF, and the joint Lyapunov descent property.

noncomputable def hebbianUpdateWeight {N : ℕ} (W : Fin N → Fin N → ℝ) (i j : Fin N) (x : ℝ) : Fin N → Fin N → ℝ

Update a single weight entry W i j to x (used to differentiate in that entry).

Equations

• hebbianUpdateWeight W i j x = Function.update W i (Function.update (W i) j x)

noncomputable def hebbianL (K lam : ℝ) (N : ℕ) (W : Fin N → Fin N → ℝ) (θ : Fin N → ℝ) : ℝ

Joint phase/weight Lyapunov function with a Frobenius weight penalty.

Equations

• hebbianL K lam N W θ = weightedKuramotoV K N W θ + lam / 2 * ∑ i : Fin N, ∑ j : Fin N, W i j * W i j

noncomputable def hebbianWeightF (K lam : ℝ) (N : ℕ) (W : Fin N → Fin N → ℝ) (θ : Fin N → ℝ) (i j : Fin N) : ℝ

Unprojected Hebbian weight flow, the negative weight-gradient of hebbianL.

Equations

• hebbianWeightF K lam N W θ i j = K / 2 * Real.cos (θ j - θ i) - lam * W i j

theorem hebbian_weight_gradient_identity (K lam : ℝ) (N : ℕ) (W : Fin N → Fin N → ℝ) (θ : Fin N → ℝ) (i j : Fin N) : hebbianWeightF K lam N W θ i j = -deriv (fun (x : ℝ) => hebbianL K lam N (hebbianUpdateWeight W i j x) θ) (W i j)

theorem hebbian_phase_gradient_identity (K lam : ℝ) (N : ℕ) (W : Fin N → Fin N → ℝ) (hW : ∀ (i j : Fin N), W i j = W j i) (θ : Fin N → ℝ) (i : Fin N) : weightedKuramotoF K N W i θ = -deriv (fun (x : ℝ) => hebbianL K lam N W (Function.update θ i x)) (θ i)

theorem hebbian_joint_lyapunov_descent (K lam : ℝ) (N : ℕ) (W : Fin N → Fin N → ℝ) (hW : ∀ (i j : Fin N), W i j = W j i) (θ : Fin N → ℝ) : ∑ i : Fin N, weightedKuramotoF K N W i θ * deriv (fun (x : ℝ) => hebbianL K lam N W (Function.update θ i x)) (θ i) + ∑ i : Fin N, ∑ j : Fin N, hebbianWeightF K lam N W θ i j * deriv (fun (x : ℝ) => hebbianL K lam N (hebbianUpdateWeight W i j x) θ) (W i j) ≤ 0