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

standardEL

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)

  81noncomputable def standardEL (m : ℝ) (V : ℝ → ℝ) (γ : ℝ → ℝ) (t : ℝ) : ℝ :=

proof body

Definition body.

  82  m * deriv (deriv γ) t + deriv V (γ t)
  83
  84/-- **Newton's Second Law from the Euler–Lagrange equation.**
  85
  86    The Euler–Lagrange equation `EL[γ](t) = 0` for the standard
  87    Lagrangian `L = ½ m q̇² - V(q)` is exactly Newton's second law
  88    `m γ̈ = -V'(γ)`.
  89
  90    This is a definitional consequence of `standardEL`: the EL operator
  91    is constructed so that its zero-set is exactly the Newtonian
  92    trajectories. Any quantitative dynamical content lives in the
  93    relationship between the cost functional `J` and the kinetic
  94    energy `½ m q̇²` (handled by `Jcost_taylor_quadratic`). -/

used by (8)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (21)

Lean names referenced from this declaration's body.