Connections between the models

Relations between the weighted Kuramoto potential and the Hebbian Lyapunov function: with zero weight regularisation they coincide, and the Hebbian penalty is convex in each weight.

theorem hebbianL_zero_lam_eq_weighted (K : ℝ) (N : ℕ) (W : Fin N → Fin N → ℝ) (_hW : ∀ (i j : Fin N), W i j = W j i) (θ : Fin N → ℝ) : hebbianL K 0 N W θ = weightedKuramotoV K N W θ

With zero weight regularisation, the Hebbian Lyapunov function is exactly the weighted Kuramoto potential under the full double-sum convention used here.

theorem hebbianL_convex_weight_entry (K lam : ℝ) (hlam : 0 < lam) (N : ℕ) (W : Fin N → Fin N → ℝ) (θ : Fin N → ℝ) (i j : Fin N) : 0 < deriv (fun (x : ℝ) => deriv (fun (y : ℝ) => hebbianL K lam N (hebbianUpdateWeight W i j y) θ) x) (W i j)