Symplectic geometry and Hamiltonian mechanics

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremTauCeti.CotangentBundle.isSymplectic_symplecticForm#

The canonical symplectic form of the cotangent bundle is closed and nondegenerate.

TauCeti.CotangentBundle.isSymplectic_symplecticForm.{u_1, u_2, u_3} {E : Type u_1} {H : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
  {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] :
  (TauCeti.CotangentBundle.symplecticForm I M).IsSymplectic

Lean

Formalized in Tau Ceti as TauCeti.CotangentBundle.isSymplectic_symplecticForm.

Sources

• Tau Ceti documentation: TauCeti.CotangentBundle.isSymplectic_symplecticForm
• Source of TauCeti.CotangentBundle.isSymplectic_symplecticForm in TauCeti/Geometry/Symplectic/Cotangent/Bundle/Liouville.lean
• Tau Ceti roadmap status: Symplectic geometry and Hamiltonian mechanics

LeanTauCeti.CotangentBundle.isSymplectic_symplecticForm

Uses 2 · Used by 1

Statement usesTauCeti.CotangentBundle

Proof usesChart formula for the canonical symplectic form

Used byThe unit codisc bundle is a Liouville domain

TheoremChart formula for the canonical symplectic form#

In every preferred chart of the cotangent bundle, the canonical symplectic form is the linear form TauCeti.strongDualCotangentSymplecticForm, ω((δq, δp), (δq', δp')) = δp'(δq) - δp(δq').

TauCeti.CotangentBundle.inChartAt_symplecticForm_apply.{u_1, u_2, u_3} {E : Type u_1} {H : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
  {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M]
  (z₀ : TauCeti.CotangentBundle I M) {w : E × (E →L[ℝ] ℝ)}
  (hw : w ∈ (extChartAt (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] ℝ))) z₀).target)
  (v : Fin 2 → E × (E →L[ℝ] ℝ)) :
  (TauCeti.RoughForm.inChartAt (↑(TauCeti.CotangentBundle.symplecticForm I M)) z₀ w) v =
    (fun v w => (TauCeti.strongDualCotangentSymplecticForm.toBilinForm v) w) (v 0) (v 1)

Lean

Formalized in Tau Ceti as TauCeti.CotangentBundle.inChartAt_symplecticForm_apply.

Sources

• Tau Ceti documentation: TauCeti.CotangentBundle.inChartAt_symplecticForm_apply
• Source of TauCeti.CotangentBundle.inChartAt_symplecticForm_apply in TauCeti/Geometry/Symplectic/Cotangent/Bundle/Liouville.lean
• Tau Ceti roadmap status: Symplectic geometry and Hamiltonian mechanics

LeanTauCeti.CotangentBundle.inChartAt_symplecticForm_apply

Uses 1 · Used by 2

Statement usesTauCeti.CotangentBundle

Used byThe unit codisc bundle is a Liouville domain · TauCeti.CotangentBundle.isSymplectic_symplecticForm

TheoremThe Liouville form is tautological#

Pulling it back along the smooth section of the cotangent bundle defined by a smooth one-form α gives back α.

