Weighted Kuramoto model

The weighted Kuramoto potential and vector field, where coupling strengths are given by a matrix W. For the gradient identity the coupling matrix is assumed symmetric.

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

The weighted Kuramoto potential V = -(K / 2) ∑_{i,j} W i j * cos (θ_j - θ_i).

Equations

• weightedKuramotoV K N W θ = -(K / 2) * ∑ i : Fin N, ∑ j : Fin N, W i j * Real.cos (θ j - θ i)

noncomputable def weightedKuramotoF (K : ℝ) (N : ℕ) (W : Fin N → Fin N → ℝ) (i : Fin N) (θ : Fin N → ℝ) : ℝ

The weighted Kuramoto force on oscillator i, F_i = K ∑_j W i j * sin (θ_j - θ_i).

Equations

• weightedKuramotoF K N W i θ = K * ∑ j : Fin N, W i j * Real.sin (θ j - θ i)

theorem weighted_gradient_identity (K : ℝ) (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 : ℝ) => weightedKuramotoV K N W (Function.update θ i x)) (θ i)

theorem weightedKuramotoV_symm_cancel (K : ℝ) (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 θ * weightedKuramotoF K N W i θ = -∑ i : Fin N, weightedKuramotoF K N W i θ * deriv (fun (x : ℝ) => weightedKuramotoV K N W (Function.update θ i x)) (θ i)

theorem weighted_lyapunov_descent (K : ℝ) (_hK : 0 < K) (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 : ℝ) => weightedKuramotoV K N W (Function.update θ i x)) (θ i) ≤ 0