Kuramoto order parameter

The Kuramoto order parameter for N oscillators with phases θ : Fin N → ℝ. Each oscillator contributes a unit phasor exp (i θ_k), and the main result is the bound ‖R‖ ≤ 1 where R = (∑_k exp (i θ_k)) / N.

noncomputable def kuramotoR (N : ℕ) (θ : Fin N → ℝ) : ℂ

The Kuramoto order parameter R = (∑_k exp (i θ_k)) / N.

Equations

• kuramotoR N θ = (∑ k : Fin N, Complex.exp (↑(θ k) * Complex.I)) / ↑N

theorem kuramotoR_norm_le_one (N : ℕ) (hN : 0 < N) (θ : Fin N → ℝ) : ‖kuramotoR N θ‖ ≤ 1