feat: add Liouville–Arnold eval problem

LeanEval/Geometry/LiouvilleArnold.lean

@@ -0,0 +1,88 @@
+import Mathlib
+import EvalTools.Markers
+
+namespace LeanEval
+namespace Geometry
+
+/-!
+# Liouville–Arnold theorem
+
+§45 of Knill's *Some Fundamental Theorems in Mathematics*. On a `2n`-
+dimensional symplectic manifold with `n` smooth, pointwise linearly
+independent, pairwise Poisson-commuting first integrals
+`F₁, …, F_n`, every compact connected component of a joint level set
+`{F₁ = c₁, …, F_n = c_n}` is diffeomorphic to the `n`-torus `T^n`.
+
+We formalize on `E n := EuclideanSpace ℝ (Fin (2n))` with the standard
+symplectic form `ω₀ = ∑ᵢ dpᵢ ∧ dqᵢ`. The induced Poisson bracket is
+`{F, G}(x) = ∑ᵢ ((∂F/∂pᵢ)(x)(∂G/∂qᵢ)(x) − (∂F/∂qᵢ)(x)(∂G/∂pᵢ)(x))`.
+
+Mathlib has `EuclideanSpace`, `fderiv`, `Matrix.charpoly`, `AddCircle`,
+`Homeomorph`, and the standard smooth-manifold framework, but **no
+Poisson brackets, no symplectic manifolds beyond `Matrix.symplecticGroup`,
+no first integrals, no Liouville–Arnold theorem in any form** (the
+`Liouville` files in `Mathlib/Analysis/Complex/` are Liouville's theorem
+on bounded entire functions, a different theorem). The Challenge ships
+~1 page of helper definitions (`E`, `idxP`, `idxQ`, `poissonBracket`,
+`IsLiouvilleIntegrable`, `levelSet`).
+-/
+
+open Set
+open scoped ContDiff
+
+/-- The model space `ℝ^{2n}`. -/
+abbrev E (n : ℕ) := EuclideanSpace ℝ (Fin (2 * n))
+
+/-- The "p" coordinate index `i ∈ Fin n` viewed in `Fin (2n)`. -/
+def idxP {n : ℕ} (i : Fin n) : Fin (2 * n) :=
+  ⟨i.val, by have := i.isLt; omega⟩
+
+/-- The "q" coordinate index `i ∈ Fin n` viewed in `Fin (2n)`. -/
+def idxQ {n : ℕ} (i : Fin n) : Fin (2 * n) :=
+  ⟨i.val + n, by have := i.isLt; omega⟩
+
+/-- Standard **Poisson bracket** on `ℝ^{2n}` for the symplectic form
+`ω₀ = ∑ᵢ dpᵢ ∧ dqᵢ`:
+`{F, G}(x) = ∑ᵢ ((∂F/∂pᵢ)(x)(∂G/∂qᵢ)(x) − (∂F/∂qᵢ)(x)(∂G/∂pᵢ)(x))`. -/
+noncomputable def poissonBracket {n : ℕ} (F G : E n → ℝ) (x : E n) : ℝ :=
+  ∑ i : Fin n,
+    (fderiv ℝ F x (EuclideanSpace.single (idxP i) (1 : ℝ)) *
+        fderiv ℝ G x (EuclideanSpace.single (idxQ i) (1 : ℝ))
+      - fderiv ℝ F x (EuclideanSpace.single (idxQ i) (1 : ℝ)) *
+        fderiv ℝ G x (EuclideanSpace.single (idxP i) (1 : ℝ)))
+
+/-- A tuple `F : Fin n → (E n → ℝ)` is **Liouville integrable on `U`**
+(an open subset of `ℝ^{2n}`) if each component is smooth on `U`, they
+pairwise Poisson-commute on `U`, and their Fréchet derivatives are
+linearly independent at every point of `U`. -/
+def IsLiouvilleIntegrable {n : ℕ} (F : Fin n → E n → ℝ) (U : Set (E n)) : Prop :=
+  (∀ i, ContDiffOn ℝ ∞ (F i) U) ∧
+  (∀ i j, ∀ x ∈ U, poissonBracket (F i) (F j) x = 0) ∧
+  (∀ x ∈ U, LinearIndependent ℝ (fun i => fderiv ℝ (F i) x))
+
+/-- The common level set `{x : F₁(x) = c₁, …, F_n(x) = c_n}`. -/
+def levelSet {n : ℕ} (F : Fin n → E n → ℝ) (c : Fin n → ℝ) : Set (E n) :=
+  {x | ∀ i, F i x = c i}
+
+/-- **Liouville–Arnold theorem.** For a Liouville integrable system on an
+open `U ⊆ ℝ^{2n}`, every compact connected joint level set
+`M_c = {x ∈ ℝ^{2n} : F₁(x) = c₁, …, F_n(x) = c_n}` contained in `U` is
+homeomorphic to the `n`-torus `T^n = (ℝ/ℤ)^n`.
+
+The hypotheses *compact* and *connected* on the level set, and its
+containment in the open set where the derivatives are independent,
+restore standard regularity assumptions that Knill elides; without them
+the conclusion fails. -/
+@[eval_problem]
+theorem liouville_arnold
+    {n : ℕ} (F : Fin n → E n → ℝ) (U : Set (E n)) (_hU : IsOpen U)
+    (_hLI : IsLiouvilleIntegrable F U)
+    (c : Fin n → ℝ)
+    (_hMc_sub : levelSet F c ⊆ U)
+    (_hMc_compact : IsCompact (levelSet F c))
+    (_hMc_connected : IsConnected (levelSet F c)) :
+    Nonempty ((levelSet F c) ≃ₜ (Fin n → AddCircle (1 : ℝ))) := by
+  sorry
+
+end Geometry
+end LeanEval

