Weinstein conjecture

AbbreviationSmooth one-forms#✓fully proved

Let \(M\) be a smooth manifold (possibly with boundary or corners). A smooth one-form on \(M\) is a smooth section of the cotangent bundle of \(M\): a smooth choice of a linear map \(\alpha_x : T_xM \to \mathbb{R}\) at each point \(x \in M\).

abbrev OneForm :=
  Cₛ^∞⟮I; E →L[ℝ] ℝ, fun x : M => TangentSpace I x →L[ℝ] ℝ⟯

Used by 4

Used byContact condition for a one-form · Exterior derivative of a one-form · Reeb vector fields · Weinstein conjecture in dimension three (Taubes)

AbbreviationTwo-forms as fields of bilinear forms#✓fully proved

Let \(M\) be a smooth manifold (possibly with boundary or corners). A two-form on \(M\) is here a smooth section of the bundle whose fiber at \(x \in M\) is the space of bilinear maps \(T_xM \times T_xM \to \mathbb{R}\); antisymmetry is not required.

abbrev TwoForm :=
  Cₛ^∞⟮I; E →L[ℝ] E →L[ℝ] ℝ,
    fun x : M => TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ⟯

Used by 4

Used byContact condition for a one-form · Exterior derivative of a one-form · Reeb vector fields · Weinstein conjecture in dimension three (Taubes)

AbbreviationSmooth vector fields#✓fully proved

Let \(M\) be a smooth manifold (possibly with boundary or corners). A smooth vector field on \(M\) is a smooth section of the tangent bundle of \(M\): a smooth choice of a tangent vector \(X_x \in T_xM\) at each point \(x \in M\).

abbrev SmoothVectorField :=
  Cₛ^∞⟮I; E, fun x : M => TangentSpace I x⟯

Used by 1

Used byExterior derivative of a one-form

DefinitionExterior derivative of a one-form#✓fully proved

A two-form \(d\alpha\) on \(M\) is the exterior derivative of a one-form \(\alpha\) on \(M\) when, for all smooth vector fields \(X, Y\) on \(M\) and every point \(x \in M\),

\[ d\alpha_x(X_x, Y_x) = X_x\big(\alpha(Y)\big) - Y_x\big(\alpha(X)\big) - \alpha_x\big([X, Y]_x\big), \]

where \(\alpha(Y)\) is the function \(y \mapsto \alpha_y(Y_y)\), \(X_x(f)\) is the derivative of a function \(f\) at \(x\) in the direction \(X_x\), and \([X, Y]\) is the Lie bracket of \(X\) and \(Y\).

This coordinate-free identity determines \(d\alpha\) uniquely.

def IsExteriorDerivative (α : OneForm I (M := M)) (dα : TwoForm I (M := M)) : Prop :=
  ∀ (X Y : SmoothVectorField I (M := M)) (x : M),
    let dXαY : ℝ := mfderiv I 𝓘(ℝ, ℝ) (fun y => α y (Y y)) x (X x)
    let dYαX : ℝ := mfderiv I 𝓘(ℝ, ℝ) (fun y => α y (X y)) x (Y x)
    dα x (X x) (Y x) = dXαY - dYαX - α x (VectorField.mlieBracket I (⇑X) (⇑Y) x)

Uses 3 · Used by 1

Statement usesSmooth one-forms · Smooth vector fields · Two-forms as fields of bilinear forms

Used byContact condition for a one-form

DefinitionContact condition for a one-form#✓fully proved

Let \(\alpha\) be a one-form and \(d\alpha\) a two-form on \(M\). The pair satisfies the contact condition when \(d\alpha\) is the exterior derivative of \(\alpha\) and, at every point \(x \in M\), the covector \(\alpha_x\) is nonzero and there are tangent vectors \(u, v \in T_xM\) with \(\alpha_x(u) = \alpha_x(v) = 0\) and \(d\alpha_x(u, v) \ne 0\).

When \(M\) has dimension \(3\), this says that \(\alpha\) vanishes nowhere and \(d\alpha\) is nondegenerate on the plane \(\ker \alpha_x\), which is equivalent to \(\alpha \wedge d\alpha\) vanishing nowhere.

def IsContactForm3 (α : OneForm I (M := M)) (dα : TwoForm I (M := M)) : Prop :=
  IsExteriorDerivative I α dα ∧
    ∀ x : M, α x ≠ 0 ∧ ∃ u v : TangentSpace I x,
      α x u = 0 ∧ α x v = 0 ∧ dα x u v ≠ 0

Uses 3 · Used by 1

Statement usesExterior derivative of a one-form · Smooth one-forms · Two-forms as fields of bilinear forms

Used byWeinstein conjecture in dimension three (Taubes)

DefinitionReeb vector fields#✓fully proved