TauCeti.CotangentBundle.mpullback_liouvilleForm.{u_1, u_2, u_3} {E : Type u_1} {H : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
  {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M]
  (α : TauCeti.SmoothForm I M ℝ 1) :
  (TauCeti.SmoothForm.mpullback (fun x => ⟨x, (TauCeti.SmoothForm.degreeOneEquiv α) x⟩) ⋯)
      (TauCeti.CotangentBundle.liouvilleForm I M) =
    α

Lean

Formalized in Tau Ceti as TauCeti.CotangentBundle.mpullback_liouvilleForm.

Sources

• Tau Ceti documentation: TauCeti.CotangentBundle.mpullback_liouvilleForm
• Source of TauCeti.CotangentBundle.mpullback_liouvilleForm in TauCeti/Geometry/Symplectic/Cotangent/Bundle/Liouville.lean
• Tau Ceti roadmap status: Symplectic geometry and Hamiltonian mechanics

LeanTauCeti.CotangentBundle.mpullback_liouvilleForm

Uses 1

Statement usesTauCeti.CotangentBundle

TheoremCotangent lifts are symplectic#

The cotangent lift of a smooth diffeomorphism pulls the canonical symplectic form of T*N back to the canonical symplectic form of T*M.

Diffeomorph.mpullback_cotangent_symplecticForm.{u_1, u_2, u_3, u_4, u_5, u_6} {E : Type u_1}
  {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4}
  {H' : Type u_5} [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H']
  {J : ModelWithCorners ℝ F H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N]
  [IsManifold I (↑⊤) M] [IsManifold J (↑⊤) N] (h : Diffeomorph I J M N ↑⊤) :
  (TauCeti.SmoothForm.mpullback ⇑h.cotangent ⋯) (TauCeti.CotangentBundle.symplecticForm J N) =
    TauCeti.CotangentBundle.symplecticForm I M

Lean

Formalized in Tau Ceti as Diffeomorph.mpullback_cotangent_symplecticForm.

Sources

• Tau Ceti documentation: Diffeomorph.mpullback_cotangent_symplecticForm
• Source of Diffeomorph.mpullback_cotangent_symplecticForm in TauCeti/Geometry/Symplectic/Cotangent/Bundle/Lift.lean
• Tau Ceti roadmap status: Symplectic geometry and Hamiltonian mechanics

LeanDiffeomorph.mpullback_cotangent_symplecticForm

Uses 1

Statement usesTauCeti.CotangentBundle

TheoremFibre translation by a closed one-form is symplectic#

Translating the fibres of the cotangent bundle by a one-form α preserves the canonical symplectic form exactly when α is closed.

TauCeti.CotangentBundle.mpullback_vectorBundleTranslateDiffeomorph_symplecticForm_eq_self_iff.{u_1,
    u_2, u_3}
  {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M]
  [IsManifold I (↑⊤) M] (α : TauCeti.SmoothForm I M ℝ 1) :
  (TauCeti.SmoothForm.mpullback
          ⇑(TauCeti.vectorBundleTranslateDiffeomorph ⇑(TauCeti.SmoothForm.degreeOneEquiv α) ⋯) ⋯)
        (TauCeti.CotangentBundle.symplecticForm I M) =
      TauCeti.CotangentBundle.symplecticForm I M ↔
    α.IsClosed

Lean

Formalized in Tau Ceti as TauCeti.CotangentBundle.mpullback_vectorBundleTranslateDiffeomorph_symplecticForm_eq_self_iff.

Sources

• Tau Ceti documentation: TauCeti.CotangentBundle.mpullback_vectorBundleTranslateDiffeomorph_symplecticForm_eq_self_iff
• Source of TauCeti.CotangentBundle.mpullback_vectorBundleTranslateDiffeomorph_symplecticForm_eq_self_iff in TauCeti/Geometry/Symplectic/Cotangent/Bundle/Fiberwise.lean
• Tau Ceti roadmap status: Symplectic geometry and Hamiltonian mechanics

LeanTauCeti.CotangentBundle.mpullback_vectorBundleTranslateDiffeomorph_symplecticForm_eq_self_iff

Uses 1

Statement usesTauCeti.CotangentBundle

TheoremTauCeti.SymplecticForm.isLagrangian_iff_maximal_isIsotropic#

Lagrangian subspaces are exactly the maximal isotropic subspaces, in any dimension.

TauCeti.SymplecticForm.isLagrangian_iff_maximal_isIsotropic.{u_1} {V : Type u_1} [AddCommGroup V]
  [_root_.Module ℝ V] {ω : TauCeti.SymplecticForm V} {L : Submodule ℝ V} :
  ω.IsLagrangian L ↔ Maximal ω.IsIsotropic L

Lean

Formalized in Tau Ceti as TauCeti.SymplecticForm.isLagrangian_iff_maximal_isIsotropic.

Sources

• Tau Ceti documentation: TauCeti.SymplecticForm.isLagrangian_iff_maximal_isIsotropic
• Source of TauCeti.SymplecticForm.isLagrangian_iff_maximal_isIsotropic in TauCeti/Geometry/Symplectic/Lagrangian/Basic.lean
• Tau Ceti roadmap status: Symplectic geometry and Hamiltonian mechanics

LeanTauCeti.SymplecticForm.isLagrangian_iff_maximal_isIsotropic

AbbreviationTauCeti.CotangentBundle#

The cotangent bundle of a manifold M modelled on I: the total space of the bundle whose fibre at x is the space of continuous linear functionals on TangentSpace I x. It is a manifold modelled on I.prod 𝓘(𝕜, E →L[𝕜] 𝕜).

TauCeti.CotangentBundle.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3}
  [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u_4) [TopologicalSpace M] [ChartedSpace H M] :
  Type (max u_4 u_1 u_2)

