standardEL

formal source

  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
  93    relationship between the cost functional `J` and the kinetic
  94    energy `½ m q̇²` (handled by `Jcost_taylor_quadratic`). -/
  95theorem newton_second_law (m : ℝ) (V : ℝ → ℝ) (γ : ℝ → ℝ) (t : ℝ) :
  96    standardEL m V γ t = 0 ↔ m * deriv (deriv γ) t = -(deriv V (γ t)) := by
  97  unfold standardEL
  98  constructor
  99  · intro h; linarith
 100  · intro h; linarith
 101
 102/-- **Inertia (Newton's First Law).** When the potential is constant
 103    (`V' ≡ 0`), the EL equation reduces to `m γ̈ = 0`, i.e., constant
 104    velocity motion. -/
 105theorem newton_first_law (m : ℝ) (hm : m ≠ 0) (γ : ℝ → ℝ) (t : ℝ)
 106    (h_no_force : deriv (fun _ : ℝ => (0 : ℝ)) (γ t) = 0)
 107    (h_EL : standardEL m (fun _ => 0) γ t = 0) :
 108    deriv (deriv γ) t = 0 := by
 109  rw [newton_second_law] at h_EL
 110  rw [h_no_force, neg_zero] at h_EL
 111  exact (mul_left_cancel₀ hm (by rw [h_EL, mul_zero]))