import GinibrePoincare.Concrete.Configuration
import Mathlib.LinearAlgebra.Vandermonde
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic

/-!
# The complex Vandermonde polynomial

This file connects the Vandermonde determinant used in the Ginibre density to
Mathlib's Vandermonde matrix.  It proves the product formula, the precise
collision zero set, nonvanishing on collision-free configurations, and
alternation under particle permutations.
-/

namespace GinibrePoincare

/-- The Vandermonde determinant of a complex particle configuration. -/
def vandermonde {n : ℕ} (z : Configuration n) : ℂ :=
  (Matrix.vandermonde z).det

/-- Product formula for the Vandermonde determinant. -/
theorem vandermonde_eq_product {n : ℕ} (z : Configuration n) :
    vandermonde z = ∏ i : Fin n, ∏ j > i, (z j - z i) := by
  exact Matrix.det_vandermonde z

/-- The Vandermonde vanishes exactly on the collision locus. -/
theorem vandermonde_eq_zero_iff {n : ℕ} (z : Configuration n) :
    vandermonde z = 0 ↔ z ∈ collisionSet n := by
  simpa only [vandermonde, mem_collisionSet_iff] using
    (Matrix.det_vandermonde_eq_zero_iff (v := z))

/-- The Vandermonde is nonzero exactly at collision-free configurations. -/
theorem vandermonde_ne_zero_iff {n : ℕ} (z : Configuration n) :
    vandermonde z ≠ 0 ↔ CollisionFree z := by
  simpa only [vandermonde, CollisionFree] using
    (Matrix.det_vandermonde_ne_zero_iff (v := z))

/-- Relabelling the particles multiplies the Vandermonde by the permutation sign. -/
theorem vandermonde_permute {n : ℕ} (σ : ParticlePermutation n)
    (z : Configuration n) :
    vandermonde (permute σ z) =
      permutationSign σ * vandermonde z := by
  have hmatrix :
      Matrix.vandermonde (permute σ z) =
        (Matrix.vandermonde z).submatrix σ id := by
    ext i j
    simp [permute]
  unfold vandermonde
  rw [hmatrix]
  simpa [permutationSign] using
    (Matrix.det_permute σ (Matrix.vandermonde z))

/-- The Vandermonde observable is alternating. -/
theorem vandermonde_isAlternating {n : ℕ} :
    IsAlternating (fun z : Configuration n => vandermonde z) := by
  intro σ z
  exact vandermonde_permute σ z

end GinibrePoincare