Lean

Formalized in Tau Ceti as TauCeti.CotangentBundle.

Sources

• Tau Ceti documentation: TauCeti.CotangentBundle
• Source of TauCeti.CotangentBundle in TauCeti/Geometry/Manifold/VectorBundle/Cotangent/Basic.lean
• Tau Ceti roadmap status: Symplectic geometry and Hamiltonian mechanics

LeanTauCeti.CotangentBundle

Used by 10

Used byThe unit codisc bundle is a Liouville domain · Closed normal disc theorem for a closed smooth submanifold · Smooth Riemannian tubular neighbourhood theorem · Chart formula for the canonical symplectic form · Cotangent lifts are symplectic · Fibre translation by a closed one-form is symplectic · TauCeti.CotangentBundle.isSymplectic_symplecticForm · The Liouville form is tautological · Transition maps of the cotangent bundle · Euler's identity for the kinetic energy

TheoremTransition maps of the cotangent bundle#

Changing from the preferred chart at z₀ to the preferred chart at z₁ sends (q, p) to (φ q, p ∘ (dφ_q)⁻¹), where φ is the change of base charts; (dφ_q)⁻¹ is the derivative of the inverse change of charts at φ q.

TauCeti.CotangentBundle.extChartAt_extChartAt_symm.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1}
  {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M]
  [ChartedSpace H M] [IsManifold I 1 M] (z₀ z₁ : TauCeti.CotangentBundle I M) {q : E}
  (p : E →L[𝕜] 𝕜) (hq : q ∈ (extChartAt I z₀.proj).target)
  (hq₁ : ↑(extChartAt I z₀.proj).symm q ∈ (extChartAt I z₁.proj).source) :
  ↑(extChartAt (I.prod (modelWithCornersSelf 𝕜 (E →L[𝕜] 𝕜))) z₁)
      (↑(extChartAt (I.prod (modelWithCornersSelf 𝕜 (E →L[𝕜] 𝕜))) z₀).symm (q, p)) =
    ((↑(extChartAt I z₁.proj) ∘ ↑(extChartAt I z₀.proj).symm) q,
      p ∘SL
        fderivWithin 𝕜 (↑(extChartAt I z₀.proj) ∘ ↑(extChartAt I z₁.proj).symm) (Set.range ↑I)
          ((↑(extChartAt I z₁.proj) ∘ ↑(extChartAt I z₀.proj).symm) q))

Lean

Formalized in Tau Ceti as TauCeti.CotangentBundle.extChartAt_extChartAt_symm.

Sources

• Tau Ceti documentation: TauCeti.CotangentBundle.extChartAt_extChartAt_symm
• Source of TauCeti.CotangentBundle.extChartAt_extChartAt_symm in TauCeti/Geometry/Manifold/VectorBundle/Cotangent/Basic.lean
• Tau Ceti roadmap status: Symplectic geometry and Hamiltonian mechanics