Let \(\alpha\) be a one-form and \(d\alpha\) a two-form on \(M\). An assignment \(R\) of a tangent vector \(R(x) \in T_xM\) to each point \(x \in M\) is a Reeb vector field for \((\alpha, d\alpha)\) when, at every point \(x \in M\), \(\alpha_x(R(x)) = 1\) and \(d\alpha_x(R(x), v) = 0\) for all \(v \in T_xM\).

def IsReebVectorField (α : OneForm I (M := M)) (dα : TwoForm I (M := M))
    (R : ∀ x : M, TangentSpace I x) : Prop :=
  ∀ x : M, α x (R x) = 1 ∧ ∀ v : TangentSpace I x, dα x (R x) v = 0

Uses 2 · Used by 1

Statement usesSmooth one-forms · Two-forms as fields of bilinear forms

Used byWeinstein conjecture in dimension three (Taubes)

DefinitionIntegral curves#✓fully proved

Let \(M\) be a smooth manifold (possibly with boundary or corners) and let \(R\) assign to each point \(x \in M\) a tangent vector \(R(x) \in T_xM\). A curve \(\gamma : \mathbb{R} \to M\) is an integral curve of \(R\) when \(\gamma\) is smooth and \(\gamma'(t) = R(\gamma(t))\) for every \(t \in \mathbb{R}\).

def IsIntegralCurve (R : ∀ x : M, TangentSpace I x) (γ : ℝ → M) : Prop :=
  ContMDiff 𝓘(ℝ) I ∞ γ ∧
    ∀ t : ℝ, mfderiv 𝓘(ℝ) I γ t (1 : TangentSpace 𝓘(ℝ) t) = R (γ t)

Used by 1

Used byVector fields with a closed orbit

DefinitionVector fields with a closed orbit#✓fully proved

Let \(M\) be a smooth manifold (possibly with boundary or corners) and let \(R\) assign to each point \(x \in M\) a tangent vector \(R(x) \in T_xM\). We say that \(R\) has a closed orbit when there are a curve \(\gamma : \mathbb{R} \to M\) and a real number \(T > 0\) such that \(\gamma\) is \(T\)-periodic, \(\gamma\) is a smooth integral curve of \(R\), and \(\gamma\) is not constant.

The main theorem applies this to a Reeb vector field, whence the name closed Reeb orbit.

def HasClosedReebOrbit (R : ∀ x : M, TangentSpace I x) : Prop :=
  ∃ γ : ℝ → M, ∃ T : ℝ,
    0 < T ∧ Function.Periodic γ T ∧ IsIntegralCurve I R γ ∧ ∃ s t : ℝ, γ s ≠ γ t

Uses 1 · Used by 1

Statement usesIntegral curves

Used byWeinstein conjecture in dimension three (Taubes)

TheoremWeinstein conjecture in dimension three (Taubes)#●ready to prove

Let \(M\) be a nonempty compact Hausdorff smooth manifold without boundary, modelled on a real vector space of dimension \(3\). Let \(\alpha\) be a smooth one-form and \(d\alpha\) a smooth two-form on \(M\) satisfying the contact condition: \(d\alpha\) is the exterior derivative of \(\alpha\) and, at every point \(x\), \(\alpha_x \ne 0\) and \(d\alpha_x(u, v) \ne 0\) for some \(u, v \in \ker \alpha_x\). Let \(R\) be a Reeb vector field for \((\alpha, d\alpha)\). Then \(R\) has a closed orbit: a nonconstant smooth integral curve of \(R\) that is periodic with some positive period.

public theorem_wanted weinstein_conjecture_dim_three
    (E' : Type*) [NormedAddCommGroup E'] [NormedSpace ℝ E']
    [FiniteDimensional ℝ E']
    (H' : Type*) [TopologicalSpace H']
    (I' : ModelWithCorners ℝ E' H')
    (M' : Type*) [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' ∞ M']
    [T2Space M'] [CompactSpace M'] [Nonempty M'] [Fact (Module.finrank ℝ E' = 3)]
    [I'.Boundaryless]
    (α : OneForm I' (M := M')) (dα : TwoForm I' (M := M'))
    (R : ∀ x : M', TangentSpace I' x)
    (_hcontact : IsContactForm3 I' α dα)
    (_hReeb : IsReebVectorField I' α dα R) :
    HasClosedReebOrbit I' R

Sources

• C.H. Taubes, 'The Seiberg–Witten equations and the Weinstein conjecture', Geom. Topol. 11 (2007) 2117–2202; arXiv:math/0611007. Conjecture: A. Weinstein, 'On the hypotheses of Rabinowitz' periodic orbit theorems', J. Differential Equations 33 (1979) 353–358. §141 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem weinstein_conjecture_dim3 of the lean-eval benchmark.

Uses 5

Statement usesVector fields with a closed orbit · Contact condition for a one-form · Reeb vector fields · Smooth one-forms · Two-forms as fields of bilinear forms

8 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.