  59/-- The standard kinetic action `T[ε] = (1/2) ∫_a^b ε(t)² dt`, viewed as
  60    the small-strain limit of the J-action via the substitution
  61    `γ = 1 + ε`. -/
  62noncomputable def kineticAction (a b : ℝ) (ε : ℝ → ℝ) : ℝ :=
  63  ∫ t in a..b, (ε t) ^ 2 / 2
  64
  65/-! ## Standard Lagrangian and Newton's law -/
  66
  67/-- The standard mechanics Lagrangian `L(q, q̇) = ½ m q̇² - V(q)`. -/
  68noncomputable def standardLagrangian (m : ℝ) (V : ℝ → ℝ) (q qdot : ℝ) : ℝ :=
  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'(γ)`. -/
  81noncomputable def standardEL (m : ℝ) (V : ℝ → ℝ) (γ : ℝ → ℝ) (t : ℝ) : ℝ :=
  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

papers checked against this theorem

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