EnergyConservationCert

formal statement (Lean)

  46structure EnergyConservationCert where
  47  energy_conserved : ∀ (m : ℝ) (_hm : 0 < m) (V : ℝ → ℝ) (γ : ℝ → ℝ),
  48      (∀ t, DifferentiableAt ℝ V (γ t)) →
  49      (∀ t, DifferentiableAt ℝ γ t) →
  50      (∀ t, DifferentiableAt ℝ (deriv γ) t) →
  51      (∀ t : ℝ,
  52        deriv (HamiltonianMech.totalEnergy m V γ) t =
  53          deriv γ t * (m * deriv (deriv γ) t + deriv V (γ t))) →
  54      (∀ t : ℝ, QuadraticLimit.standardEL m V γ t = 0) →
  55      ∀ t₁ t₂ : ℝ,
  56        HamiltonianMech.totalEnergy m V γ t₁ =
  57          HamiltonianMech.totalEnergy m V γ t₂
  58  hamilton_qdot : ∀ (m : ℝ) (_hm : m ≠ 0) (V : ℝ → ℝ) (γ : ℝ → ℝ)
  59      (_hV_diff : ∀ t, DifferentiableAt ℝ V (γ t))
  60      (_hγ_diff : ∀ t, DifferentiableAt ℝ γ t)
  61      (_hγ_diff2 : ∀ t, DifferentiableAt ℝ (deriv γ) t)
  62      (_hEL : ∀ t : ℝ, QuadraticLimit.standardEL m V γ t = 0),
  63      HamiltonianMech.hamiltonQDotEquation m γ
  64        (HamiltonianMech.conjugateMomentum m γ)
  65
  66/-- Inhabited witness — both clauses are theorems in
  67`Action.Hamiltonian`. -/