LeanTauCeti.CotangentBundle.extChartAt_extChartAt_symm

Uses 1

Statement usesTauCeti.CotangentBundle

TheoremBundle.isSubmersion_proj#

The projection of a fibre bundle is a submersion.

Bundle.isSubmersion_proj.{u_1, u_2, u_3, u_4, u_5, u_6} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3}
  {EB : Type u_4} {HB : Type u_5} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6}
  [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → TopologicalSpace (V x)]
  [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F V] [IsManifold IB n B]
  [IsManifold (IB.prod (modelWithCornersSelf 𝕜 F)) n (Bundle.TotalSpace F V)] :
  Manifold.IsSubmersion (IB.prod (modelWithCornersSelf 𝕜 F)) IB n Bundle.TotalSpace.proj

Lean

Formalized in Tau Ceti as Bundle.isSubmersion_proj.

Sources

• Tau Ceti documentation: Bundle.isSubmersion_proj
• Source of Bundle.isSubmersion_proj in TauCeti/Geometry/Manifold/VectorBundle/Submersion.lean
• Tau Ceti roadmap status: Symplectic geometry and Hamiltonian mechanics

LeanBundle.isSubmersion_proj

DefinitionTauCeti.SymplecticForm.IsSymplectic#

A submodule is symplectic if it meets its symplectic complement only in zero, equivalently (isSymplectic_iff_nondegenerate_restrict) ω restricts to it nondegenerately.

TauCeti.SymplecticForm.IsSymplectic.{u_1} {V : Type u_1} [AddCommGroup V] [_root_.Module ℝ V]
  (ω : TauCeti.SymplecticForm V) (L : Submodule ℝ V) : Prop

Lean

Formalized in Tau Ceti as TauCeti.SymplecticForm.IsSymplectic.

Sources

• Tau Ceti documentation: TauCeti.SymplecticForm.IsSymplectic
• Source of TauCeti.SymplecticForm.IsSymplectic in TauCeti/Geometry/Symplectic/Lagrangian/Basic.lean
• Tau Ceti roadmap status: Symplectic geometry and Hamiltonian mechanics

LeanTauCeti.SymplecticForm.IsSymplectic

TheoremAddCircle.instIsManifold#

The circle AddCircle p is an analytic manifold modelled on ℝ.

AddCircle.instIsManifold (p : ℝ) [Fact (0 < p)] {n : WithTop ℕ∞} :
  IsManifold (modelWithCornersSelf ℝ ℝ) n (AddCircle p)

Lean

Formalized in Tau Ceti as AddCircle.instIsManifold.

Sources

• Tau Ceti documentation: AddCircle.instIsManifold
• Source of AddCircle.instIsManifold in TauCeti/Geometry/Manifold/Instances/AddCircle.lean
• Tau Ceti roadmap status: Symplectic geometry and Hamiltonian mechanics

LeanAddCircle.instIsManifold

Uses 1

Proof usesHomeomorph.pullbackChartedSpace

TheoremAddCircle.isLocalDiffeomorph_coe#

The quotient map ℝ → AddCircle p is an analytic local diffeomorphism.

AddCircle.isLocalDiffeomorph_coe (p : ℝ) [Fact (0 < p)] (n : WithTop ℕ∞) :
  IsLocalDiffeomorph (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) n QuotientAddGroup.mk

Lean

Formalized in Tau Ceti as AddCircle.isLocalDiffeomorph_coe.

Sources

• Tau Ceti documentation: AddCircle.isLocalDiffeomorph_coe
• Source of AddCircle.isLocalDiffeomorph_coe in TauCeti/Geometry/Manifold/Instances/AddCircle.lean
• Tau Ceti roadmap status: Symplectic geometry and Hamiltonian mechanics

LeanAddCircle.isLocalDiffeomorph_coe

Uses 2

Proof usesHomeomorph.pullbackChartedSpace · Homeomorph.pullbackDiffeomorph

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.