Kuramoto gradient flow

The Kuramoto potential kuramotoV and force field kuramotoF, together with the gradient identity expressing the force as the negative phase-derivative of the potential.

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

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

Equations

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

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

The Kuramoto force on oscillator i, F_i = (K / N) ∑_j sin (θ_j - θ_i).

Equations

• kuramotoF K N i θ = K / ↑N * ∑ j : Fin N, Real.sin (θ j - θ i)

theorem kuramoto_gradient_identity (K : ℝ) (N : ℕ) (hN : 0 < N) (hK : 0 < K) (θ : Fin N → ℝ) (i : Fin N) : kuramotoF K N i θ = -deriv (fun (x : ℝ) => kuramotoV K N (Function.update θ i x)) (θ i)