Darboux's theorem

AbbreviationModel space \(\mathbb{R}^{2n}\) for Darboux's theorem#✓fully proved

For a natural number \(n\), the model space is \(\mathbb{R}^{2n}\), the Euclidean space of dimension \(2n\) with coordinates indexed by \(0, 1, \dots, 2n - 1\) and the standard inner product.

abbrev E (n : ℕ) := EuclideanSpace ℝ (Fin (2 * n))

Used by 3

Used byDarboux's theorem · Darboux normal form · Symplectic 2-form fields

DefinitionIndex of the \(i\)-th \(p\)-coordinate in \(\mathbb{R}^{2n}\)#✓fully proved

For \(i \in \{0, \dots, n - 1\}\), the index of the \(i\)-th \(p\)-coordinate among the coordinates \(0, \dots, 2n - 1\) of \(\mathbb{R}^{2n}\) is \(i\) itself.

def idxP {n : ℕ} (i : Fin n) : Fin (2 * n) :=
  ⟨i.val, by have := i.isLt; omega⟩

Used by 1

Used byDarboux normal form

DefinitionIndex of the \(i\)-th \(q\)-coordinate in \(\mathbb{R}^{2n}\)#✓fully proved

For \(i \in \{0, \dots, n - 1\}\), the index of the \(i\)-th \(q\)-coordinate among the coordinates \(0, \dots, 2n - 1\) of \(\mathbb{R}^{2n}\) is \(i + n\).

def idxQ {n : ℕ} (i : Fin n) : Fin (2 * n) :=
  ⟨i.val + n, by have := i.isLt; omega⟩

Used by 1

Used byDarboux normal form

DefinitionDarboux normal form#✓fully proved

Let \(n\) be a natural number and let \(e_0, \dots, e_{2n-1}\) be the standard basis of \(\mathbb{R}^{2n}\). A continuous alternating 2-form \(\omega\) on \(\mathbb{R}^{2n}\) is in Darboux normal form if for all \(i, j \in \{0, \dots, n - 1\}\) we have \(\omega(e_i, e_{n+j}) = 1\) when \(i = j\) and \(0\) otherwise, \(\omega(e_i, e_j) = 0\), and \(\omega(e_{n+i}, e_{n+j}) = 0\).

By antisymmetry these conditions determine the form uniquely: it is the standard symplectic form \(\omega_0 = \sum_i dx_i \wedge 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)

Uses 3 · Used by 1

Statement usesModel space \(\mathbb{R}^{2n}\) for Darboux's theorem · Index of the \(i\)-th \(p\)-coordinate in \(\mathbb{R}^{2n}\) · Index of the \(i\)-th \(q\)-coordinate in \(\mathbb{R}^{2n}\)

Used byDarboux's theorem

DefinitionSymplectic 2-form fields#✓fully proved

Let \(n\) be a natural number and \(U\) a subset of \(\mathbb{R}^{2n}\). A field \(\alpha\) of continuous alternating 2-forms on \(\mathbb{R}^{2n}\) is symplectic on \(U\) if \(\alpha\) is \(C^\infty\) on \(U\), its exterior derivative \(d\alpha\) vanishes at every point of \(U\), and \(\alpha\) is non-degenerate at every point of \(U\): for every \(x \in U\) and every nonzero \(v \in \mathbb{R}^{2n}\) there is \(w \in \mathbb{R}^{2n}\) with \(\alpha(x)(v, w) \neq 0\).

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)

Uses 1 · Used by 1

Statement usesModel space \(\mathbb{R}^{2n}\) for Darboux's theorem

Used byDarboux's theorem

TheoremDarboux's theorem#●ready to prove

Let \(n\) be a natural number, let \(U\) be an open subset of the model space \(\mathbb{R}^{2n}\), and let \(\alpha\) be a field of continuous alternating 2-forms on \(\mathbb{R}^{2n}\) that is symplectic on \(U\). Then for every \(x \in U\) there is an open partial homeomorphism \(\varphi\) of \(\mathbb{R}^{2n}\) whose source contains \(x\) and is contained in \(U\), such that \(\varphi\) is \(C^\infty\) on its source, \(\varphi^{-1}\) is \(C^\infty\) on its target, and for every \(z\) in the target the pullback of \(\alpha(\varphi^{-1}(z))\) by the derivative \(D\varphi^{-1}(z)\), namely \((v, w) \mapsto \alpha(\varphi^{-1}(z))(D\varphi^{-1}(z)\, v, D\varphi^{-1}(z)\, w)\), is in Darboux normal form.

public theorem_wanted 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))

Sources

• 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). Problem darboux of the lean-eval benchmark.

Uses 3

Statement usesModel space \(\mathbb{R}^{2n}\) for Darboux's theorem · Darboux normal form · Symplectic 2-form fields

5 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.