pith. machine review for the scientific record. sign in
def definition def or abbrev

standardLagrangian

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  68noncomputable def standardLagrangian (m : ℝ) (V : ℝ → ℝ) (q qdot : ℝ) : ℝ :=

proof body

Definition body.

  69  (m / 2) * qdot ^ 2 - V q
  70
  71/-- The Euler–Lagrange operator `(d/dt)(∂L/∂q̇) - ∂L/∂q` for the standard
  72    Lagrangian, evaluated on a smooth trajectory `γ`. The EL equation
  73    is `EL[γ](t) = 0`.
  74
  75    For `L = ½ m q̇² - V(q)`:
  76    * `∂L/∂q̇ = m q̇`, so `(d/dt)(∂L/∂q̇) = m γ̈(t)`.
  77    * `∂L/∂q = -V'(q)`, so `EL[γ](t) = m γ̈(t) + V'(γ(t))`.
  78
  79    The EL equation `EL[γ](t) = 0` is therefore `m γ̈ = -V'(γ)`,
  80    which is **Newton's second law** with force `F = -V'(γ)`. -/

depends on (16)

Lean names referenced from this declaration's body.