Pairwise contraction

The relative velocity of two oscillators and the resulting pairwise contraction: when the phase gap lies in (0, π) and the coupling is positive, the gap is contracting.

theorem kuramoto_relative_velocity (K : ℝ) (θ : Fin 2 → ℝ) : kuramotoF K 2 0 θ - kuramotoF K 2 1 θ = -K * Real.sin (θ 0 - θ 1)

theorem kuramoto_pairwise_contraction (K : ℝ) (hK : 0 < K) (θ : Fin 2 → ℝ) (hgap : 0 < θ 0 - θ 1) (hpi : θ 0 - θ 1 < Real.pi) : kuramotoF K 2 0 θ < kuramotoF K 2 1 θ

theorem kuramoto_coupling_contraction (K : ℝ) (hK : 0 < K) (N : ℕ) (W : Fin N → Fin N → ℝ) (hW : ∀ (i j : Fin N), W i j = W j i) (θ : Fin N → ℝ) (i j : Fin N) (hWpos : 0 < W i j) (hgap : 0 < θ i - θ j) (hpi : θ i - θ j < Real.pi) : K * W i j * Real.sin (θ j - θ i) - K * W j i * Real.sin (θ i - θ j) < 0