Documentation

LeanPool.Kuramoto.Frontier

Kuramoto Frontier: ODE Solutions, Lyapunov Stability, and Synchronisation #

This file extends the Kuramoto oscillator library with results on:

  1. ODE existence and uniqueness (the vector field is smooth, hence locally Lipschitz)
  2. Lyapunov stability along trajectories
  3. Local synchronisation under the semicircle condition
  4. Phase diameter non-expansion
  5. Convergence to synchrony

We build on the algebraic identities proved in Weighted.lean, Contraction.lean, and GradientFlow.lean.

Target 1: Smoothness of the Kuramoto vector field and ODE existence #

source
noncomputable def kuramotoVectorField (K : ℝ) (N : ℕ) (W : Fin N → Fin N → ℝ) :
(Fin N → ℝ) → Fin N → ℝ

The Kuramoto vector field as a function (Fin N → ℝ) → (Fin N → ℝ).

Equations
Instances For
    source
    theorem kuramotoVectorField_contDiff (K : ℝ) (N : ℕ) (W : Fin N → Fin N → ℝ) :
    ContDiff ℝ ⊤ (kuramotoVectorField K N W)
    source
    theorem kuramotoVectorField_locallyLipschitz (K : ℝ) (N : ℕ) (W : Fin N → Fin N → ℝ) (θ₀ : Fin N → ℝ) :
    ∃ (ε : ℝ) (_ : 0 < ε) (L : NNReal), LipschitzOnWith L (kuramotoVectorField K N W) (Metric.ball θ₀ ε)
    source
    theorem kuramoto_ode_exists (K : ℝ) (N : ℕ) (W : Fin N → Fin N → ℝ) (θ₀ : Fin N → ℝ) :
    ∃ (θ : ℝ → Fin N → ℝ), θ 0 = θ₀ ∧ ∃ (ε : ℝ) (_ : 0 < ε), ∀ t ∈ Set.Ioo (-ε) ε, HasDerivAt θ (kuramotoVectorField K N W (θ t)) t
    source
    theorem kuramoto_ode_unique (K : ℝ) (N : ℕ) (W : Fin N → Fin N → ℝ) (θ θ' : ℝ → Fin N → ℝ) {T : ℝ} (_hT : 0 ≤ T) (hinit : θ 0 = θ' 0) (hf : ContinuousOn θ (Set.Icc 0 T)) (hf' : ∀ t ∈ Set.Ico 0 T, HasDerivWithinAt θ (kuramotoVectorField K N W (θ t)) (Set.Ici t) t) (hg : ContinuousOn θ' (Set.Icc 0 T)) (hg' : ∀ t ∈ Set.Ico 0 T, HasDerivWithinAt θ' (kuramotoVectorField K N W (θ' t)) (Set.Ici t) t) (hLip : ∃ (M : NNReal), LipschitzWith M (kuramotoVectorField K N W)) :
    Set.EqOn θ θ' (Set.Icc 0 T)

    Target 2: Lyapunov stability along trajectories #

    source
    theorem lyapunov_derivative_eq (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) = -∑ i : Fin N, weightedKuramotoF K N W i θ ^ 2
    source
    theorem lyapunov_derivative_nonpos (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
    source
    theorem lyapunov_nonincreasing_along_trajectory (K : ℝ) (_hK : 0 < K) (N : ℕ) (W : Fin N → Fin N → ℝ) (_hW : ∀ (i j : Fin N), W i j = W j i) (θ : ℝ → Fin N → ℝ) (hsol : ∀ (t : ℝ), HasDerivAt θ (kuramotoVectorField K N W (θ t)) t) (t : ℝ) :
    HasDerivAt (fun (s : ℝ) => weightedKuramotoV K N W (θ s)) (∑ i : Fin N, weightedKuramotoF K N W i (θ t) * deriv (fun (x : ℝ) => weightedKuramotoV K N W (Function.update (θ t) i x)) (θ t i)) t

    Target 3: Local synchronisation under the semicircle condition #

    source
    theorem semicircle_extremal_contraction (K : ℝ) (_hK : 0 < K) (N : ℕ) (_hN : 0 < N) (W : Fin N → Fin N → ℝ) (_hW : ∀ (i j : Fin N), W i j = W j i) (hWnn : ∀ (i j : Fin N), 0 ≤ W i j) (θ : Fin N → ℝ) (i j : Fin N) (_hij : i ≠ j) (_hWij : 0 < W i j) (hWeq : ∀ (k : Fin N), W i k = W j k) (hmax : ∀ (k : Fin N), θ k ≤ θ i) (hmin : ∀ (k : Fin N), θ j ≤ θ k) (hgap : θ i - θ j < Real.pi) :
    weightedKuramotoF K N W i θ - weightedKuramotoF K N W j θ ≤ 0
    source
    theorem sin_nonneg_of_phase_between {N : ℕ} (θ : Fin N → ℝ) (i j k : Fin N) (hmax : θ k ≤ θ i) (hmin : θ j ≤ θ k) (hgap : θ i - θ j < Real.pi) :
    0 ≤ Real.sin (θ k - θ j) ∧ 0 ≤ Real.sin (θ i - θ k)

    Target 4: Phase diameter non-expansion #

    source
    theorem extremal_gap_derivative_nonpos (K : ℝ) (hK : 0 < K) (N : ℕ) (hN : 0 < N) (W : Fin N → Fin N → ℝ) (hW : ∀ (i j : Fin N), W i j = W j i) (hWnn : ∀ (i j : Fin N), 0 ≤ W i j) (hWeq : ∀ (i j k : Fin N), W i k = W j k) (θ : ℝ → Fin N → ℝ) (hsol : ∀ (t : ℝ), HasDerivAt θ (kuramotoVectorField K N W (θ t)) t) (t : ℝ) (i j : Fin N) (hij : i ≠ j) (hWij : 0 < W i j) (hmax : ∀ (k : Fin N), θ t k ≤ θ t i) (hmin : ∀ (k : Fin N), θ t j ≤ θ t k) (hgap : θ t i - θ t j < Real.pi) :
    HasDerivAt (fun (s : ℝ) => θ s i - θ s j) (weightedKuramotoF K N W i (θ t) - weightedKuramotoF K N W j (θ t)) t ∧ weightedKuramotoF K N W i (θ t) - weightedKuramotoF K N W j (θ t) ≤ 0

    Target 5: Convergence to synchrony #

    source
    theorem kuramotoR_norm_eq_one_at_synchrony (N : ℕ) (hN : 0 < N) (θ : Fin N → ℝ) (hsync : ∀ (i j : Fin N), θ i = θ j) :
    ‖kuramotoR N θ‖ = 1
    source
    theorem weightedKuramotoV_bounded_below (K : ℝ) (hK : 0 < K) (N : ℕ) (W : Fin N → Fin N → ℝ) (hWnn : ∀ (i j : Fin N), 0 ≤ W i j) (hWle : ∀ (i j : Fin N), W i j ≤ 1) (θ : Fin N → ℝ) :
    -(K / 2) * ↑N ^ 2 ≤ weightedKuramotoV K N W θ

    Helper lemmas for convergence proof #

    source
    theorem allToAll_convergence_to_synchrony (K : ℝ) (hK : 0 < K) (N : ℕ) (hN : 2 ≤ N) (W : Fin N → Fin N → ℝ) (hWdiag : ∀ (i : Fin N), W i i = 0) (hWoff : ∀ (i j : Fin N), i ≠ j → W i j = 1) (θ : ℝ → Fin N → ℝ) (hsol : ∀ (t : ℝ), HasDerivAt θ (kuramotoVectorField K N W (θ t)) t) (hsemi : ∀ (a b : Fin N), |θ 0 a - θ 0 b| < Real.pi) :
    Filter.Tendsto (fun (t : ℝ) => ‖kuramotoR N (θ t)‖) Filter.atTop (nhds 1)

    Full convergence to synchrony under all-to-all coupling, K > 0, and initial phases in an open semicircle.