EnergyConservationCert

formal source

  43
  44/-- Domain certificate for energy conservation along Newtonian
  45trajectories of the small-strain J-action. -/
  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`. -/
  68def energyConservationCert : EnergyConservationCert where
  69  energy_conserved := by
  70    intro m hm V γ hV_diff hγ_diff hγ_diff2 h_dE_factored hEL t₁ t₂
  71    exact HamiltonianMech.energy_conservation m hm V γ
  72      hV_diff hγ_diff hγ_diff2 h_dE_factored hEL t₁ t₂
  73  hamilton_qdot := by
  74    intro m hm V γ hV_diff hγ_diff hγ_diff2 hEL
  75    exact (HamiltonianMech.hamilton_equations_from_EL m hm V γ
  76      hV_diff hγ_diff hγ_diff2 hEL).1