manifests/problems/liouville_arnold.toml

@@ -0,0 +1,9 @@
+id = "liouville_arnold"
+title = "Liouville–Arnold theorem on integrable systems"
+test = false
+module = "LeanEval.Geometry.LiouvilleArnold"
+holes = ["liouville_arnold"]
+submitter = "Kim Morrison"
+notes = "§45 of Knill's 'Some Fundamental Theorems in Mathematics'. On a 2n-dimensional symplectic manifold with n smooth, pointwise linearly independent, pairwise Poisson-commuting first integrals F₁, …, F_n, every compact connected component of a joint level set is diffeomorphic to the n-torus T^n. Formalized on ℝ^{2n} with the standard symplectic form ω₀ = ∑ᵢ dpᵢ ∧ dqᵢ. Mathlib has EuclideanSpace, fderiv, AddCircle, Homeomorph but no Poisson brackets, no symplectic manifolds beyond Matrix.symplecticGroup, no first integrals, and no Liouville–Arnold theorem in any form (the Liouville files in Mathlib/Analysis/Complex/ are Liouville's theorem on bounded entire functions, a different result). The Challenge ships ~1 page of helper definitions (E, idxP, idxQ, poissonBracket, IsLiouvilleIntegrable, levelSet)."
+source = "V. I. Arnold, *Mathematical Methods of Classical Mechanics* (2nd ed., 1989), Theorem 49.A.1 (the standard modern reference). The result is due to Liouville (1855) for the local existence of action-angle coordinates and Arnold (1963) for the compact-connected-component topology. Listed as §45 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf)."
+informal_solution = "Joint hamiltonian flows of F₁, …, F_n commute (by Poisson-commutativity) and are everywhere transverse to the level set (by linear independence of the gradients), so each compact connected component carries a transitive free action of ℝⁿ. The stabilizer is a discrete subgroup of full rank n (compactness), hence isomorphic to ℤⁿ, exhibiting M_c as ℝⁿ/ℤⁿ ≃ T^n."