  52
  53    For the standard Hamiltonian `H = p²/(2m) + V(q)`,
  54    `∂H/∂q = V'(q)`, so `ṗ(t) = -V'(γ(t))`. -/
  55def hamiltonPDotEquation (V : ℝ → ℝ) (γ : ℝ → ℝ) (p : ℝ → ℝ) : Prop :=
  56  ∀ t : ℝ, deriv p t = -(deriv V (γ t))
  57
  58/-! ## EL ↔ Hamilton's equations -/
  59
  60/-- **Hamilton's equations from the Euler–Lagrange equation.**
  61
  62    Given a trajectory `γ` and conjugate momentum `p = m γ̇`, the EL
  63    equation for the standard Lagrangian implies Hamilton's equations:
  64
  65    * `q̇ = p/m` is *definitional*: it just says `m γ̇ = p`, i.e., the
  66      momentum is what we said it is.
  67    * `ṗ = -V'(q)` is the EL equation itself, since
  68      `ṗ = d(m γ̇)/dt = m γ̈ = -V'(γ)` by Newton's second law.
  69
  70    Therefore Hamilton's formulation and the Lagrangian formulation are
  71    equivalent for the standard mechanics Lagrangian. -/
  72theorem hamilton_equations_from_EL (m : ℝ) (hm : m ≠ 0) (V : ℝ → ℝ)
  73    (γ : ℝ → ℝ)
  74    (hV_diff : ∀ t, DifferentiableAt ℝ V (γ t))
  75    (hγ_diff : ∀ t, DifferentiableAt ℝ γ t)
  76    (hγ_diff2 : ∀ t, DifferentiableAt ℝ (deriv γ) t)
  77    (hEL : ∀ t : ℝ, QuadraticLimit.standardEL m V γ t = 0) :
  78    hamiltonQDotEquation m γ (conjugateMomentum m γ) ∧
  79    hamiltonPDotEquation V γ (conjugateMomentum m γ) := by
  80  constructor
  81  · -- q̇ = p/m where p = m γ̇
  82    intro t
  83    unfold conjugateMomentum
  84    field_simp
  85  · -- ṗ = -V'(γ): comes from EL ⇒ m γ̈ = -V'(γ)

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.