def definition def or abbrev

`harmonicEnergy`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 184noncomputable def harmonicEnergy (m k : ℝ) (pt : PhasePoint) : ℝ :=

Definition body.

 185  pt.p^2 / (2 * m) + k * pt.q^2 / 2
 186
 187/-- Harmonic oscillator flow (exact solution). -/

From the project-wide theorem graph. These declarations reference this one in their body.

harmonic_energy_conserved in IndisputableMonolith.QFT.NoetherTheorem decl_use

Lean names referenced from this declaration's body.