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
proof body
Tactic-mode proof.
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'(γ) 86 intro t 87 have hEL_t := hEL t 88 rw [QuadraticLimit.newton_second_law m V γ t] at hEL_t 89 -- p(t) = m * deriv γ t, so deriv p t = m * deriv (deriv γ) t 90 have hp_eq : deriv (conjugateMomentum m γ) t = m * deriv (deriv γ) t := by 91 unfold conjugateMomentum 92 rw [deriv_const_mul m (hγ_diff2 t)] 93 rw [hp_eq, hEL_t] 94 95/-! ## Energy conservation -/ 96 97/-- The total energy of a trajectory: `E(t) = H(γ(t), p(t))`. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.