feat: add Darboux's theorem eval problem

LeanEval/Geometry/Darboux.lean

@@ -0,0 +1,86 @@
+import Mathlib
+import EvalTools.Markers
+
+namespace LeanEval
+namespace Geometry
+
+/-!
+# Darboux's theorem
+
+§39 of Oliver Knill's *Some Fundamental Theorems in Mathematics*. Every
+symplectic form on an open `U ⊆ ℝ^{2n}` is locally symplectomorphic to the
+standard symplectic form `ω₀ = ∑_{i=1}^n dxᵢ ∧ dx_{n+i}`.
+
+The local content lives entirely on open subsets of `ℝ^{2n}`; we formalize
+Darboux against mathlib's normed-space differential-form machinery.
+
+mathlib has continuous alternating maps, the exterior derivative `extDeriv`,
+pullbacks of alternating forms, `Matrix.symplecticGroup`, and
+`OpenPartialHomeomorph`, but no symplectic forms, no `ω₀` value, and no
+Darboux theorem (`Analysis/Calculus/Darboux.lean` is the unrelated
+derivative-IVT theorem). No formalization of Darboux's theorem was found in
+any other proof assistant.
+-/
+
+open Set Function Matrix
+open scoped ContDiff
+
+/-- The model space `ℝ^{2n}` for the local Darboux theorem. -/
+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⟩
+
+/-- A continuous alternating 2-form on `E n = ℝ^{2n}` is in **Darboux normal
+form** if its values on the standard basis are the Liouville symplectic
+values: `ω(eP_i, eQ_j) = δ_{ij}`, and `ω(eP_i, eP_j) = ω(eQ_i, eQ_j) = 0`.
+By antisymmetry these conditions uniquely determine the form (it is the
+standard symplectic form `ω₀ = ∑_i dxᵢ ∧ dx_{n+i}`). -/
+def IsDarbouxNormal {n : ℕ} (α : E n [⋀^Fin 2]→L[ℝ] ℝ) : Prop :=
+  (∀ i j : Fin n,
+      α ![EuclideanSpace.single (idxP i) (1 : ℝ),
+          EuclideanSpace.single (idxQ j) (1 : ℝ)]
+        = if i = j then (1 : ℝ) else 0) ∧
+  (∀ i j : Fin n,
+      α ![EuclideanSpace.single (idxP i) (1 : ℝ),
+          EuclideanSpace.single (idxP j) (1 : ℝ)] = 0) ∧
+  (∀ i j : Fin n,
+      α ![EuclideanSpace.single (idxQ i) (1 : ℝ),
+          EuclideanSpace.single (idxQ j) (1 : ℝ)] = 0)
+
+/-- A 2-form field `α` on an open set `U ⊆ ℝ^{2n}` is **symplectic** on `U`
+if it is smooth on `U`, closed on `U` (`dα = 0`), and pointwise
+non-degenerate. -/
+def IsSymplecticOn {n : ℕ}
+    (α : E n → E n [⋀^Fin 2]→L[ℝ] ℝ) (U : Set (E n)) : Prop :=
+  ContDiffOn ℝ ∞ α U ∧
+  (∀ x ∈ U, extDeriv α x = 0) ∧
+  (∀ x ∈ U, ∀ v : E n, v ≠ 0 → ∃ w : E n, α x ![v, w] ≠ 0)
+
+/-- **Darboux's theorem.** Every symplectic form on an open subset
+`U ⊆ ℝ^{2n}` is locally symplectomorphic to the standard symplectic form
+`ω₀`. Formally: for every `x ∈ U` there is a smooth local diffeomorphism
+`φ` (`OpenPartialHomeomorph`, smooth in both directions) whose source lies
+in `U` and contains `x`, such that on the target the pullback of `α` by
+`φ⁻¹` is in Darboux normal form (and hence equals `ω₀`) at every point. -/
+@[eval_problem]
+theorem darboux {n : ℕ} {U : Set (E n)} (_hU : IsOpen U)
+    (α : E n → E n [⋀^Fin 2]→L[ℝ] ℝ) (_hα : IsSymplecticOn α U)
+    {x : E n} (_hx : x ∈ U) :
+    ∃ φ : OpenPartialHomeomorph (E n) (E n),
+      x ∈ φ.source ∧ φ.source ⊆ U ∧
+      ContDiffOn ℝ ∞ (φ : E n → E n) φ.source ∧
+      ContDiffOn ℝ ∞ (φ.symm : E n → E n) φ.target ∧
+      ∀ z ∈ φ.target,
+        IsDarbouxNormal
+          ((α (φ.symm z)).compContinuousLinearMap
+            (fderiv ℝ (φ.symm : E n → E n) z)) := by
+  sorry
+
+end Geometry
+end LeanEval

manifests/problems.toml

@@ -673,3 +673,14 @@ module = "LeanEval.Geometry.Uniformization"
 holes = ["uniformization"]
 submitter = "Junyan Xu"
 source = "John Hamal Hubbard, *Teichmüller theory and applications to geometry, topology, and dynamics. Vol. 1*, Chapter 1."
+
+[[problem]]
+id = "darboux"
+title = "Darboux's theorem (symplectic forms are locally standard)"
+test = false
+module = "LeanEval.Geometry.Darboux"
+holes = ["darboux"]
+submitter = "Kim Morrison"
+notes = "§39 of Oliver Knill's 'Some Fundamental Theorems in Mathematics'. Every symplectic form on an open U ⊆ ℝ^{2n} is locally symplectomorphic to the standard symplectic form ω₀ = ∑_i dxᵢ ∧ dx_{n+i}. The local content lives on open subsets of ℝ^{2n}; formalized against mathlib's normed-space differential-form machinery (continuous alternating maps, extDeriv, OpenPartialHomeomorph). Mathlib has all the supporting infrastructure but no symplectic forms, no ω₀, and no Darboux theorem (Analysis/Calculus/Darboux.lean is the unrelated derivative-IVT theorem). No formalization of Darboux's theorem was found in any other proof assistant."
+source = "J. G. Darboux, Sur le problème de Pfaff, Bull. Sci. Math. 6 (1882), 14-36, 49-68. Listed as §39 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf)."
+informal_solution = "Moser's trick: choose linear coordinates at x ∈ U so that α(x) equals ω₀ on tangent vectors at x (possible because α is non-degenerate, by linear-algebraic normalization of an alternating bilinear form). Define the path of 2-forms αₜ := (1 − t)·ω₀ + t·α; each αₜ is closed and equals α at t = 1, ω₀ at t = 0, and αₜ(x) = ω₀(x) for all t. The closedness lets one write α − ω₀ = dβ for some 1-form β near x; non-degeneracy of αₜ near x lets one solve ι_{Xₜ} αₜ = -β for a time-dependent vector field Xₜ. Integrate Xₜ for t ∈ [0,1] starting at x to get a flow φ_t; then (φ_1)*α = ω₀ on a neighborhood, giving the desired symplectomorphism (after restricting to the open set where the flow is defined and bijective)."